49 #ifndef __CVC4__EXPR_MANAGER_H
50 #define __CVC4__EXPR_MANAGER_H
71 #include "util/rational.h"
97 #line 38 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/expr/expr_manager_template.h"
106 struct ExprManagerMapCollection;
107 class StatisticsRegistry;
129 NodeManager* d_nodeManager;
132 IntStat* d_exprStatisticsVars[
LAST_TYPE];
139 NodeManager* getNodeManager()
const;
159 friend class ExprManagerScope;
162 friend class NodeManager;
187 explicit ExprManager(const
Options& options);
194 ~ExprManager() throw();
197 const
Options& getOptions() const;
270 Expr mkExpr(
Kind kind, const std::vector<
Expr>& children);
283 Expr mkExpr(
Kind kind,
Expr child1, const std::vector<
Expr>& otherChildren);
357 Expr mkExpr(
Expr opExpr, const std::vector<
Expr>& children);
361 Expr mkConst(const T&);
374 Expr mkAssociative(
Kind kind, const std::vector<
Expr>& children);
380 static
bool hasOperator(
Kind k);
447 mkMutualDatatypeTypes(const std::vector<
Datatype>& datatypes);
479 mkMutualDatatypeTypes(const std::vector<
Datatype>& datatypes,
480 const std::set<
Type>& unresolvedTypes);
496 SORT_FLAG_PLACEHOLDER = 1
500 SortType mkSort(
const std::string& name, uint32_t flags = SORT_FLAG_NONE)
const;
534 Type getType(
Expr e,
bool check =
false)
565 Expr mkVar(
const std::string& name,
Type type, uint32_t flags = VAR_FLAG_NONE);
579 Expr mkVar(
Type type, uint32_t flags = VAR_FLAG_NONE);
598 Expr mkBoundVar(
const std::string& name,
Type type);
619 SExpr getStatistic(const std::
string& name) const throw();
627 static
unsigned minArity(
Kind kind);
630 static
unsigned maxArity(
Kind kind);
635 #line 264 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
638 #line 274 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
641 #line 285 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
644 #line 304 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
647 #line 310 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
650 #line 337 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/builtin/kinds"
653 #line 21 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/booleans/kinds"
656 #line 30 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
659 #line 49 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
662 #line 62 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arith/kinds"
665 #line 15 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
668 #line 24 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
671 #line 73 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
674 #line 79 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
677 #line 85 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
680 #line 91 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
683 #line 97 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
686 #line 103 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
689 #line 109 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
692 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/bv/kinds"
695 #line 35 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/arrays/kinds"
698 #line 45 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
701 #line 77 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
704 #line 107 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
707 #line 115 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
710 #line 123 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
713 #line 143 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
716 #line 151 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/datatypes/kinds"
719 #line 50 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-proof/../../../src/theory/strings/kinds"
722 #line 56 "/builddir/build/BUILD/cvc4-1.3/builds/aarch64-redhat-linux-gnu/default-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 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.
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
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.
Class encapsulating the bit-vector type.
The structure representing the divisibility-by-k predicate.
A multi-precision rational constant.
Interface for expression types.