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 cvc5 :: 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. Both terms must belong to the same solver object.

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. Both terms must belong to the same solver object.

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.

int32_t getInt32Value ( ) const

Get the int32_t representation of this integer 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.

uint32_t getUInt32Value ( ) const

Get the uint32_t representation of this integer 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.

int64_t getInt64Value ( ) const

Get the int64_t representation of this integer 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.

uint64_t getUInt64Value ( ) const

Get the uint64_t representation of this integer value.

Note

Asserts isUInt64Value() .

Returns

This integer value as a uint64_t .

bool isIntegerValue ( ) const
Returns

True if the term is an integer value.

std :: string getIntegerValue ( ) const

Note

Asserts isIntegerValue() .

Returns

The integer 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 isUninterpretedSortValue ( ) const
Returns

True if the term is an abstract value.

std :: string getUninterpretedSortValue ( ) const
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
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
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
Returns

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

Friends

friend class cvc5::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 ( const Solver * slv , const std :: shared_ptr < internal :: Node > & e , uint32_t p )

Constructor

Parameters
  • slv – The associated solver object.

  • 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 std :: hash < cvc5 :: Term >

Hash function for Terms.

Public Functions

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