49 #ifndef __CVC4__EXPR_MANAGER_H 50 #define __CVC4__EXPR_MANAGER_H 71 #include "util/rational.h" 98 #line 38 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/expr/expr_manager_template.h" 107 struct ExprManagerMapCollection;
108 class StatisticsRegistry;
130 NodeManager* d_nodeManager;
133 IntStat* d_exprStatisticsVars[
LAST_TYPE];
140 NodeManager* getNodeManager()
const;
160 friend class ExprManagerScope;
163 friend class NodeManager;
188 explicit ExprManager(const
Options& options);
195 ~ExprManager() throw();
198 const
Options& getOptions() const;
362 Expr mkConst(const T&);
381 static
bool hasOperator(
Kind k);
451 mkMutualDatatypeTypes(const
std::vector<
Datatype>& datatypes);
483 mkMutualDatatypeTypes(const
std::vector<
Datatype>& datatypes,
484 const
std::set<
Type>& unresolvedTypes);
500 SORT_FLAG_PLACEHOLDER = 1
504 SortType mkSort(
const std::string& name, uint32_t flags = SORT_FLAG_NONE)
const;
538 Type getType(
Expr e,
bool check =
false)
569 Expr mkVar(
const std::string& name,
Type type, uint32_t flags = VAR_FLAG_NONE);
583 Expr mkVar(
Type type, uint32_t flags = VAR_FLAG_NONE);
602 Expr mkBoundVar(
const std::string& name,
Type type);
623 SExpr getStatistic(const
std::
string& name) const throw();
631 static
unsigned minArity(
Kind kind);
634 static
unsigned maxArity(
Kind kind);
639 #line 266 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 642 #line 276 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 645 #line 287 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 648 #line 309 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 651 #line 315 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 654 #line 343 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/builtin/kinds" 657 #line 21 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/booleans/kinds" 660 #line 29 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 663 #line 48 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 666 #line 61 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arith/kinds" 669 #line 15 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 672 #line 24 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 675 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 678 #line 83 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 681 #line 89 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 684 #line 95 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 687 #line 101 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 690 #line 107 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 693 #line 113 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 696 #line 127 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/bv/kinds" 699 #line 35 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/arrays/kinds" 702 #line 45 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 705 #line 77 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 708 #line 108 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 711 #line 116 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 714 #line 124 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 717 #line 144 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 720 #line 152 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/datatypes/kinds" 723 #line 18 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/sets/kinds" 726 #line 62 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds" 729 #line 68 "/builddir/build/BUILD/cvc4-1.4/builds/powerpc64-redhat-linux-gnu/production-abc-proof/../../../src/theory/strings/kinds" A class representing a Datatype definition.
Singleton class encapsulating the real type.
Class encapsulating the Selector type.
TypeConstant
The enumeration for the built-in atomic types.
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Singleton class encapsulating the integer type.
Class encapsulating a user-defined sort.
Class encapsulating an set type.
Class encapsulating a tuple type.
The representation of an inductive datatype.
Expr mkConst(const T &)
Create a constant of type T.
The structure representing the extraction of one Boolean bit.
Class encapsulating CVC4 expression types.
A class to represent a chained, built-in operator.
Simple representation of S-expressions.
A class representing a type ascription.
A multi-precision rational constant.
[[ Add one-line brief description here ]]
Representation of a constant array (an array in which the element is the same for all indices) ...
StatisticsRegistry * getStatisticsRegistry(ExprManager *)
Class encapsulating the Tester type.
Singleton class encapsulating the Boolean type.
marks the upper-bound of this enumeration
Representation of subrange bounds.
Exception thrown in the case of type-checking errors.
Class encapsulating an array type.
Class encapsulating a function type.
Class encapsulating a user-defined sort constructor.
Class encapsulating the datatype type.
Representation of abstract values.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Class encapsulating a record type.
A class used to parameterize a type ascription.
[[ Add one-line brief description here ]]
Class encapsulating a tuple type.
A class representing a Record definition.
[[ Add one-line brief description here ]]
[[ Add one-line brief description here ]]
Singleton class encapsulating the string type.
Representation of predicates for predicate subtyping.
[[ Add one-line brief description here ]]
Representation of constants of uninterpreted sorts.
Class encapsulating the constructor type.
A constructor for a Datatype.
[[ Add one-line brief description here ]]
Class encapsulating the bit-vector type.
The structure representing the divisibility-by-k predicate.
A hash function for Boolean.
Interface for expression types.