Term 

The Term class represents arbitrary expressions that are Boolean or from some of the supported theories. The list of all supported types (or kinds) is given by the Kind enum. The Term class provides methods for general inspection (e.g., comparison, retrieve the kind and sort, access sub-terms), but also methods to retrieving constant values for the supported theories (i.e., is<Type>Value() and get<Type>Value() , which returns the constant values in the best type standard C++ offers).

Additionally, a Term can be hashed (using std::hash<cvc5::Term> ) and given to output streams, including terms within standard containers like std::map , std::set , or std::vector .

The Term only offers the default constructor to create a null term. Instead, the Solver class provides factory functions for all other terms, e.g., Solver::mkTerm() for generic terms and Solver::mk<Type>() for constant values of a given type.

class Term 

A cvc5 Term .

Public Functions

Term ( ) : Constructor for a null term.

~Term ( ) : Destructor.

bool operator == ( const Term & t ) const 

Syntactic equality operator. Return true if both terms are syntactically identical.

Note

Both terms must belong to the same node manager.

Parameters :: t – The term to compare to for equality.
Returns :: True if the terms are equal.

bool operator != ( const Term & t ) const 

Syntactic disequality operator. Return true if both terms differ syntactically.

Note

Both terms must belong to the same node manager.

Parameters :: t – The term to compare to for disequality.
Returns :: True if terms are disequal.

bool operator < ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is less than t.

bool operator > ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is greater than t.

bool operator <= ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is less than or equal to t.

bool operator >= ( const Term & t ) const 

Comparison for ordering on terms by their id.

Parameters :: t – The term to compare to.
Returns :: True if this term is greater than or equal to t.

size_t getNumChildren ( ) const 

Returns :: The number of children of this term

Term operator [] ( size_t index ) const 

Get the child term at a given index.

Parameters :: index – The index of the child term to return.
Returns :: The child term with the given index.

uint64_t getId ( ) const 

Returns :: The id of this term.

Kind getKind ( ) const 

Returns :: The kind of this term.

Sort getSort ( ) const 

Returns :: The sort of this term.

Term substitute ( const Term & term , const Term & replacement ) const 

Replace term with replacement in this term.

Note

This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).

Returns :: The result of replacing term with replacement in this term.

Term substitute ( const std :: vector < Term > & terms , const std :: vector < Term > & replacements ) const 

Simultaneously replace terms with replacements in this term.

In the case that terms contains duplicates, the replacement earliest in the vector takes priority. For example, calling substitute on f(x,y) with terms = { x, z } , replacements = { g(z), w } results in the term f(g(z),y) .

Note

This replacement is applied during a pre-order traversal and only once (it is not run until fixed point).

Returns :: The result of simultaneously replacing terms with replacements in this term.

bool hasOp ( ) const 

Returns :: True iff this term has an operator.

Op getOp ( ) const 

Note

This is safe to call when hasOp() returns true.

Returns :: The Op used to create this term.

bool hasSymbol ( ) const 

Does the term have a symbol, i.e., a name?

For example, free constants and variables have symbols.

Returns :: True if the term has a symbol.

std :: string getSymbol ( ) const 

Get the symbol of this Term .

The symbol of the term is the string that was provided when constructing it via Solver::mkConst() or Solver::mkVar() .

Note

Asserts hasSymbol() .

Returns :: The raw symbol of the term.

bool isNull ( ) const 

Returns :: True if this Term is a null term.

Term notTerm ( ) const 

Boolean negation.

Returns :: The Boolean negation of this term.

Term andTerm ( const Term & t ) const 

Boolean and.

Parameters :: t – A Boolean term.
Returns :: The conjunction of this term and the given term.

Term orTerm ( const Term & t ) const 

Boolean or.

Parameters :: t – A Boolean term.
Returns :: The disjunction of this term and the given term.

Term xorTerm ( const Term & t ) const 

Boolean exclusive or.

Parameters :: t – A Boolean term.
Returns :: The exclusive disjunction of this term and the given term.

Term eqTerm ( const Term & t ) const 

Equality.

Parameters :: t – A Boolean term.
Returns :: The Boolean equivalence of this term and the given term.

Term impTerm ( const Term & t ) const 

Boolean implication.

Parameters :: t – A Boolean term.
Returns :: The implication of this term and the given term.

Term iteTerm ( const Term & then_t , const Term & else_t ) const 

If-then-else with this term as the Boolean condition.

Parameters :

then_t – The ‘then’ term.
else_t – The ‘else’ term.

Returns :

The if-then-else term with this term as the Boolean condition.

std :: string toString ( ) const 

Returns :: A string representation of this term.

const_iterator begin ( ) const 

Returns :: An iterator to the first child of this Term .

const_iterator end ( ) const 

Returns :: An iterator to one-off-the-last child of this Term .

int32_t getRealOrIntegerValueSign ( ) const 

Get integer or real value sign. Must be called on integer or real values, or otherwise an exception is thrown.

Returns :: 0 if this term is zero, -1 if this term is a negative real or integer value, 1 if this term is a positive real or integer value.

bool isInt32Value ( ) const 

Returns :: True if the term is an integer value that fits within int32_t. Note that this method will return true for integer constants and real constants that have integer value.

int32_t getInt32Value ( ) const 

Get the int32_t representation of this integral value.

Note

Asserts isInt32Value() .

Returns :: This integer value as a int32_t .

bool isUInt32Value ( ) const 

Returns :: True if the term is an integer value that fits within uint32_t. Note that this method will return true for integer constants and real constants that have integral value.

uint32_t getUInt32Value ( ) const 

Get the uint32_t representation of this integral value.

Note

Asserts isUInt32Value() .

Returns :: This integer value as a uint32_t .

bool isInt64Value ( ) const 

Returns :: True if the term is an integer value that fits within int64_t. Note that this method will return true for integer constants and real constants that have integral value.

int64_t getInt64Value ( ) const 

Get the int64_t representation of this integral value.

Note

Asserts isInt64Value() .

Returns :: This integer value as a int64_t .

bool isUInt64Value ( ) const 

Returns :: True if the term is an integer value that fits within uint64_t. Note that this method will return true for integer constants and real constants that have integral value.

uint64_t getUInt64Value ( ) const 

Get the uint64_t representation of this integral value.

Note

Asserts isUInt64Value() .

Returns :: This integer value as a uint64_t .

bool isIntegerValue ( ) const 

Returns :: True if the term is an integer constant or a real constant that has an integral value.

std :: string getIntegerValue ( ) const 

Note

Asserts isIntegerValue() .

Returns :: The integral term in (decimal) string representation.

bool isStringValue ( ) const 

Returns :: True if the term is a string value.

std :: wstring getStringValue ( ) const 

Note

Asserts isStringValue() .

Note

This method is not to be confused with toString() , which returns some string representation of the term, whatever data it may hold.

Returns :: The string term as a native string value.

bool isReal32Value ( ) const 

Returns :: True if the term is a rational value whose numerator and denominator fit within int32_t and uint32_t, respectively.

std :: pair < int32_t , uint32_t > getReal32Value ( ) const 

Note

Asserts isReal32Value() .

Returns :: The representation of a rational value as a pair of its numerator and denominator.

bool isReal64Value ( ) const 

Returns :: True if the term is a rational value whose numerator and denominator fit within int64_t and uint64_t, respectively.

std :: pair < int64_t , uint64_t > getReal64Value ( ) const 

Note

Asserts isReal64Value() .

Returns :: The representation of a rational value as a pair of its numerator and denominator.

bool isRealValue ( ) const 

Note

A term of kind PI is not considered to be a real value.

Returns :: True if the term is a rational value.

std :: string getRealValue ( ) const 

Note

Asserts isRealValue() .

Returns :: The representation of a rational value as a (rational) string.

bool isConstArray ( ) const 

Returns :: True if the term is a constant array.

Term getConstArrayBase ( ) const 

Note

Asserts isConstArray() .

Returns :: The base (element stored at all indices) of a constant array.

bool isBooleanValue ( ) const 

Returns :: True if the term is a Boolean value.

bool getBooleanValue ( ) const 

Note

Asserts isBooleanValue() .

Returns :: The representation of a Boolean value as a native Boolean value.

bool isBitVectorValue ( ) const 

Returns :: True if the term is a bit-vector value.

std :: string getBitVectorValue ( uint32_t base = 2 ) const 

Get the string representation of a bit-vector value.

Supported values for base are 2 (bit string), 10 (decimal string) or 16 (hexadecimal string).

Note

Asserts isBitVectorValue() .

Returns :: The string representation of a bit-vector value.

bool isFiniteFieldValue ( ) const 

Returns :: True if the term is a finite field value.

std :: string getFiniteFieldValue ( ) const 

Get the string representation of a finite field value (base 10).

Note

Asserts isFiniteFieldValue() .

Note

Uses the integer representative of smallest absolute value.

Returns :: The string representation of the integer representation of this finite field value.

bool isUninterpretedSortValue ( ) const 

Returns :: True if the term is an abstract value.

std :: string getUninterpretedSortValue ( ) const 

Note

Asserts isUninterpretedSortValue() .

Returns :: The representation of an uninterpreted sort value as a string.

bool isTupleValue ( ) const 

Returns :: True if the term is a tuple value.

std :: vector < Term > getTupleValue ( ) const 

Note

Asserts isTupleValue() .

Returns :: The representation of a tuple value as a vector of terms.

bool isRoundingModeValue ( ) const 

Returns :: True if the term is a floating-point rounding mode value.

RoundingMode getRoundingModeValue ( ) const 

Note

Asserts isRoundingModeValue() .

Returns :: The floating-point rounding mode value held by the term.

bool isFloatingPointPosZero ( ) const 

Returns :: True if the term is the floating-point value for positive zero.

bool isFloatingPointNegZero ( ) const 

Returns :: True if the term is the floating-point value for negative zero.

bool isFloatingPointPosInf ( ) const 

Returns :: True if the term is the floating-point value for positive. infinity.

bool isFloatingPointNegInf ( ) const 

Returns :: True if the term is the floating-point value for negative. infinity.

bool isFloatingPointNaN ( ) const 

Returns :: True if the term is the floating-point value for not a number.

bool isFloatingPointValue ( ) const 

Returns :: True if the term is a floating-point value.

std :: tuple < uint32_t , uint32_t , Term > getFloatingPointValue ( ) const 

Note

Asserts isFloatingPointValue() .

Returns :: The representation of a floating-point value as a tuple of the exponent width, the significand width and a bit-vector value.

bool isSetValue ( ) const 

A term is a set value if it is considered to be a (canonical) constant set value. A canonical set value is one whose AST is:

                (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))

               

where \(c_1 ... c_n\) are values ordered by id such that \(c_1 > ... > c_n\) (see Term::operator>(const Term&) const ).

Note

A universe set term (kind SET_UNIVERSE ) is not considered to be a set value.

Returns :: True if the term is a set value.

std :: set < Term > getSetValue ( ) const 

Note

Asserts isSetValue() .

Returns :: The representation of a set value as a set of terms.

bool isSequenceValue ( ) const 

Determine if this term is a sequence value.

A term is a sequence value if it has kind CONST_SEQUENCE . In contrast to values for the set sort (as described in isSetValue() ), a sequence value is represented as a Term with no children.

Semantically, a sequence value is a concatenation of unit sequences whose elements are themselves values. For example:

                (seq.++ (seq.unit 0) (seq.unit 1))

               

The above term has two representations in Term . One is as the sequence concatenation term:

                (SEQ_CONCAT (SEQ_UNIT 0) (SEQ_UNIT 1))

               

where 0 and 1 are the terms corresponding to the integer constants 0 and 1.

Alternatively, the above term is represented as the constant sequence value:

CONST_SEQUENCE_{0,1}

where calling getSequenceValue() on the latter returns the vector {0, 1} .

The former term is not a sequence value, but the latter term is.

Constant sequences cannot be constructed directly via the API. They are returned in response to API calls such Solver::getValue() and Solver::simplify() .

Returns :: True if the term is a sequence value.

std :: vector < Term > getSequenceValue ( ) const 

Note

Asserts isSequenceValue() .

Returns :: The representation of a sequence value as a vector of terms.

bool isCardinalityConstraint ( ) const 

Returns :: True if the term is a cardinality constraint.

std :: pair < Sort , uint32_t > getCardinalityConstraint ( ) const 

Note

Asserts isCardinalityConstraint() .

Returns :: The sort the cardinality constraint is for and its upper bound.

bool isRealAlgebraicNumber ( ) const 

Returns :: True if the term is a real algebraic number.

Term getRealAlgebraicNumberDefiningPolynomial ( const Term & v ) const 

Note

Asserts isRealAlgebraicNumber() .

Parameters :: v – The variable over which to express the polynomial.
Returns :: The defining polynomial for the real algebraic number, expressed in terms of the given variable.

Term getRealAlgebraicNumberLowerBound ( ) const 

Note

Asserts isRealAlgebraicNumber() .

Returns :: The lower bound for the value of the real algebraic number.

Term getRealAlgebraicNumberUpperBound ( ) const 

Note

Asserts isRealAlgebraicNumber() .

Returns :: The upper bound for the value of the real algebraic number.

Friends

friend class parser::Command

friend struct std::hash< Term >

class const_iterator 

Iterator for the children of a Term .

Note

This treats uninterpreted functions as Term just like any other term for example, the term f(x, y) will have Kind APPLY_UF and three children: f , x , and y

Public Types

using iterator_category = std :: forward_iterator_tag : Iterator tag

using value_type = Term : The type of the item

using pointer = const Term * : The pointer type of the item

using reference = const Term & : The reference type of the item

using difference_type = std :: ptrdiff_t : The type returned when two iterators are subtracted

Public Functions

const_iterator ( ) : Null Constructor.

const_iterator ( internal :: NodeManager * nm , const std :: shared_ptr < internal :: Node > & e , uint32_t p ) 

Constructor

Parameters :

nm – The associated node manager.
e – A std::shared pointer to the node that we’re iterating over.
p – The position of the iterator (e.g. which child it’s on).

const_iterator ( const const_iterator & it ) : Copy constructor.

const_iterator & operator = ( const const_iterator & it ) 

Assignment operator.

Parameters :: it – The iterator to assign to.
Returns :: The reference to the iterator after assignment.

bool operator == ( const const_iterator & it ) const 

Equality operator.

Parameters :: it – The iterator to compare to for equality.
Returns :: True if the iterators are equal.

bool operator != ( const const_iterator & it ) const 

Disequality operator.

Parameters :: it – The iterator to compare to for disequality.
Returns :: True if the iterators are disequal.

const_iterator & operator ++ ( ) 

Increment operator (prefix).

Returns :: A reference to the iterator after incrementing by one.

const_iterator operator ++ ( int ) 

Increment operator (postfix).

Returns :: A reference to the iterator after incrementing by one.

Term operator * ( ) const 

Dereference operator.

Returns :: The term this iterator points to.

template < > struct hash < cvc5 :: Term > 

Hash function for Terms.

Public Functions

size_t operator () ( const cvc5 :: Term & t ) const 