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/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1000 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1003 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1006 #line 309 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1009 #line 315 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1012 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 1015 #line 21 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-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/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 1021 #line 48 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 1024 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 1027 #line 15 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1030 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1033 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1036 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1039 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1042 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1045 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1048 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1051 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1054 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 1057 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds" 1060 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1063 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1066 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1069 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1072 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1075 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1078 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 1081 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds" 1084 #line 62 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds" 1087 #line 68 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds" 1091 #line 938 "/builddir/build/BUILD/cvc4-1.4/builds/armv7hl-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h" 1154 return (
size_t) e.
getId();
A class representing a Datatype definition.
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::EmptySet const & Expr::getConst< ::CVC4::EmptySet >() const
::CVC4::UninterpretedConstant const & Expr::getConst< ::CVC4::UninterpretedConstant >() const
Class encapsulating CVC4 expressions and methods for constructing new expressions.
::CVC4::Record const & Expr::getConst< ::CVC4::Record >() const
expr::ExprPrintTypes printtypes
IOStream manipulator to print type ascriptions or not.
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)
::CVC4::BitVectorRotateRight const & Expr::getConst< ::CVC4::BitVectorRotateRight >() const
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)
The representation of an inductive datatype.
static OutputLanguage getLanguage(std::ostream &out)
IOStream manipulator to set the output language for Exprs.
::CVC4::BitVectorSize const & Expr::getConst< ::CVC4::BitVectorSize >() const
::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >() const
The structure representing the extraction of one Boolean bit.
static bool getPrintTypes(std::ostream &out)
::CVC4::String const & Expr::getConst< ::CVC4::String >() const
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::AbstractValue const & Expr::getConst< ::CVC4::AbstractValue >() const
A class representing a type ascription.
A multi-precision rational constant.
bool operator>=(const Expr &e) const
Order comparison operator.
::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >() const
static void setDepth(std::ostream &out, long depth)
::CVC4::TupleUpdate const & Expr::getConst< ::CVC4::TupleUpdate >() const
::CVC4::IntToBitVector const & Expr::getConst< ::CVC4::IntToBitVector >() const
TheoryId & operator++(TheoryId &id)
::CVC4::BitVectorRotateLeft const & Expr::getConst< ::CVC4::BitVectorRotateLeft >() const
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::BitVectorBitOf const & Expr::getConst< ::CVC4::BitVectorBitOf >() const
Match the output language to the input language.
::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >() const
Scope(std::ostream &out, long depth)
IOStream manipulator to print type ascriptions or not.
IOStream manipulator to print expressions as a dag (or not).
Representation of subrange bounds.
Exception thrown in the case of type-checking errors.
void applyDag(std::ostream &out)
::CVC4::BitVectorExtract const & Expr::getConst< ::CVC4::BitVectorExtract >() const
::CVC4::RecordSelect const & Expr::getConst< ::CVC4::RecordSelect >() const
::CVC4::ArrayStoreAll const & Expr::getConst< ::CVC4::ArrayStoreAll >() const
Definition of input and output languages.
::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >() const
Representation of abstract values.
::CVC4::BitVectorSignExtend const & Expr::getConst< ::CVC4::BitVectorSignExtend >() const
static void setDag(std::ostream &out, size_t dag)
void applyPrintTypes(std::ostream &out)
struct CVC4::options::outputLanguage__option_t outputLanguage
static Options & current()
Get the current Options in effect.
Macros that should be defined everywhere during the building of the libraries and driver binary...
std::vector< Expr > getChildren() const
Returns the children of this Expr.
A class used to parameterize a type ascription.
bool operator!=(const const_iterator &it) const
unsigned long getId() const
Get the ID of this expression (used for the comparison operators).
[[ Add one-line brief description here ]]
Scope(std::ostream &out, OutputLanguage language)
static long getDepth(std::ostream &out)
::CVC4::TypeConstant const & Expr::getConst< ::CVC4::TypeConstant >() const
A class representing a Record definition.
::CVC4::TupleSelect const & Expr::getConst< ::CVC4::TupleSelect >() const
ExprDag(int dag)
Construct a ExprDag with the given setting (letify only common subexpressions that appear more than '...
[[ Add one-line brief description here ]]
size_t operator()(CVC4::Expr e) const
struct CVC4::options::defaultDagThresh__option_t defaultDagThresh
[[ Add one-line brief description here ]]
bool operator<=(const Expr &e) const
Order comparison operator.
ExprSetDepth(long depth)
Construct a ExprSetDepth with the given depth.
Representation of predicates for predicate subtyping.
::CVC4::SubrangeBounds const & Expr::getConst< ::CVC4::SubrangeBounds >() 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::BitVectorRepeat const & Expr::getConst< ::CVC4::BitVectorRepeat >() const
ExportUnsupportedException(const char *msg)
Scope(std::ostream &out, bool printTypes)
[[ Add one-line brief description here ]]
::CVC4::AscriptionType const & Expr::getConst< ::CVC4::AscriptionType >() const
The structure representing the divisibility-by-k predicate.
bool operator!=(enum Result::Sat s, const Result &r)
::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >() const
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::RecordUpdate const & Expr::getConst< ::CVC4::RecordUpdate >() const
::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >() const
static void setLanguage(std::ostream &out, OutputLanguage l)
::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >() const
static void setPrintTypes(std::ostream &out, bool printTypes)
::CVC4::BitVectorZeroExtend const & Expr::getConst< ::CVC4::BitVectorZeroExtend >() const
Exception thrown in case of failure to export.
::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >() const
Scope(std::ostream &out, size_t dag)