64 #include "util/rational.h"
86 #ifndef __CVC4__EXPR_H
87 #define __CVC4__EXPR_H
103 #line 44 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/expr/expr_template.h"
108 template <
bool ref_count>
117 class TypeCheckingException;
118 class TypeCheckingExceptionPrivate;
130 struct ExprManagerMapCollection;
132 struct ExprHashFunction;
135 class SmtEnginePrivate;
153 friend class smt::SmtEnginePrivate;
164 const TypeCheckingExceptionPrivate* exc)
throw();
181 Expr getExpression() const throw();
188 void toStream(std::ostream&
out) const throw();
199 Exception("export unsupported") {
232 ExprManager* d_exprManager;
294 bool operator<(
const Expr& e)
const;
306 bool operator>(
const Expr& e)
const;
338 unsigned long getId()
const;
345 Kind getKind()
const;
352 size_t getNumChildren()
const;
360 Expr operator[](
unsigned i)
const;
366 return std::vector<Expr>(begin(), end());
372 Expr notExpr()
const;
409 Expr iteExpr(
const Expr& then_e,
const Expr& else_e)
const;
415 ExprManager* d_exprManager;
429 return !(*
this == it);
433 Expr operator*()
const;
439 const_iterator begin()
const;
444 const_iterator end()
const;
451 bool hasOperator()
const;
459 Expr getOperator()
const;
495 Expr substitute(const std::vector<
Expr> exes,
496 const std::vector<
Expr>& replacements) const;
507 std::
string toString() const;
521 void toStream(std::ostream&
out,
int toDepth = -1,
bool types = false,
size_t dag = 1,
536 bool isVariable() const;
543 bool isConst() const;
561 const T& getConst() const;
566 ExprManager* getExprManager() const;
609 typedef expr::ExprDag dag;
622 void printAst(std::ostream& out,
int indent = 0) const;
648 friend class smt::SmtEnginePrivate;
649 friend class ExprManager;
650 friend class NodeManager;
651 friend class TypeCheckingException;
652 friend class expr::pickle::Pickler;
653 friend class prop::TheoryProxy;
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 264 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1000 #line 274 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1003 #line 285 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1004 template <>
::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >()
const;
1006 #line 304 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1007 template <>
::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >()
const;
1009 #line 310 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1012 #line 337 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
1013 template <>
::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >()
const;
1015 #line 21 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/booleans/kinds"
1016 template <>
bool const & Expr::getConst< bool >()
const;
1018 #line 30 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
1019 template <>
::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >()
const;
1021 #line 49 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
1024 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
1025 template <>
::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >()
const;
1027 #line 15 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1030 #line 24 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1031 template <>
::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >()
const;
1033 #line 73 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1036 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1039 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1042 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1045 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1048 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1051 #line 109 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1054 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
1057 #line 35 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/arrays/kinds"
1060 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1061 template <>
::CVC4::Datatype const & Expr::getConst< ::CVC4::Datatype >()
const;
1063 #line 77 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1066 #line 107 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1069 #line 115 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1072 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1073 template <>
::CVC4::Record const & Expr::getConst< ::CVC4::Record >()
const;
1075 #line 143 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1078 #line 151 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
1081 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
1082 template <>
::CVC4::String const & Expr::getConst< ::CVC4::String >()
const;
1084 #line 56 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
1085 template <>
::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >()
const;
1088 #line 939 "/builddir/build/BUILD/cvc4-1.3/builds/armv7hl-redhat-linux-gnu/default-proof/../../../src/expr/expr_template.h"
1151 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.
NodeTemplate< true > exportInternal(NodeTemplate< false > n, ExprManager *from, ExprManager *to, ExprManagerMapCollection &vmap, uint32_t flags)
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.
Scope(std::ostream &out, long depth)
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
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 '...
[[ 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)
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
Scope(std::ostream &out, bool printTypes)
The structure representing the divisibility-by-k predicate.
bool operator!=(enum Result::Sat s, const Result &r)
ExportUnsupportedException()
A multi-precision rational constant.
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)