cvc4-1.3
|
#include <expr_manager.h>
Public Types | |
enum | { SORT_FLAG_NONE, SORT_FLAG_PLACEHOLDER } |
Bits for use in mkSort() flags. More... | |
enum | { VAR_FLAG_NONE, VAR_FLAG_GLOBAL, VAR_FLAG_DEFINED } |
Bits for use in mkVar() flags. More... | |
Public Member Functions | |
ExprManager () | |
Creates an expression manager with default options. More... | |
ExprManager (const Options &options) | |
Creates an expression manager. More... | |
~ExprManager () throw () | |
Destroys the expression manager. More... | |
const Options & | getOptions () const |
Get this node manager's options. More... | |
BooleanType | booleanType () const |
Get the type for booleans. More... | |
StringType | stringType () const |
Get the type for strings. More... | |
RealType | realType () const |
Get the type for reals. More... | |
IntegerType | integerType () const |
Get the type for integers. More... | |
Expr | mkExpr (Kind kind, Expr child1) |
Make a unary expression of a given kind (NOT, BVNOT, ...). More... | |
Expr | mkExpr (Kind kind, Expr child1, Expr child2) |
Make a binary expression of a given kind (AND, PLUS, ...). More... | |
Expr | mkExpr (Kind kind, Expr child1, Expr child2, Expr child3) |
Make a 3-ary expression of a given kind (AND, PLUS, ...). More... | |
Expr | mkExpr (Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) |
Make a 4-ary expression of a given kind (AND, PLUS, ...). More... | |
Expr | mkExpr (Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) |
Make a 5-ary expression of a given kind (AND, PLUS, ...). More... | |
Expr | mkExpr (Kind kind, const std::vector< Expr > &children) |
Make an n-ary expression of given kind given a vector of its children. More... | |
Expr | mkExpr (Kind kind, Expr child1, const std::vector< Expr > &otherChildren) |
Make an n-ary expression of given kind given a first arg and a vector of its remaining children (this can be useful where the kind is parameterized operator, so the first arg is really an arg to the kind to construct an operator) More... | |
Expr | mkExpr (Expr opExpr) |
Make a nullary parameterized expression with the given operator. More... | |
Expr | mkExpr (Expr opExpr, Expr child1) |
Make a unary parameterized expression with the given operator. More... | |
Expr | mkExpr (Expr opExpr, Expr child1, Expr child2) |
Make a binary parameterized expression with the given operator. More... | |
Expr | mkExpr (Expr opExpr, Expr child1, Expr child2, Expr child3) |
Make a ternary parameterized expression with the given operator. More... | |
Expr | mkExpr (Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4) |
Make a quaternary parameterized expression with the given operator. More... | |
Expr | mkExpr (Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) |
Make a quinary parameterized expression with the given operator. More... | |
Expr | mkExpr (Expr opExpr, const std::vector< Expr > &children) |
Make an n-ary expression of given operator to apply and a vector of its children. More... | |
template<class T > | |
Expr | mkConst (const T &) |
Create a constant of type T. More... | |
Expr | mkAssociative (Kind kind, const std::vector< Expr > &children) |
Create an Expr by applying an associative operator to the children. More... | |
Expr | operatorOf (Kind k) |
Get the (singleton) operator of an OPERATOR-kinded kind. More... | |
FunctionType | mkFunctionType (Type domain, Type range) |
Make a function type from domain to range. More... | |
FunctionType | mkFunctionType (const std::vector< Type > &argTypes, Type range) |
Make a function type with input types from argTypes. More... | |
FunctionType | mkFunctionType (const std::vector< Type > &sorts) |
Make a function type with input types from sorts[0..sorts.size()-2] and result type sorts[sorts.size()-1] . More... | |
FunctionType | mkPredicateType (const std::vector< Type > &sorts) |
Make a predicate type with input types from sorts . More... | |
TupleType | mkTupleType (const std::vector< Type > &types) |
Make a tuple type with types from types[0..types.size()-1] . More... | |
RecordType | mkRecordType (const Record &rec) |
Make a record type with types from the rec parameter. More... | |
SExprType | mkSExprType (const std::vector< Type > &types) |
Make a symbolic expressiontype with types from types[0..types.size()-1] . More... | |
BitVectorType | mkBitVectorType (unsigned size) const |
Make a type representing a bit-vector of the given size. More... | |
ArrayType | mkArrayType (Type indexType, Type constituentType) const |
Make the type of arrays with the given parameterization. More... | |
DatatypeType | mkDatatypeType (const Datatype &datatype) |
Make a type representing the given datatype. More... | |
std::vector< DatatypeType > | mkMutualDatatypeTypes (const std::vector< Datatype > &datatypes) |
Make a set of types representing the given datatypes, which may be mutually recursive. More... | |
std::vector< DatatypeType > | mkMutualDatatypeTypes (const std::vector< Datatype > &datatypes, const std::set< Type > &unresolvedTypes) |
Make a set of types representing the given datatypes, which may be mutually recursive. More... | |
ConstructorType | mkConstructorType (const DatatypeConstructor &constructor, Type range) const |
Make a type representing a constructor with the given parameterization. More... | |
SelectorType | mkSelectorType (Type domain, Type range) const |
Make a type representing a selector with the given parameterization. More... | |
TesterType | mkTesterType (Type domain) const |
Make a type representing a tester with the given parameterization. More... | |
SortType | mkSort (const std::string &name, uint32_t flags=SORT_FLAG_NONE) const |
Make a new sort with the given name. More... | |
SortConstructorType | mkSortConstructor (const std::string &name, size_t arity) const |
Make a sort constructor from a name and arity. More... | |
Type | mkSubrangeType (const SubrangeBounds &bounds) throw (TypeCheckingException) |
Make a predicate subtype type defined by the given LAMBDA expression. More... | |
Type | getType (Expr e, bool check=false) throw (TypeCheckingException) |
Get the type of an expression. More... | |
Expr | mkVar (const std::string &name, Type type, uint32_t flags=VAR_FLAG_NONE) |
Create a new, fresh variable. More... | |
Expr | mkVar (Type type, uint32_t flags=VAR_FLAG_NONE) |
Create a (nameless) new, fresh variable. More... | |
Expr | mkBoundVar (const std::string &name, Type type) |
Create a new, fresh variable for use in a binder expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). More... | |
Expr | mkBoundVar (Type type) |
Create a (nameless) new, fresh variable for use in a binder expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). More... | |
Statistics | getStatistics () const throw () |
Get a reference to the statistics registry for this ExprManager. More... | |
SExpr | getStatistic (const std::string &name) const throw () |
Get a reference to the statistics registry for this ExprManager. More... | |
template<> | |
Expr | mkConst (::CVC4::UninterpretedConstant const &val) |
template<> | |
Expr | mkConst (::CVC4::AbstractValue const &val) |
template<> | |
Expr | mkConst (::CVC4::Kind const &val) |
template<> | |
Expr | mkConst (::CVC4::Chain const &val) |
template<> | |
Expr | mkConst (::CVC4::TypeConstant const &val) |
template<> | |
Expr | mkConst (::CVC4::Predicate const &val) |
template<> | |
Expr | mkConst (bool const &val) |
template<> | |
Expr | mkConst (::CVC4::Divisible const &val) |
template<> | |
Expr | mkConst (::CVC4::SubrangeBounds const &val) |
template<> | |
Expr | mkConst (::CVC4::Rational const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorSize const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVector const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorBitOf const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorExtract const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorRepeat const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorZeroExtend const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorSignExtend const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorRotateLeft const &val) |
template<> | |
Expr | mkConst (::CVC4::BitVectorRotateRight const &val) |
template<> | |
Expr | mkConst (::CVC4::IntToBitVector const &val) |
template<> | |
Expr | mkConst (::CVC4::ArrayStoreAll const &val) |
template<> | |
Expr | mkConst (::CVC4::Datatype const &val) |
template<> | |
Expr | mkConst (::CVC4::AscriptionType const &val) |
template<> | |
Expr | mkConst (::CVC4::TupleSelect const &val) |
template<> | |
Expr | mkConst (::CVC4::TupleUpdate const &val) |
template<> | |
Expr | mkConst (::CVC4::Record const &val) |
template<> | |
Expr | mkConst (::CVC4::RecordSelect const &val) |
template<> | |
Expr | mkConst (::CVC4::RecordUpdate const &val) |
template<> | |
Expr | mkConst (::CVC4::String const &val) |
template<> | |
Expr | mkConst (::CVC4::RegExp const &val) |
Static Public Member Functions | |
static bool | hasOperator (Kind k) |
Determine whether Exprs of a particular Kind have operators. More... | |
static Type | exportType (const Type &t, ExprManager *em, ExprManagerMapCollection &vmap) |
Export an expr to a different ExprManager. More... | |
static unsigned | minArity (Kind kind) |
Returns the minimum arity of the given kind. More... | |
static unsigned | maxArity (Kind kind) |
Returns the maximum arity of the given kind. More... | |
Friends | |
class | SmtEngine |
SmtEngine will use all the internals, so it will grab the NodeManager. More... | |
class | ExprManagerScope |
ExprManagerScope reaches in to get the NodeManager. More... | |
class | NodeManager |
NodeManager reaches in to get the NodeManager. More... | |
friend::CVC4::StatisticsRegistry * | CVC4::stats::getStatisticsRegistry (ExprManager *) |
Statistics reach in to get the StatisticsRegistry. More... | |
Definition at line 123 of file expr_manager.h.
anonymous enum |
Bits for use in mkSort() flags.
Enumerator | |
---|---|
SORT_FLAG_NONE | |
SORT_FLAG_PLACEHOLDER |
Definition at line 494 of file expr_manager.h.
anonymous enum |
Bits for use in mkVar() flags.
Enumerator | |
---|---|
VAR_FLAG_NONE | |
VAR_FLAG_GLOBAL | |
VAR_FLAG_DEFINED |
Definition at line 538 of file expr_manager.h.
CVC4::ExprManager::ExprManager | ( | ) |
Creates an expression manager with default options.
|
explicit |
Creates an expression manager.
options | the earlyTypeChecking field is used to configure whether to do at Expr creation time. |
CVC4::ExprManager::~ExprManager | ( | ) | ||
throw | ( | |||
) |
Destroys the expression manager.
No will be deallocated at this point, so any expression references that used to be managed by this expression manager and are left-over are bad.
BooleanType CVC4::ExprManager::booleanType | ( | ) | const |
Get the type for booleans.
|
static |
Export an expr to a different ExprManager.
Export a type to a different ExprManager
const Options& CVC4::ExprManager::getOptions | ( | ) | const |
Get this node manager's options.
SExpr CVC4::ExprManager::getStatistic | ( | const std::string & | name | ) | const |
throw | ( | ||||
) |
Get a reference to the statistics registry for this ExprManager.
Statistics CVC4::ExprManager::getStatistics | ( | ) | const | |
throw | ( | |||
) |
Get a reference to the statistics registry for this ExprManager.
Type CVC4::ExprManager::getType | ( | Expr | e, |
bool | check = false |
||
) | |||
throw | ( | TypeCheckingException | |
) |
Get the type of an expression.
|
static |
Determine whether Exprs of a particular Kind have operators.
IntegerType CVC4::ExprManager::integerType | ( | ) | const |
Get the type for integers.
|
static |
Returns the maximum arity of the given kind.
|
static |
Returns the minimum arity of the given kind.
Make the type of arrays with the given parameterization.
Create an Expr by applying an associative operator to the children.
If children.size()
is greater than the max arity for kind
, then the expression will be broken up into suitably-sized chunks, taking advantage of the associativity of kind
. For example, if kind FOO
has max arity 2, then calling mkAssociative(FOO,a,b,c)
will return (FOO (FOO a b) c)
or (FOO a (FOO b c))
. The order of the arguments will be preserved in a left-to-right traversal of the resulting tree.
BitVectorType CVC4::ExprManager::mkBitVectorType | ( | unsigned | size | ) | const |
Make a type representing a bit-vector of the given size.
Create a new, fresh variable for use in a binder expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
It is an error for this bound variable to exist outside of a binder, and it should also only be used in a single binder expression. That is, two distinct FORALL expressions should use entirely disjoint sets of bound variables (however, a single FORALL expression can be used in multiple places in a formula without a problem). This newly-created bound variable is guaranteed to be distinct from every variable thus far in the ExprManager, even if it shares a name with another; this is to support any kind of scoping policy on top of ExprManager. The SymbolTable class can be used to store and lookup symbols by name, if desired.
name | a name to associate to the fresh new bound variable |
type | the type for the new bound variable |
Create a (nameless) new, fresh variable for use in a binder expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA).
It is an error for this bound variable to exist outside of a binder, and it should also only be used in a single binder expression. That is, two distinct FORALL expressions should use entirely disjoint sets of bound variables (however, a single FORALL expression can be used in multiple places in a formula without a problem). This newly-created bound variable is guaranteed to be distinct from every variable thus far in the ExprManager.
type | the type for the new bound variable |
Expr CVC4::ExprManager::mkConst | ( | const T & | ) |
Create a constant of type T.
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::UninterpretedConstant const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::AbstractValue const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Kind const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Chain const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::TypeConstant const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Predicate const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | bool const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Divisible const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::SubrangeBounds const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Rational const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorSize const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVector const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorBitOf const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorExtract const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorRepeat const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorZeroExtend const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorSignExtend const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorRotateLeft const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::BitVectorRotateRight const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::IntToBitVector const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::ArrayStoreAll const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Datatype const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::AscriptionType const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::TupleSelect const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::TupleUpdate const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::Record const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::RecordSelect const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::RecordUpdate const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::String const & | val | ) |
Expr CVC4::ExprManager::mkConst | ( | ::CVC4::RegExp const & | val | ) |
ConstructorType CVC4::ExprManager::mkConstructorType | ( | const DatatypeConstructor & | constructor, |
Type | range | ||
) | const |
Make a type representing a constructor with the given parameterization.
DatatypeType CVC4::ExprManager::mkDatatypeType | ( | const Datatype & | datatype | ) |
Make a type representing the given datatype.
Make a unary expression of a given kind (NOT, BVNOT, ...).
kind | the kind of expression |
child1 | kind the kind of expression |
Make a binary expression of a given kind (AND, PLUS, ...).
kind | the kind of expression |
child1 | the first child of the new expression |
child2 | the second child of the new expression |
Make a 3-ary expression of a given kind (AND, PLUS, ...).
kind | the kind of expression |
child1 | the first child of the new expression |
child2 | the second child of the new expression |
child3 | the third child of the new expression |
Make a 4-ary expression of a given kind (AND, PLUS, ...).
kind | the kind of expression |
child1 | the first child of the new expression |
child2 | the second child of the new expression |
child3 | the third child of the new expression |
child4 | the fourth child of the new expression |
Expr CVC4::ExprManager::mkExpr | ( | Kind | kind, |
Expr | child1, | ||
Expr | child2, | ||
Expr | child3, | ||
Expr | child4, | ||
Expr | child5 | ||
) |
Make a 5-ary expression of a given kind (AND, PLUS, ...).
kind | the kind of expression |
child1 | the first child of the new expression |
child2 | the second child of the new expression |
child3 | the third child of the new expression |
child4 | the fourth child of the new expression |
child5 | the fifth child of the new expression |
Make an n-ary expression of given kind given a vector of its children.
kind | the kind of expression to build |
children | the subexpressions |
Expr CVC4::ExprManager::mkExpr | ( | Kind | kind, |
Expr | child1, | ||
const std::vector< Expr > & | otherChildren | ||
) |
Make an n-ary expression of given kind given a first arg and a vector of its remaining children (this can be useful where the kind is parameterized operator, so the first arg is really an arg to the kind to construct an operator)
kind | the kind of expression to build |
child1 | the first subexpression |
otherChildren | the remaining subexpressions |
Make a nullary parameterized expression with the given operator.
opExpr | the operator expression |
Make a unary parameterized expression with the given operator.
opExpr | the operator expression |
child1 | the subexpression |
Make a binary parameterized expression with the given operator.
opExpr | the operator expression |
child1 | the first subexpression |
child2 | the second subexpression |
Make a ternary parameterized expression with the given operator.
opExpr | the operator expression |
child1 | the first subexpression |
child2 | the second subexpression |
child3 | the third subexpression |
Make a quaternary parameterized expression with the given operator.
opExpr | the operator expression |
child1 | the first subexpression |
child2 | the second subexpression |
child3 | the third subexpression |
child4 | the fourth subexpression |
Expr CVC4::ExprManager::mkExpr | ( | Expr | opExpr, |
Expr | child1, | ||
Expr | child2, | ||
Expr | child3, | ||
Expr | child4, | ||
Expr | child5 | ||
) |
Make a quinary parameterized expression with the given operator.
opExpr | the operator expression |
child1 | the first subexpression |
child2 | the second subexpression |
child3 | the third subexpression |
child4 | the fourth subexpression |
child5 | the fifth subexpression |
Make an n-ary expression of given operator to apply and a vector of its children.
opExpr | the operator expression |
children | the subexpressions |
FunctionType CVC4::ExprManager::mkFunctionType | ( | Type | domain, |
Type | range | ||
) |
Make a function type from domain to range.
FunctionType CVC4::ExprManager::mkFunctionType | ( | const std::vector< Type > & | argTypes, |
Type | range | ||
) |
Make a function type with input types from argTypes.
argTypes
must have at least one element.
FunctionType CVC4::ExprManager::mkFunctionType | ( | const std::vector< Type > & | sorts | ) |
Make a function type with input types from sorts[0..sorts.size()-2]
and result type sorts[sorts.size()-1]
.
sorts
must have at least 2 elements.
std::vector<DatatypeType> CVC4::ExprManager::mkMutualDatatypeTypes | ( | const std::vector< Datatype > & | datatypes | ) |
Make a set of types representing the given datatypes, which may be mutually recursive.
std::vector<DatatypeType> CVC4::ExprManager::mkMutualDatatypeTypes | ( | const std::vector< Datatype > & | datatypes, |
const std::set< Type > & | unresolvedTypes | ||
) |
Make a set of types representing the given datatypes, which may be mutually recursive.
unresolvedTypes is a set of SortTypes that were used as placeholders in the Datatypes for the Datatypes of the same name. This is just a more complicated version of the above mkMutualDatatypeTypes() function, but is required to handle complex types.
For example, unresolvedTypes might contain the single sort "list" (with that name reported from SortType::getName()). The datatypes list might have the single datatype
DATATYPE list = cons(car:ARRAY INT OF list, cdr:list) | nil; END;
To represent the Type of the array, the user had to create a placeholder type (an uninterpreted sort) to stand for "list" in the type of "car". It is this placeholder sort that should be passed in unresolvedTypes. If the datatype was of the simpler form:
DATATYPE list = cons(car:list, cdr:list) | nil; END;
then no complicated Type needs to be created, and the above, simpler form of mkMutualDatatypeTypes() is enough.
FunctionType CVC4::ExprManager::mkPredicateType | ( | const std::vector< Type > & | sorts | ) |
Make a predicate type with input types from sorts
.
The result with be a function type with range BOOLEAN
. sorts
must have at least one element.
RecordType CVC4::ExprManager::mkRecordType | ( | const Record & | rec | ) |
Make a record type with types from the rec parameter.
SelectorType CVC4::ExprManager::mkSelectorType | ( | Type | domain, |
Type | range | ||
) | const |
Make a type representing a selector with the given parameterization.
Make a symbolic expressiontype with types from types[0..types.size()-1]
.
types
may have any number of elements.
SortType CVC4::ExprManager::mkSort | ( | const std::string & | name, |
uint32_t | flags = SORT_FLAG_NONE |
||
) | const |
Make a new sort with the given name.
SortConstructorType CVC4::ExprManager::mkSortConstructor | ( | const std::string & | name, |
size_t | arity | ||
) | const |
Make a sort constructor from a name and arity.
Type CVC4::ExprManager::mkSubrangeType | ( | const SubrangeBounds & | bounds | ) | |
throw | ( | TypeCheckingException | |||
) |
Make a predicate subtype type defined by the given LAMBDA expression.
A TypeCheckingException can be thrown if lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that the resulting predicate subtype is inhabited. Make a predicate subtype type defined by the given LAMBDA expression and whose non-emptiness is witnessed by the given witness. A TypeCheckingException can be thrown if lambda is not a LAMBDA, or is ill-typed, or if the witness is not a witness or ill-typed. Make an integer subrange type as defined by the argument.
TesterType CVC4::ExprManager::mkTesterType | ( | Type | domain | ) | const |
Make a type representing a tester with the given parameterization.
Make a tuple type with types from types[0..types.size()-1]
.
types
must have at least one element.
Expr CVC4::ExprManager::mkVar | ( | const std::string & | name, |
Type | type, | ||
uint32_t | flags = VAR_FLAG_NONE |
||
) |
Create a new, fresh variable.
This variable is guaranteed to be distinct from every variable thus far in the ExprManager, even if it shares a name with another; this is to support any kind of scoping policy on top of ExprManager. The SymbolTable class can be used to store and lookup symbols by name, if desired.
name | a name to associate to the fresh new variable |
type | the type for the new variable |
flags | - VAR_FLAG_NONE - no flags; VAR_FLAG_GLOBAL - whether this variable is to be considered "global" or not. Note that this information isn't used by the ExprManager, but is passed on to the ExprManager's event subscribers like the model-building service; if isGlobal is true, this newly-created variable will still available in models generated after an intervening pop. VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for use with SmtEngine::defineFunction(). This keeps a declaration from being emitted in API dumps (since a subsequent definition is expected to be dumped instead). |
Expr CVC4::ExprManager::mkVar | ( | Type | type, |
uint32_t | flags = VAR_FLAG_NONE |
||
) |
Create a (nameless) new, fresh variable.
This variable is guaranteed to be distinct from every variable thus far in the ExprManager.
type | the type for the new variable |
flags | - VAR_FLAG_GLOBAL - whether this variable is to be considered "global" or not. Note that this information isn't used by the ExprManager, but is passed on to the ExprManager's event subscribers like the model-building service; if isGlobal is true, this newly-created variable will still available in models generated after an intervening pop. |
Get the (singleton) operator of an OPERATOR-kinded kind.
The returned Expr e will have kind BUILTIN, and calling e.getConst<CVC4::Kind>() will yield k.
RealType CVC4::ExprManager::realType | ( | ) | const |
Get the type for reals.
StringType CVC4::ExprManager::stringType | ( | ) | const |
Get the type for strings.
|
friend |
Statistics reach in to get the StatisticsRegistry.
|
friend |
ExprManagerScope reaches in to get the NodeManager.
Definition at line 159 of file expr_manager.h.
|
friend |
NodeManager reaches in to get the NodeManager.
Definition at line 162 of file expr_manager.h.
|
friend |
SmtEngine will use all the internals, so it will grab the NodeManager.
Definition at line 156 of file expr_manager.h.