64 #include "util/rational.h" 87 #ifndef __CVC4__EXPR_H 88 #define __CVC4__EXPR_H 104 #line 44 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h" 109 template <
bool ref_count>
119 class TypeCheckingExceptionPrivate;
136 class SmtEnginePrivate;
154 friend class smt::SmtEnginePrivate;
165 const TypeCheckingExceptionPrivate* exc)
throw();
182 Expr getExpression()
const throw();
189 void toStream(std::ostream&
out)
const throw();
295 bool operator<(
const Expr& e)
const;
307 bool operator>(
const Expr& e)
const;
339 unsigned long getId()
const;
346 Kind getKind()
const;
353 size_t getNumChildren()
const;
361 Expr operator[](
unsigned i)
const;
367 return std::vector<Expr>(begin(), end());
373 Expr notExpr()
const;
410 Expr iteExpr(
const Expr& then_e,
const Expr& else_e)
const;
430 return !(*
this == it);
434 Expr operator*()
const;
452 bool hasOperator()
const;
460 Expr getOperator()
const;
496 Expr substitute(
const std::vector<Expr> exes,
497 const std::vector<Expr>& replacements)
const;
502 Expr substitute(
const std::hash_map<Expr, Expr, ExprHashFunction> map)
const;
508 std::string toString()
const;
522 void toStream(std::ostream& out,
int toDepth = -1,
bool types =
false,
size_t dag = 1,
537 bool isVariable()
const;
544 bool isConst()
const;
562 const T& getConst()
const;
623 void printAst(std::ostream& out,
int indent = 0)
const;
649 friend class smt::SmtEnginePrivate;
651 friend class NodeManager;
653 friend class expr::pickle::Pickler;
654 friend class prop::TheoryProxy;
655 friend class expr::ExportPrivate;
656 friend
std::ostream&
CVC4::operator<<(
std::ostream& out, const
Expr& e);
686 static const int s_iosIndex;
692 static const int s_defaultPrintDepth = -1;
706 out.iword(s_iosIndex) = d_depth;
710 long& l = out.iword(s_iosIndex);
722 return s_defaultPrintDepth;
728 static inline void setDepth(std::ostream& out,
long depth) {
729 out.iword(s_iosIndex) = depth;
744 inline Scope(std::ostream& out,
long depth) :
771 static const int s_iosIndex;
785 out.iword(s_iosIndex) = d_printTypes;
789 return out.iword(s_iosIndex);
793 out.iword(s_iosIndex) = printTypes;
804 bool d_oldPrintTypes;
808 inline Scope(std::ostream& out,
bool printTypes) :
829 static const int s_iosIndex;
835 static const size_t s_defaultDag = 1;
846 explicit ExprDag(
bool dag) : d_dag(dag ? 1 : 0) {}
853 explicit ExprDag(
int dag) : d_dag(dag < 0 ? 0 : dag) {}
857 out.iword(s_iosIndex) =
static_cast<long>(d_dag) + 1;
860 static inline size_t getDag(std::ostream& out) {
861 long& l = out.iword(s_iosIndex);
874 return s_defaultDag + 1;
877 return static_cast<size_t>(l - 1);
880 static inline void setDag(std::ostream& out,
size_t dag) {
882 out.iword(s_iosIndex) =
static_cast<long>(dag) + 1;
897 inline Scope(std::ostream& out,
size_t dag) :
899 d_oldDag(
ExprDag::getDag(out)) {
918 static const int s_iosIndex;
940 out.iword(s_iosIndex) = int(d_language) + 1;
944 long& l = out.iword(s_iosIndex);
965 out.iword(s_iosIndex) = int(l) + 1;
997 #line 266 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1000 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1003 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1006 #line 309 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1009 #line 315 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1012 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1015 #line 21 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds" 1016 template <>
bool const & Expr::getConst< bool >()
const;
1018 #line 29 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 1021 #line 48 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 1024 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 1027 #line 15 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1030 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1033 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1036 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1039 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1042 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1045 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1048 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1051 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1054 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1057 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds" 1060 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1063 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1066 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1069 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1072 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1075 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1078 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1081 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds" 1084 #line 62 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds" 1087 #line 68 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds" 1091 #line 938 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h" 1154 return (
size_t) e.
getId();
A class representing a Datatype definition.
::CVC4::TypeConstant const & Expr::getConst< ::CVC4::TypeConstant >() const
expr::ExprSetDepth setdepth
IOStream manipulator to set the maximum depth of Exprs when pretty-printing.
TypeConstant
The enumeration for the built-in atomic types.
Iterator type for the children of an Expr.
language::output::Language OutputLanguage
::CVC4::RecordUpdate const & Expr::getConst< ::CVC4::RecordUpdate >() const
::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >() const
Class encapsulating CVC4 expressions and methods for constructing new expressions.
expr::ExprPrintTypes printtypes
IOStream manipulator to print type ascriptions or not.
::CVC4::BitVectorRotateLeft const & Expr::getConst< ::CVC4::BitVectorRotateLeft >() const
Set the expression depth on the output stream for the current stack scope.
Set the dag state on the output stream for the current stack scope.
void applyDepth(std::ostream &out)
Set the print-types state on the output stream for the current stack scope.
ExprDag(bool dag)
Construct a ExprDag with the given setting (dagification on or off).
static size_t getDag(std::ostream &out)
bool operator>=(const Expr &e) const
Order comparison operator.
std::vector< Expr > getChildren() const
Returns the children of this Expr.
::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >() const
The representation of an inductive datatype.
static OutputLanguage getLanguage(std::ostream &out)
IOStream manipulator to set the output language for Exprs.
The structure representing the extraction of one Boolean bit.
static bool getPrintTypes(std::ostream &out)
Set a language on the output stream for the current stack scope.
Class encapsulating CVC4 expression types.
A class to represent a chained, built-in operator.
[[ Add one-line brief description here ]]
LANG_MAX is > any valid OutputLanguage id.
void applyLanguage(std::ostream &out)
ExprSetLanguage(OutputLanguage l)
Construct a ExprSetLanguage with the given setting.
::CVC4::String const & Expr::getConst< ::CVC4::String >() const
A class representing a type ascription.
A multi-precision rational constant.
unsigned long getId() const
Get the ID of this expression (used for the comparison operators).
static void setDepth(std::ostream &out, long depth)
::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >() const
::CVC4::AbstractValue const & Expr::getConst< ::CVC4::AbstractValue >() const
TheoryId & operator++(TheoryId &id)
Representation of a constant array (an array in which the element is the same for all indices) ...
CVC4's exception base class and some associated utilities.
std::ostream & operator<<(std::ostream &out, ExprSetDepth sd)
Sets the default depth when pretty-printing a Expr to an ostream.
::CVC4::IntToBitVector const & Expr::getConst< ::CVC4::IntToBitVector >() const
Match the output language to the input language.
Scope(std::ostream &out, long depth)
::CVC4::Record const & Expr::getConst< ::CVC4::Record >() const
IOStream manipulator to print type ascriptions or not.
::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >() const
IOStream manipulator to print expressions as a dag (or not).
Representation of subrange bounds.
Exception thrown in the case of type-checking errors.
::CVC4::RecordSelect const & Expr::getConst< ::CVC4::RecordSelect >() const
void applyDag(std::ostream &out)
::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >() const
Definition of input and output languages.
bool operator<=(const Expr &e) const
Order comparison operator.
Representation of abstract values.
static void setDag(std::ostream &out, size_t dag)
void applyPrintTypes(std::ostream &out)
struct CVC4::options::outputLanguage__option_t outputLanguage
::CVC4::BitVectorExtract const & Expr::getConst< ::CVC4::BitVectorExtract >() const
static Options & current()
Get the current Options in effect.
Macros that should be defined everywhere during the building of the libraries and driver binary...
::CVC4::BitVectorBitOf const & Expr::getConst< ::CVC4::BitVectorBitOf >() const
::CVC4::TupleUpdate const & Expr::getConst< ::CVC4::TupleUpdate >() const
A class used to parameterize a type ascription.
[[ Add one-line brief description here ]]
::CVC4::UninterpretedConstant const & Expr::getConst< ::CVC4::UninterpretedConstant >() const
Scope(std::ostream &out, OutputLanguage language)
::CVC4::BitVectorRotateRight const & Expr::getConst< ::CVC4::BitVectorRotateRight >() const
static long getDepth(std::ostream &out)
::CVC4::ArrayStoreAll const & Expr::getConst< ::CVC4::ArrayStoreAll >() const
A class representing a Record definition.
ExprDag(int dag)
Construct a ExprDag with the given setting (letify only common subexpressions that appear more than '...
size_t operator()(CVC4::Expr e) const
[[ Add one-line brief description here ]]
struct CVC4::options::defaultDagThresh__option_t defaultDagThresh
[[ Add one-line brief description here ]]
::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >() const
::CVC4::BitVectorSize const & Expr::getConst< ::CVC4::BitVectorSize >() const
ExprSetDepth(long depth)
Construct a ExprSetDepth with the given depth.
Representation of predicates for predicate subtyping.
::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >() const
ExprPrintTypes(bool printTypes)
Construct a ExprPrintTypes with the given setting.
[[ Add one-line brief description here ]]
expr::ExprSetLanguage setlanguage
IOStream manipulator to set the output language for Exprs.
struct CVC4::options::out__option_t out
IOStream manipulator to set the maximum depth of Exprs when pretty-printing.
Representation of constants of uninterpreted sorts.
::CVC4::BitVectorZeroExtend const & Expr::getConst< ::CVC4::BitVectorZeroExtend >() const
bool operator!=(const const_iterator &it) const
::CVC4::TupleSelect const & Expr::getConst< ::CVC4::TupleSelect >() const
ExportUnsupportedException(const char *msg)
Scope(std::ostream &out, bool printTypes)
::CVC4::SubrangeBounds const & Expr::getConst< ::CVC4::SubrangeBounds >() const
[[ Add one-line brief description here ]]
The structure representing the divisibility-by-k predicate.
bool operator!=(enum Result::Sat s, const Result &r)
ExportUnsupportedException()
A hash function for Boolean.
struct CVC4::options::defaultExprDepth__option_t defaultExprDepth
bool operator==(enum Result::Sat s, const Result &r)
expr::ExprDag dag
IOStream manipulator to print expressions as a DAG (or not).
::CVC4::BitVectorSignExtend const & Expr::getConst< ::CVC4::BitVectorSignExtend >() const
::CVC4::EmptySet const & Expr::getConst< ::CVC4::EmptySet >() const
::CVC4::BitVectorRepeat const & Expr::getConst< ::CVC4::BitVectorRepeat >() const
static void setLanguage(std::ostream &out, OutputLanguage l)
::CVC4::AscriptionType const & Expr::getConst< ::CVC4::AscriptionType >() const
::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >() const
static void setPrintTypes(std::ostream &out, bool printTypes)
Exception thrown in case of failure to export.
Scope(std::ostream &out, size_t dag)