TermManager

This class represents a cvc5 term manager instance.

Terms, Sorts and Ops are not tied to a cvc5.Solver but associated with a cvc5.TermManager instance, which can be shared between solver instances (and thus allows sharing of terms and sorts between solver instances). Term kinds are defined via enum class cvc5.Kind, and sort kinds via enum class cvc5.SortKind.

class cvc5.TermManager

A cvc5 term manager.

Wrapper class for cvc5::TermManager.

getBooleanSort()

Returns:: Sort Boolean.

getIntegerSort()

Returns:: Sort Integer.

getNumIndicesForSkolemId()

Get the number of indices for a skolem id.

Warning

This function is experimental and may change in future versions.

Parameters:: id – The skolem id.
Returns:: The number of indice for a skolem with the given id.

getRealSort()

Returns:: Sort Real.

getRegExpSort()

Returns:: The sort of regular expressions.

getRoundingModeSort()

Returns:: Sort RoundingMode.

getStatistics()

Get a snapshot of the current state of the statistic values of this term manager.

Term manager statistics are independent from any solver instance. The returned object is completely decoupled from the term manager and will not change when the solver is used again.

Returns:: A snapshot of the current state of the statistic values.

getStringSort()

Returns:: Sort String.

mkAbstractSort()

Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.

Given kind must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, ARRAY_SORT and BITVECTOR_SORT can be passed as the kind k to this method, while INTEGER_SORT and STRING_SORT cannot.

Providing the kind ABSTRACT_SORT as an argument to this method returns the (fully) unspecified sort, denoted ?.

Providing a kind of sort that has no indices and a fixed arity of argument sorts will return the sort of kind kind whose arguments are the unspecified sort. For example, mkAbstractSort(ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is py:obj:ARRAY_SORT <Kind.ARRAY_SORT>.

Parameters:: k – The kind of the abstract sort
Returns:: The abstract sort.

Warning

This function is experimental and may change in future versions.

mkArraySort()

Create an array sort.

Parameters:

indexSort – The array index sort.
elemSort – The array element sort.

Returns:

The array sort.

mkBagSort()

Create a bag sort.

Parameters:: elemSort – The sort of the bag elements.
Returns:: The bag sort.

mkBitVector()

Create bit-vector value.

Supports the following arguments:

Term mkBitVector(int size, int val=0)
Term mkBitVector(int size, string val, int base)

Parameters:

size – The bit-width.
val – An integer representating the value, in the first form. In the second form, a string representing the value.
base – The base of the string representation (second form only).

Returns:

A Term representing a bit-vector value.

mkBitVectorSort()

Create a bit-vector sort.

Parameters:: size – The bit-width of the bit-vector sort
Returns:: The bit-vector sort

mkBoolean()

Create a Boolean constant.

Returns:: The Boolean constant.
Parameters:: val – The value of the constant.

mkCardinalityConstraint()

Create cardinality constraint.

Warning

This function is experimental and may change in future versions.

Parameters:

sort – Sort of the constraint.
index – The upper bound for the cardinality of the sort.

mkConst()

Create (first-order) constant (0-arity function symbol).

SMT-LIB:

( declare-const <symbol> <sort> )
( declare-fun <symbol> ( ) <sort> )

Parameters:

sort – The sort of the constant.
symbol – The name of the constant. If None, a default symbol is used.

Returns:

The first-order constant.

mkConstArray()

Create a constant array with the provided constant value stored at every index

Parameters:

sort – The sort of the constant array (must be an array sort).
val – The constant value to store (must match the sort’s element sort).

Returns:

The constant array term.

mkDatatypeConstructorDecl()

Create datatype constructor declaration.

Parameters:: name – The name of the constructor.
Returns:: The datatype constructor declaration.

mkDatatypeDecl()

Create a datatype declaration.

Parameters:

name – The name of the datatype.
isCoDatatype – True if a codatatype is to be constructed.

Returns:

The datatype declaration.

mkDatatypeSort()

Create a datatype sort.

Parameters:: dtypedecl – The datatype declaration from which the sort is created.
Returns:: The datatype sort.

mkDatatypeSorts()

Create a vector of datatype sorts using unresolved sorts. The names of the datatype declarations in dtypedecls must be distinct.

When constructing datatypes, unresolved sorts are replaced by the datatype sort constructed for the datatype declaration it is associated with.

Parameters:: dtypedecls – The datatype declarations from which the sort is created.
Returns:: The datatype sorts.

mkEmptyBag()

Create a constant representing an empty bag of the given sort.

Parameters:: sort – The sort of the bag elements.
Returns:: The empty bag constant.

mkEmptySequence()

Create an empty sequence of the given element sort.

Parameters:: sort – The element sort of the sequence.
Returns:: The empty sequence with given element sort.

mkEmptySet()

Create a constant representing an empty set of the given sort.

Parameters:: sort – The sort of the set elements.
Returns:: The empty set constant.

mkFalse()

Create a Boolean false constant.

Returns:: The false constant.

mkFiniteFieldElem()

Create finite field value.

Supports the following arguments:

Term mkFiniteFieldElem(int value, Sort sort)
Term mkFiniteFieldElem(string value, Sort sort)
Term mkFiniteFieldElem(string value, Sort sort, int base)

Parameters:

value – The value of the element’s integer representation. An integer or string of base 10 if the base is not explicitly given, and else a string in the given base.
sort – The field to create the element in.
base – The base of the string representation of value.

Returns:

A Term representing a finite field value.

mkFiniteFieldSort()

Create a finite field sort.

Supports the following arguments:

Sort mkFiniteFieldSort(int size)
Sort mkFiniteFieldSort(string size)
Sort mkFiniteFieldSort(string size, int base)

Parameters:

size – The size of the field. Must be a prime-power. An integer or string of base 10 if the base is not explicitly given, and else a string in the given base.
base – The base of the string representation of size.

mkFloatingPoint()

Create a floating-point value from a bit-vector given in IEEE-754 format, or from its three IEEE-754 bit-vector value components (sign bit, exponent, significand). Arguments must be either given as (int, int, Term) or (Term, Term, Term).

:param arg0 The size of the exponent or the sign bit. :param arg1 The size of the signifcand or the bit-vector

representing the exponent.

Parameters:: arg2 – The value of the floating-point constant as a bit-vector term or the bit-vector representing the significand.

:return The floating-point value.

mkFloatingPointNaN()

Create a not-a-number (NaN) floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

mkFloatingPointNegInf()

Create a negative infinity floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

mkFloatingPointNegZero()

Create a negative zero (+0.0) floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

mkFloatingPointPosInf()

Create a positive infinity floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

mkFloatingPointPosZero()

Create a positive zero (+0.0) floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

mkFloatingPointSort()

Create a floating-point sort.

Parameters:

exp – The bit-width of the exponent of the floating-point sort.
sig – The bit-width of the significand of the floating-point sort.

mkFunctionSort()

Create function sort.

Parameters:

sorts – The sort of the function arguments.
codomain – The sort of the function return value.

Returns:

The function sort.

mkInteger()

Create an integer constant.

Parameters:: val – Representation of the constant: either a string or integer.
Returns:: A constant of sort Integer.

mkNullableIsNull()

Create a null tester for a nullable term.

Parameters:: term – A nullable term.
Returns:: A tester whether term is null.

mkNullableIsSome()

Create a some tester for a nullable term.

Parameters:: term – A nullable term.
Returns:: A tester whether term is some.

mkNullableLift()

Create a term that lifts kind to nullable terms. Example: If we have the term ((_ nullable.lift +) x y), where x, y of type (Nullable Int), then kind would be ADD, and args would be [x, y]. This function would return (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)

Parameters:

kind – The lifted operator.
args – The arguments of the lifted operator.

Returns:

A term of Kind NULLABLE_LIFT where the first child is a lambda expression, and the remaining children are the original arguments.

mkNullableNull()

Create a constant representing an null of the given sort.

Parameters:: term – The sort of the Nullable element.
Returns:: The null constant.

mkNullableSome()

Create a nullable some term.

Parameters:: term – The elements value.
Returns:: The element value wrapped in some constructor.

mkNullableSort()

Create a nullable sort.

Parameters:: elemSort – The sort of the element of the nullable.
Returns:: The nullable sort.

mkNullableVal()

Create a selector for nullable term.

Parameters:: term – A nullable term.
Returns:: The element value of the nullable term.

mkOp()

Create operator.

Supports the following arguments:

Op mkOp(Kind kind)
Op mkOp(Kind kind, const string& arg)
Op mkOp(Kind kind, uint32_t arg0, ...)

mkParamSort()

Create a sort parameter.

Warning

This function is experimental and may change in future versions.

Parameters:: symbol – The name of the sort.
Returns:: The sort parameter.

mkPi()

Create a constant representing the number Pi.

Returns:: A constant representing PI.

mkPredicateSort()

Create a predicate sort.

Parameters:: sorts – The list of sorts of the predicate.
Returns:: The predicate sort.

mkReal()

Create a real constant from a numerator and an optional denominator.

First converts the arguments to a temporary string, either "<numerator>" or "<numerator>/<denominator>". This temporary string is forwarded to cvc5::Solver::mkReal() and should thus represent an integer, a decimal number or a fraction.

Parameters:

numerator – The numerator.
denominator – The denominator, or None.

Returns:

A real term with literal value.

mkRecordSort()

Create a record sort

Warning

This function is experimental and may change in future versions.

Parameters:: fields – The list of fields of the record.
Returns:: The record sort.

mkRegexpAll()

Create a regular expression all (re.all) term.

Returns:: The all term.

mkRegexpAllchar()

Create a regular expression allchar (re.allchar) term.

Returns:: The allchar term.

mkRegexpNone()

Create a regular expression none (re.none) term.

Returns:: The none term.

mkRoundingMode()

Create a roundingmode constant.

Parameters:: rm – The floating point rounding mode this constant represents.

mkSepEmp()

Create a separation logic empty term.

Warning

This function is experimental and may change in future versions.

Returns:: The separation logic empty term.

mkSepNil()

Create a separation logic nil term.

Warning

This function is experimental and may change in future versions.

Parameters:: sort – The sort of the nil term.
Returns:: The separation logic nil term.

mkSequenceSort()

Create a sequence sort.

Parameters:: elemSort – The sort of the sequence elements
Returns:: The sequence sort.

mkSetSort()

Create a set sort.

Parameters:: elemSort – The sort of the set elements.
Returns:: The set sort.

mkSkolem()

Create a skolem.

Warning

This function is experimental and may change in future versions.

Parameters:

id – The skolem id.
indices – The indices for the skolem.

Returns:

The skolem with the given id and indices.

mkString()

Create a String constant from a str which may contain SMT-LIB compatible escape sequences like \u1234 to encode unicode characters.

Parameters:

s – The string this constant represents.
useEscSequences – Determines whether escape sequences in s should be converted to the corresponding unicode character

Returns:

The String constant.

mkTerm()

Create a term.

Supports the following arguments:

Term mkTerm(Kind kind)
Term mkTerm(Op op)
Term mkTerm(Kind kind, *args)
Term mkTerm(Op op, *args)

where *args is a comma-separated list of terms.

mkTrue()

Create a Boolean true constant.

Returns:: The true constant.

mkTuple()

Create a tuple term. Terms are automatically converted if sorts are compatible.

Parameters:: terms – The elements in the tuple.
Returns:: The tuple Term.

mkTupleSort()

Create a tuple sort.

Parameters:: sorts – Of the elements of the tuple.
Returns:: The tuple sort.

mkUninterpretedSort()

Create an uninterpreted sort.

Parameters:: symbol – The name of the sort.
Returns:: The uninterpreted sort.

mkUninterpretedSortConstructorSort()

Create a sort constructor sort.

An uninterpreted sort constructor is an uninterpreted sort with arity > 0.

Parameters:

symbol – The symbol of the sort.
arity – The arity of the sort (must be > 0).

Returns:

The sort constructor sort.

mkUniverseSet()

Create a universe set of the given sort.

Parameters:: sort – The sort of the set elements
Returns:: The universe set constant

mkUnresolvedDatatypeSort()

Create an unresolved datatype sort.

This is for creating yet unresolved sort placeholders for mutually recursive datatypes.

Parameters:

symbol – The name of the sort.
arity – The number of sort parameters of the sort.

Returns:

The unresolved sort.

mkVar()

Create a bound variable to be used in a binder (i.e. a quantifier, a lambda, or a witness binder).

Parameters:

sort – The sort of the variable.
symbol – The name of the variable.

Returns:

The variable.