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/i686-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h"
109 template <
bool ref_count>
118 class TypeCheckingException;
119 class TypeCheckingExceptionPrivate;
131 struct ExprManagerMapCollection;
133 struct ExprHashFunction;
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();
200 Exception("export unsupported") {
233 ExprManager* d_exprManager;
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;
416 ExprManager* d_exprManager;
430 return !(*
this == it);
434 Expr operator*()
const;
440 const_iterator begin()
const;
445 const_iterator end()
const;
452 bool hasOperator()
const;
460 Expr getOperator()
const;
497 const
std::vector<
Expr>& replacements) 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;
567 ExprManager* getExprManager() const;
610 typedef expr::ExprDag dag;
623 void printAst(
std::ostream& out,
int indent = 0) const;
649 friend class smt::SmtEnginePrivate;
650 friend class ExprManager;
651 friend class NodeManager;
652 friend class TypeCheckingException;
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) :
747 ExprSetDepth::setDepth(out, depth);
751 ExprSetDepth::setDepth(d_out, d_oldDepth);
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) :
811 ExprPrintTypes::setPrintTypes(out, printTypes);
815 ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
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)) {
900 ExprDag::setDag(out, dag);
904 ExprDag::setDag(d_out, d_oldDag);
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;
983 ExprSetLanguage::setLanguage(out, language);
987 ExprSetLanguage::setLanguage(d_out, d_oldLanguage);
997 #line 266 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1000 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1003 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1004 template <>
::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >()
const;
1006 #line 309 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1007 template <>
::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >()
const;
1009 #line 315 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1012 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds"
1013 template <>
::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >()
const;
1015 #line 21 "/builddir/build/BUILD/cvc4-1.4/builds/i686-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/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1019 template <>
::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >()
const;
1021 #line 48 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1024 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds"
1025 template <>
::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >()
const;
1027 #line 15 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1030 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1031 template <>
::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >()
const;
1033 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1036 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1039 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1042 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1045 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1048 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1051 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1054 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds"
1057 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds"
1060 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1061 template <>
::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >()
const;
1063 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1066 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1069 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1072 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1073 template <>
::CVC4::Record const & Expr::getConst< ::CVC4::Record >()
const;
1075 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1078 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds"
1081 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds"
1082 template <>
::CVC4::EmptySet const & Expr::getConst< ::CVC4::EmptySet >()
const;
1084 #line 62 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds"
1085 template <>
::CVC4::String const & Expr::getConst< ::CVC4::String >()
const;
1087 #line 68 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds"
1088 template <>
::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >()
const;
1091 #line 938 "/builddir/build/BUILD/cvc4-1.4/builds/i686-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_template.h"
1154 return (
size_t) e.
getId();
A class representing a Datatype definition.
TypeConstant
The enumeration for the built-in atomic types.
Iterator type for the children of an Expr.
language::output::Language OutputLanguage
Class encapsulating CVC4 expressions and methods for constructing new expressions.
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)
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.
A class representing a type ascription.
A multi-precision rational constant.
bool operator>=(const Expr &e) const
Order comparison operator.
static void setDepth(std::ostream &out, long depth)
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.
Match the output language to the input language.
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)
Definition of input and output languages.
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
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)
A class representing a Record definition.
ExprDag(int dag)
Construct a ExprDag with the given setting (letify only common subexpressions that appear more than '...
std::ostream & operator<<(std::ostream &out, const SubrangeBound &bound)
[[ 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.
ExprPrintTypes(bool printTypes)
Construct a ExprPrintTypes with the given setting.
[[ Add one-line brief description here ]]
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.
ExportUnsupportedException(const char *msg)
Scope(std::ostream &out, bool printTypes)
[[ 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)
static void setLanguage(std::ostream &out, OutputLanguage l)
static void setPrintTypes(std::ostream &out, bool printTypes)
Exception thrown in case of failure to export.
Scope(std::ostream &out, size_t dag)