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.

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.

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

Get the number of children of this term.

Returns:

The number of children of this term.

Term operator[](size_t index) const

Get the child term of this term at a given index.

Parameters:

index – The index of the child.

Returns:

The child term at the given index.

uint64_t getId() const

Get the id of this term.

Returns:

The id of this term.

Kind getKind() const

Get the kind of this term.

Returns:

The kind of this term.

Sort getSort() const

Get the sort of this term.

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

Parameters:

  • term – The term to replace.

  • replacement – The term to replace it with.

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

Requires that terms and replacements are of equal size (they are interpreted as 1 : 1 mapping).

Note

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

Parameters:

  • terms – The terms to replace.

  • replacements – The replacement terms.

Returns:

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

bool hasOp() const

Determine if this term has an operator.

Returns:

True iff this term has an operator.

Op getOp() const

Get the operator of a term with an operator.

Note

Requires that this term has an operator (see hasOp()).

Returns:

The Op used to create this term.

bool hasSymbol() const

Determine if this term has a symbol (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 TermManager::mkConst() or TermManager::mkVar().

Note

Requires that this term has a symbol (see hasSymbol()).

Returns:

The raw symbol of the term.

bool isNull() const

Determine if this term is nullary.

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:

A Boolean term representing 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 &t, const Term &e) const

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

Parameters:

  • t – The ‘then’ term.

  • e – 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 the sign of an integer or real value.

Note

Requires that this term is an integer or real value.

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

Determine if this term is an int32 value.

Note

This will return true for integer constants and real constants that have integer value.

Returns:

True if the term is an integral value that fits within int32_t.

int32_t getInt32Value() const

Get the int32_t representation of this integral value.

Note

Requires that this term is an int32 value (see isInt32Value()).

Returns:

This integral value as int32_t value.

bool isUInt32Value() const

Determine if this term is a uint32 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns:

True if the term is an integral value and fits within uint32_t.

uint32_t getUInt32Value() const

Get the uint32_t representation of this integral value.

Note

Requires that this term is a uint32 value (see isUInt32Value()).

Returns:

This integral value as a uint32_t.

bool isInt64Value() const

Determine if this term is an int64 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns:

True if the term is an integral value and fits within int64_t.

int64_t getInt64Value() const

Get the int64_t representation of this integral value.

Note

Requires that this term is an int64 value (see isInt64Value()).

Returns:

This integral value as a int64_t.

bool isUInt64Value() const

Determine if this term is a uint64 value.

Note

This will return true for integer constants and real constants that have integral value.

Returns:

True if the term is an integral value that fits within uint64_t.

uint64_t getUInt64Value() const

Get the uint64_t representation of this integral value.

Note

Requires that this term is an uint64 value (see isUInt64Value()).

Returns:

This integral value as a uint64_t.

bool isIntegerValue() const

Determine if this term is an integral value.

Returns:

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

std::string getIntegerValue() const

Get a string representation of this integral value.

Note

Requires that this term is an integral value (see isIntegerValue()).

Returns:

The integral term in (decimal) string representation.

bool isStringValue() const

Determine if this term is a string value.

Returns:

True if the term is a string value.

std::wstring getStringValue() const

Get the native string representation of a string value.

Note

Requires that this term is a string value (see isStringValue()).

Note

This 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

Determine if this term is a rational value whose numerator fits into an int32 value and its denominator fits into a uint32 value.

Returns:

True if the term is a rational and its numerator and denominator fit into 32 bit integer values.

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

Get the 32 bit integer representations of the numerator and denominator of a rational value.

Note

Requires that this term is a rational value and its numerator and denominator fit into 32 bit integer values (see isReal32Value()).

Returns:

The representation of a rational value as a pair of its numerator and denominator as integer values.

bool isReal64Value() const

Determine if this term is a rational value whose numerator fits into an int64 value and its denominator fits into a uint64 value.

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

Get the 64 bit integer representations of the numerator and denominator of a rational value.

Note

Requires that this term is a rational value and its numerator and denominator fit into 64 bit integer values (see isReal64Value()).

Returns:

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

bool isRealValue() const

Determine if this term is a rational value.

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

Get a string representation of this rational value.

Note

Requires that this term is a rational value (see isRealValue()).

Returns:

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

bool isConstArray() const

Determine if this term is a constant array.

Returns:

True if the term is a constant array.

Term getConstArrayBase() const

Determine the base (element stored at all indices) of a constant array.

Note

Requires that this term is a constant array (see isConstArray()).

Returns:

The base term.

bool isBooleanValue() const

Determine if this term is a Boolean value.

Returns:

True if the term is a Boolean value.

bool getBooleanValue() const

Get the value of a Boolean term as a native Boolean value.

Note

Asserts isBooleanValue().

Returns:

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

bool isBitVectorValue() const

Determine if this term is a bit-vector value.

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.

Note

Asserts isBitVectorValue().

Parameters:

base – 2 for binary, 10 for decimal, and 16 for hexadecimal.

Returns:

The string representation of a bit-vector value.

bool isFiniteFieldValue() const

Determine if this term is a finite field value.

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

Determine if this term is an uninterpreted sort value.

Returns:

True if the term is an abstract value.

std::string getUninterpretedSortValue() const

Get a string representation of an uninterpreted sort value.

Note

Asserts isUninterpretedSortValue().

Returns:

The representation of an uninterpreted sort value as a string.

bool isTupleValue() const

Determine if this term is a tuple value.

Returns:

True if the term is a tuple value.

std::vector<Term> getTupleValue() const

Get a tuple value as a vector of terms.

Note

Asserts isTupleValue().

Returns:

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

bool isRoundingModeValue() const

Determine if this term is a floating-point rounding mode value.

Returns:

True if the term is a rounding mode value.

RoundingMode getRoundingModeValue() const

Get the RoundingMode value of a given rounding-mode value term.

Note

Asserts isRoundingModeValue().

Returns:

The floating-point rounding mode value of the term.

bool isFloatingPointPosZero() const

Determine if this term is a floating-point positive zero value (+zero).

Returns:

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

bool isFloatingPointNegZero() const

Determine if this term is a floating-point negative zero value (-zero).

Returns:

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

bool isFloatingPointPosInf() const

Determine if this term is a floating-point positive infinity value (+oo).

Returns:

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

bool isFloatingPointNegInf() const

Determine if this term is a floating-point negative infinity value (-oo).

Returns:

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

bool isFloatingPointNaN() const

Determine if a given term is a floating-point NaN value.

Returns:

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

bool isFloatingPointValue() const

Determine if a given term is a floating-point value.

Returns:

True if the term is a floating-point value.

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

Get the representation of a floating-point value as a tuple of its exponent width, significand width and a bit-vector value term.

Note

Asserts isFloatingPointValue().

Returns:

The floating-point value representation.

bool isSetValue() const

Determine if this term is a set value.

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

Get a set value as a set of terms.

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

Get a sequence value as a vector of terms.

Note

Asserts isSequenceValue().

Returns:

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

bool isCardinalityConstraint() const

Determine if this term is a cardinality constraint.

Returns:

True if the term is a cardinality constraint.

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

Get a cardinality constraint as a pair of its sort and upper bound.

Note

Asserts isCardinalityConstraint().

Returns:

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

bool isRealAlgebraicNumber() const

Determine if this term is a real algebraic number.

Returns:

True if the term is a real algebraic number.

Term getRealAlgebraicNumberDefiningPolynomial(const Term &v) const

Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable.

Note

Asserts isRealAlgebraicNumber().

Parameters:

v – The variable over which to express the polynomial.

Returns:

The defining polynomial.

Term getRealAlgebraicNumberLowerBound() const

Get the lower bound for a real algebraic number value.

Note

Asserts isRealAlgebraicNumber().

Returns:

The lower bound.

Term getRealAlgebraicNumberUpperBound() const

Get the upper bound for a real algebraic number value.

Note

Asserts isRealAlgebraicNumber().

Returns:

The upper bound.

bool isSkolem() const

Is this term a skolem?

Warning

This function is experimental and may change in future versions.

Returns:

True if this term is a skolem function.

SkolemId getSkolemId() const

Get skolem identifier of this term.

Note

Asserts isSkolem().

Warning

This function is experimental and may change in future versions.

Returns:

The skolem identifier of this term.

std::vector<Term> getSkolemIndices() const

Get the skolem indices of this term.

Note

Asserts isSkolem().

Warning

This function is experimental and may change in future versions.

Returns:

The skolem indices of this term. This is list of terms that the skolem function is indexed by. For example, the array diff skolem SkolemId::ARRAY_DEQ_DIFF is indexed by two arrays.

Friends

friend class parser::Cmd
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(TermManager *tm, const std::shared_ptr<internal::Node> &e, uint32_t p)

Constructor

Parameters:

  • tm – The associated term 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.

std::ostream &cvc5::operator<<(std::ostream &out, const Term &t)

Serialize a term to given stream.

Parameters:

  • out – The output stream.

  • t – The term to be serialized to the given output stream.

Returns:

The output stream.

std::ostream &cvc5::operator<<(std::ostream &out, const std::vector<Term> &vector)

Serialize a vector of terms to given stream.

Parameters:

  • out – The output stream.

  • vector – The vector of terms to be serialized to the given stream.

Returns:

The output stream.

std::ostream &cvc5::operator<<(std::ostream &out, const std::set<Term> &set)

Serialize a set of terms to the given stream.

Parameters:

  • out – The output stream.

  • set – The set of terms to be serialized to the given stream.

Returns:

The output stream.

std::ostream &cvc5::operator<<(std::ostream &out, const std::unordered_set<Term> &unordered_set)

Serialize an unordered_set of terms to the given stream.

Parameters:

  • out – The output stream.

  • unordered_set – The set of terms to be serialized to the given stream.

Returns:

The output stream.

template<typename V>
std::ostream &cvc5::operator<<(std::ostream &out, const std::map<Term, V> &map)

Serialize a map of terms to the given stream.

Parameters:

  • out – The output stream.

  • map – The map of terms to be serialized to the given stream.

Returns:

The output stream.

template<typename V>
std::ostream &cvc5::operator<<(std::ostream &out, const std::unordered_map<Term, V> &unordered_map)

Serialize an unordered_map of terms to the given stream.

Parameters:

  • out – The output stream.

  • unordered_map – The map of terms to be serialized to the given stream.

Returns:

The output stream.

template<>
struct hash<cvc5::Term>

Hash function for Terms.

Public Functions

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