cvc4-1.4
CVC3::ExprManager Class Reference

#include <cvc3_compat.h>

Inheritance diagram for CVC3::ExprManager:
CVC4::ExprManager

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

std::string getKindName (int kind)
 
InputLanguage getInputLang () const
 Get the input language for printing. More...
 
InputLanguage getOutputLang () const
 Get the output language for printing. 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...
 
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::EmptySet const &val)
 
template<>
Expr mkConst (::CVC4::String const &val)
 
template<>
Expr mkConst (::CVC4::RegExp const &val)
 
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...
 
SetType mkSetType (Type elementType) const
 Make the type of set 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...
 

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...
 

Detailed Description

Definition at line 453 of file cvc3_compat.h.

Member Enumeration Documentation

◆ anonymous enum

anonymous enum
inherited

Bits for use in mkSort() flags.

Enumerator
SORT_FLAG_NONE 
SORT_FLAG_PLACEHOLDER 

Definition at line 498 of file expr_manager.h.

◆ anonymous enum

anonymous enum
inherited

Bits for use in mkVar() flags.

Enumerator
VAR_FLAG_NONE 
VAR_FLAG_GLOBAL 
VAR_FLAG_DEFINED 

Definition at line 542 of file expr_manager.h.

Member Function Documentation

◆ booleanType()

BooleanType CVC4::ExprManager::booleanType ( ) const
inherited

Get the type for booleans.

◆ exportType()

static Type CVC4::ExprManager::exportType ( const Type t,
ExprManager em,
ExprManagerMapCollection vmap 
)
staticinherited

Export an expr to a different ExprManager.

Export a type to a different ExprManager

◆ getInputLang()

InputLanguage CVC3::ExprManager::getInputLang ( ) const

Get the input language for printing.

◆ getKindName()

std::string CVC3::ExprManager::getKindName ( int  kind)

◆ getOptions()

const Options& CVC4::ExprManager::getOptions ( ) const
inherited

Get this node manager's options.

◆ getOutputLang()

InputLanguage CVC3::ExprManager::getOutputLang ( ) const

Get the output language for printing.

◆ getStatistic()

SExpr CVC4::ExprManager::getStatistic ( const std::string &  name) const
throw (
)
inherited

Get a reference to the statistics registry for this ExprManager.

◆ getStatistics()

Statistics CVC4::ExprManager::getStatistics ( ) const
throw (
)
inherited

Get a reference to the statistics registry for this ExprManager.

◆ getType()

Type CVC4::ExprManager::getType ( Expr  e,
bool  check = false 
)
throw (TypeCheckingException
)
inherited

Get the type of an expression.

◆ hasOperator()

static bool CVC4::ExprManager::hasOperator ( Kind  k)
staticinherited

Determine whether Exprs of a particular Kind have operators.

Returns
true if Exprs of Kind k have operators.

◆ integerType()

IntegerType CVC4::ExprManager::integerType ( ) const
inherited

Get the type for integers.

◆ maxArity()

static unsigned CVC4::ExprManager::maxArity ( Kind  kind)
staticinherited

Returns the maximum arity of the given kind.

◆ minArity()

static unsigned CVC4::ExprManager::minArity ( Kind  kind)
staticinherited

Returns the minimum arity of the given kind.

◆ mkArrayType()

ArrayType CVC4::ExprManager::mkArrayType ( Type  indexType,
Type  constituentType 
) const
inherited

Make the type of arrays with the given parameterization.

◆ mkAssociative()

Expr CVC4::ExprManager::mkAssociative ( Kind  kind,
const std::vector< Expr > &  children 
)
inherited

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.

◆ mkBitVectorType()

BitVectorType CVC4::ExprManager::mkBitVectorType ( unsigned  size) const
inherited

Make a type representing a bit-vector of the given size.

◆ mkBoundVar() [1/2]

Expr CVC4::ExprManager::mkBoundVar ( const std::string &  name,
Type  type 
)
inherited

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.

Parameters
namea name to associate to the fresh new bound variable
typethe type for the new bound variable

◆ mkBoundVar() [2/2]

Expr CVC4::ExprManager::mkBoundVar ( Type  type)
inherited

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.

Parameters
typethe type for the new bound variable

◆ mkConst() [1/32]

template<class T >
Expr CVC4::ExprManager::mkConst ( const T &  )
inherited

Create a constant of type T.

◆ mkConst() [2/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::UninterpretedConstant const &  val)
inherited

◆ mkConst() [3/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::AbstractValue const &  val)
inherited

◆ mkConst() [4/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Kind const &  val)
inherited

◆ mkConst() [5/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Chain const &  val)
inherited

◆ mkConst() [6/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::TypeConstant const &  val)
inherited

◆ mkConst() [7/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Predicate const &  val)
inherited

◆ mkConst() [8/32]

template<>
Expr CVC4::ExprManager::mkConst ( bool const &  val)
inherited

◆ mkConst() [9/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Divisible const &  val)
inherited

◆ mkConst() [10/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::SubrangeBounds const &  val)
inherited

◆ mkConst() [11/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Rational const &  val)
inherited

◆ mkConst() [12/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorSize const &  val)
inherited

◆ mkConst() [13/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVector const &  val)
inherited

◆ mkConst() [14/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorBitOf const &  val)
inherited

◆ mkConst() [15/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorExtract const &  val)
inherited

◆ mkConst() [16/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorRepeat const &  val)
inherited

◆ mkConst() [17/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorZeroExtend const &  val)
inherited

◆ mkConst() [18/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorSignExtend const &  val)
inherited

◆ mkConst() [19/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorRotateLeft const &  val)
inherited

◆ mkConst() [20/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::BitVectorRotateRight const &  val)
inherited

◆ mkConst() [21/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::IntToBitVector const &  val)
inherited

◆ mkConst() [22/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::ArrayStoreAll const &  val)
inherited

◆ mkConst() [23/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Datatype const &  val)
inherited

◆ mkConst() [24/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::AscriptionType const &  val)
inherited

◆ mkConst() [25/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::TupleSelect const &  val)
inherited

◆ mkConst() [26/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::TupleUpdate const &  val)
inherited

◆ mkConst() [27/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::Record const &  val)
inherited

◆ mkConst() [28/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::RecordSelect const &  val)
inherited

◆ mkConst() [29/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::RecordUpdate const &  val)
inherited

◆ mkConst() [30/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::EmptySet const &  val)
inherited

◆ mkConst() [31/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::String const &  val)
inherited

◆ mkConst() [32/32]

template<>
Expr CVC4::ExprManager::mkConst ( ::CVC4::RegExp const &  val)
inherited

◆ mkConstructorType()

ConstructorType CVC4::ExprManager::mkConstructorType ( const DatatypeConstructor constructor,
Type  range 
) const
inherited

Make a type representing a constructor with the given parameterization.

◆ mkDatatypeType()

DatatypeType CVC4::ExprManager::mkDatatypeType ( const Datatype datatype)
inherited

Make a type representing the given datatype.

◆ mkExpr() [1/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
Expr  child1 
)
inherited

Make a unary expression of a given kind (NOT, BVNOT, ...).

Parameters
kindthe kind of expression
child1kind the kind of expression
Returns
the expression

◆ mkExpr() [2/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
Expr  child1,
Expr  child2 
)
inherited

Make a binary expression of a given kind (AND, PLUS, ...).

Parameters
kindthe kind of expression
child1the first child of the new expression
child2the second child of the new expression
Returns
the expression

◆ mkExpr() [3/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
Expr  child1,
Expr  child2,
Expr  child3 
)
inherited

Make a 3-ary expression of a given kind (AND, PLUS, ...).

Parameters
kindthe kind of expression
child1the first child of the new expression
child2the second child of the new expression
child3the third child of the new expression
Returns
the expression

◆ mkExpr() [4/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
Expr  child1,
Expr  child2,
Expr  child3,
Expr  child4 
)
inherited

Make a 4-ary expression of a given kind (AND, PLUS, ...).

Parameters
kindthe kind of expression
child1the first child of the new expression
child2the second child of the new expression
child3the third child of the new expression
child4the fourth child of the new expression
Returns
the expression

◆ mkExpr() [5/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
Expr  child1,
Expr  child2,
Expr  child3,
Expr  child4,
Expr  child5 
)
inherited

Make a 5-ary expression of a given kind (AND, PLUS, ...).

Parameters
kindthe kind of expression
child1the first child of the new expression
child2the second child of the new expression
child3the third child of the new expression
child4the fourth child of the new expression
child5the fifth child of the new expression
Returns
the expression

◆ mkExpr() [6/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
const std::vector< Expr > &  children 
)
inherited

Make an n-ary expression of given kind given a vector of its children.

Parameters
kindthe kind of expression to build
childrenthe subexpressions
Returns
the n-ary expression

◆ mkExpr() [7/14]

Expr CVC4::ExprManager::mkExpr ( Kind  kind,
Expr  child1,
const std::vector< Expr > &  otherChildren 
)
inherited

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)

Parameters
kindthe kind of expression to build
child1the first subexpression
otherChildrenthe remaining subexpressions
Returns
the n-ary expression

◆ mkExpr() [8/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr)
inherited

Make a nullary parameterized expression with the given operator.

Parameters
opExprthe operator expression
Returns
the nullary expression

◆ mkExpr() [9/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr,
Expr  child1 
)
inherited

Make a unary parameterized expression with the given operator.

Parameters
opExprthe operator expression
child1the subexpression
Returns
the unary expression

◆ mkExpr() [10/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr,
Expr  child1,
Expr  child2 
)
inherited

Make a binary parameterized expression with the given operator.

Parameters
opExprthe operator expression
child1the first subexpression
child2the second subexpression
Returns
the binary expression

◆ mkExpr() [11/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr,
Expr  child1,
Expr  child2,
Expr  child3 
)
inherited

Make a ternary parameterized expression with the given operator.

Parameters
opExprthe operator expression
child1the first subexpression
child2the second subexpression
child3the third subexpression
Returns
the ternary expression

◆ mkExpr() [12/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr,
Expr  child1,
Expr  child2,
Expr  child3,
Expr  child4 
)
inherited

Make a quaternary parameterized expression with the given operator.

Parameters
opExprthe operator expression
child1the first subexpression
child2the second subexpression
child3the third subexpression
child4the fourth subexpression
Returns
the quaternary expression

◆ mkExpr() [13/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr,
Expr  child1,
Expr  child2,
Expr  child3,
Expr  child4,
Expr  child5 
)
inherited

Make a quinary parameterized expression with the given operator.

Parameters
opExprthe operator expression
child1the first subexpression
child2the second subexpression
child3the third subexpression
child4the fourth subexpression
child5the fifth subexpression
Returns
the quinary expression

◆ mkExpr() [14/14]

Expr CVC4::ExprManager::mkExpr ( Expr  opExpr,
const std::vector< Expr > &  children 
)
inherited

Make an n-ary expression of given operator to apply and a vector of its children.

Parameters
opExprthe operator expression
childrenthe subexpressions
Returns
the n-ary expression

◆ mkFunctionType() [1/3]

FunctionType CVC4::ExprManager::mkFunctionType ( Type  domain,
Type  range 
)
inherited

Make a function type from domain to range.

◆ mkFunctionType() [2/3]

FunctionType CVC4::ExprManager::mkFunctionType ( const std::vector< Type > &  argTypes,
Type  range 
)
inherited

Make a function type with input types from argTypes.

argTypes must have at least one element.

◆ mkFunctionType() [3/3]

FunctionType CVC4::ExprManager::mkFunctionType ( const std::vector< Type > &  sorts)
inherited

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.

◆ mkMutualDatatypeTypes() [1/2]

std::vector<DatatypeType> CVC4::ExprManager::mkMutualDatatypeTypes ( const std::vector< Datatype > &  datatypes)
inherited

Make a set of types representing the given datatypes, which may be mutually recursive.

◆ mkMutualDatatypeTypes() [2/2]

std::vector<DatatypeType> CVC4::ExprManager::mkMutualDatatypeTypes ( const std::vector< Datatype > &  datatypes,
const std::set< Type > &  unresolvedTypes 
)
inherited

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.

◆ mkPredicateType()

FunctionType CVC4::ExprManager::mkPredicateType ( const std::vector< Type > &  sorts)
inherited

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.

◆ mkRecordType()

RecordType CVC4::ExprManager::mkRecordType ( const Record rec)
inherited

Make a record type with types from the rec parameter.

◆ mkSelectorType()

SelectorType CVC4::ExprManager::mkSelectorType ( Type  domain,
Type  range 
) const
inherited

Make a type representing a selector with the given parameterization.

◆ mkSetType()

SetType CVC4::ExprManager::mkSetType ( Type  elementType) const
inherited

Make the type of set with the given parameterization.

◆ mkSExprType()

SExprType CVC4::ExprManager::mkSExprType ( const std::vector< Type > &  types)
inherited

Make a symbolic expressiontype with types from types[0..types.size()-1].

types may have any number of elements.

◆ mkSort()

SortType CVC4::ExprManager::mkSort ( const std::string &  name,
uint32_t  flags = SORT_FLAG_NONE 
) const
inherited

Make a new sort with the given name.

◆ mkSortConstructor()

SortConstructorType CVC4::ExprManager::mkSortConstructor ( const std::string &  name,
size_t  arity 
) const
inherited

Make a sort constructor from a name and arity.

◆ mkSubrangeType()

Type CVC4::ExprManager::mkSubrangeType ( const SubrangeBounds bounds)
throw (TypeCheckingException
)
inherited

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.

◆ mkTesterType()

TesterType CVC4::ExprManager::mkTesterType ( Type  domain) const
inherited

Make a type representing a tester with the given parameterization.

◆ mkTupleType()

TupleType CVC4::ExprManager::mkTupleType ( const std::vector< Type > &  types)
inherited

Make a tuple type with types from types[0..types.size()-1].

types must have at least one element.

◆ mkVar() [1/2]

Expr CVC4::ExprManager::mkVar ( const std::string &  name,
Type  type,
uint32_t  flags = VAR_FLAG_NONE 
)
inherited

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.

Parameters
namea name to associate to the fresh new variable
typethe 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).

◆ mkVar() [2/2]

Expr CVC4::ExprManager::mkVar ( Type  type,
uint32_t  flags = VAR_FLAG_NONE 
)
inherited

Create a (nameless) new, fresh variable.

This variable is guaranteed to be distinct from every variable thus far in the ExprManager.

Parameters
typethe 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.

◆ operatorOf()

Expr CVC4::ExprManager::operatorOf ( Kind  k)
inherited

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()

RealType CVC4::ExprManager::realType ( ) const
inherited

Get the type for reals.

◆ stringType()

StringType CVC4::ExprManager::stringType ( ) const
inherited

Get the type for strings.


The documentation for this class was generated from the following file: