Solver 

This class represents a cvc5 solver instance.

Terms , Sorts and Ops are not tied to a cvc5::Solver instance and can be shared between instances. Term kinds are defined via enum class cvc5::Kind , and sort kinds via enum class cvc5::SortKind .

Solver options are configured via cvc5::Solver::setOption() and queried via cvc5::Solver::getOption() (for more information on configuration options, see Options ). Information about a specific option can be retrieved via cvc5::getOptionInfo() (see OptionInfo ).

class Solver 

A cvc5 solver.

Public Functions

Solver ( ) 

Constructor.

Returns :: The Solver .

~Solver ( ) : Destructor.

Solver ( const Solver & ) = delete : Disallow copy/assignment.

Solver & operator = ( const Solver & ) = delete 

Sort getBooleanSort ( ) const 

Get the Boolean sort.

Returns :: Sort Boolean.

Sort getIntegerSort ( ) const 

Get the Integer sort.

Returns :: Sort Integer.

Sort getRealSort ( ) const 

Get the Real sort.

Returns :: Sort Real.

Sort getRegExpSort ( ) const 

Get the regular expression sort.

Returns :: Sort RegExp.

Sort getRoundingModeSort ( ) const 

Get the rounding mode sort.

Returns :: Sort RoundingMode.

Sort getStringSort ( ) const 

Get the string sort.

Returns :: Sort String.

Sort mkArraySort ( const Sort & indexSort , const Sort & elemSort ) const 

Create an array sort.

Parameters :

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

Returns :

The array sort.

Sort mkBitVectorSort ( uint32_t size ) const 

Create a bit-vector sort.

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

Sort mkFloatingPointSort ( uint32_t exp , uint32_t sig ) const 

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.

Sort mkFiniteFieldSort ( const std :: string & size , uint32_t base = 10 ) const 

Create a finite-field sort from a given string of base n.

Parameters :

size – The modulus of the field. Must be prime.
base – The base of the string representation of size .

Returns :

The finite-field sort.

Sort mkDatatypeSort ( const DatatypeDecl & dtypedecl ) const 

Create a datatype sort.

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

std :: vector < Sort > mkDatatypeSorts ( const std :: vector < DatatypeDecl > & dtypedecls ) const 

Create a vector of datatype sorts.

Note

The names of the datatype declarations must be distinct.

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

Sort mkFunctionSort ( const std :: vector < Sort > & sorts , const Sort & codomain ) const 

Create function sort.

Parameters :

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

Returns :

The function sort.

Sort mkParamSort ( const std :: optional < std :: string > & symbol = std :: nullopt ) const 

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.

Sort mkPredicateSort ( const std :: vector < Sort > & sorts ) const 

Create a predicate sort.

This is equivalent to calling mkFunctionSort() with the Boolean sort as the codomain.

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

Sort mkRecordSort ( const std :: vector < std :: pair < std :: string , Sort > > & fields ) const 

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.

Sort mkSetSort ( const Sort & elemSort ) const 

Create a set sort.

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

Sort mkBagSort ( const Sort & elemSort ) const 

Create a bag sort.

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

Sort mkSequenceSort ( const Sort & elemSort ) const 

Create a sequence sort.

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

Sort mkAbstractSort ( SortKind k ) const 

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

The kind k 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 function, while #INTEGER_SORT and #STRING_SORT cannot.

Note

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

Note

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

Warning

This function is experimental and may change in future versions.

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

Sort mkUninterpretedSort ( const std :: optional < std :: string > & symbol = std :: nullopt ) const 

Create an uninterpreted sort.

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

Sort mkUnresolvedDatatypeSort ( const std :: string & symbol , size_t arity = 0 ) const 

Create an unresolved datatype sort.

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

Warning

This function is experimental and may change in future versions.

Parameters :

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

Returns :

The unresolved sort.

Sort mkUninterpretedSortConstructorSort ( size_t arity , const std :: optional < std :: string > & symbol = std :: nullopt ) const 

Create an uninterpreted 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 uninterpreted sort constructor sort.

Sort mkTupleSort ( const std :: vector < Sort > & sorts ) const 

Create a tuple sort.

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

Term mkTerm ( Kind kind , const std :: vector < Term > & children = { } ) const 

Create n-ary term of given kind.

Parameters :

kind – The kind of the term.
children – The children of the term.

Returns :

The Term

Term mkTerm ( const Op & op , const std :: vector < Term > & children = { } ) const 

Create n-ary term of given kind from a given operator. Create operators with mkOp() .

Parameters :

op – The operator.
children – The children of the term.

Returns :

The Term .

Term mkTuple ( const std :: vector < Term > & terms ) const 

Create a tuple term.

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

Op mkOp ( Kind kind , const std :: vector < uint32_t > & args = { } ) const 

Create operator of Kind:

#BITVECTOR_EXTRACT
#BITVECTOR_REPEAT
#BITVECTOR_ROTATE_LEFT
#BITVECTOR_ROTATE_RIGHT
#BITVECTOR_SIGN_EXTEND
#BITVECTOR_ZERO_EXTEND
#DIVISIBLE
#FLOATINGPOINT_TO_FP_FROM_FP
#FLOATINGPOINT_TO_FP_FROM_IEEE_BV
#FLOATINGPOINT_TO_FP_FROM_REAL
#FLOATINGPOINT_TO_FP_FROM_SBV
#FLOATINGPOINT_TO_FP_FROM_UBV
#FLOATINGPOINT_TO_SBV
#FLOATINGPOINT_TO_UBV
#INT_TO_BITVECTOR
#TUPLE_PROJECT

See cvc5::Kind for a description of the parameters.

Note

If args is empty, the Op simply wraps the cvc5::Kind . The Kind can be used in Solver::mkTerm directly without creating an Op first.

Parameters :

kind – The kind of the operator.
args – The arguments (indices) of the operator.

Op mkOp ( Kind kind , const std :: string & arg ) const 

Create operator of kind:

#DIVISIBLE (to support arbitrary precision integers) See cvc5::Kind for a description of the parameters.

Parameters :

kind – The kind of the operator.
arg – The string argument to this operator.

Term mkTrue ( ) const 

Create a Boolean true constant.

Returns :: The true constant.

Term mkFalse ( ) const 

Create a Boolean false constant.

Returns :: The false constant.

Term mkBoolean ( bool val ) const 

Create a Boolean constant.

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

Term mkPi ( ) const 

Create a constant representing the number Pi.

Returns :: A constant representing Pi.

Term mkInteger ( const std :: string & s ) const 

Create an integer constant from a string.

Parameters :: s – The string representation of the constant, may represent an integer (e.g., “123”).
Returns :: A constant of sort Integer assuming s represents an integer)

Term mkInteger ( int64_t val ) const 

Create an integer constant from a c++ int.

Parameters :: val – The value of the constant.
Returns :: A constant of sort Integer.

Term mkReal ( const std :: string & s ) const 

Create a real constant from a string.

Parameters :: s – The string representation of the constant, may represent an integer (e.g., “123”) or real constant (e.g., “12.34” or “12/34”).
Returns :: A constant of sort Real.

Term mkReal ( int64_t val ) const 

Create a real constant from an integer.

Parameters :: val – The value of the constant.
Returns :: A constant of sort Integer.

Term mkReal ( int64_t num , int64_t den ) const 

Create a real constant from a rational.

Parameters :

num – The value of the numerator.
den – The value of the denominator.

Returns :

A constant of sort Real.

Term mkRegexpAll ( ) const 

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

Returns :: The all term.

Term mkRegexpAllchar ( ) const 

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

Returns :: The allchar term.

Term mkRegexpNone ( ) const 

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

Returns :: The none term.

Term mkEmptySet ( const Sort & sort ) const 

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

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

Term mkEmptyBag ( const Sort & sort ) const 

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

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

Term mkSepEmp ( ) const 

Create a separation logic empty term.

Warning

This function is experimental and may change in future versions.

Returns :: The separation logic empty term.

Term mkSepNil ( const Sort & sort ) const 

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.

Term mkString ( const std :: string & s , bool useEscSequences = false ) const 

Create a String constant from a std::string 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.

Term mkString ( const std :: wstring & s ) const 

Create a String constant from a std::wstring . This function does not support escape sequences as std::wstring already supports unicode characters.

Parameters :: s – The string this constant represents.
Returns :: The String constant.

Term mkEmptySequence ( const Sort & sort ) const 

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.

Term mkUniverseSet ( const Sort & sort ) const 

Create a universe set of the given sort.

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

Term mkBitVector ( uint32_t size , uint64_t val = 0 ) const 

Create a bit-vector constant of given size and value.

Note

The given value must fit into a bit-vector of the given size.

Parameters :

size – The bit-width of the bit-vector sort.
val – The value of the constant.

Returns :

The bit-vector constant.

Term mkBitVector ( uint32_t size , const std :: string & s , uint32_t base ) const 

Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

Note

The given value must fit into a bit-vector of the given size.

Parameters :

size – The bit-width of the constant.
s – The string representation of the constant.
base – The base of the string representation ( 2 for binary, 10 for decimal, and 16 for hexadecimal).

Returns :

The bit-vector constant.

Term mkFiniteFieldElem ( const std :: string & value , const Sort & sort , uint32_t base = 10 ) const 

Create a finite field constant in a given field from a given string of base n.

If size is the field size, the constant needs not be in the range [0,size). If it is outside this range, it will be reduced modulo size before being constructed.

Parameters :

value – The string representation of the constant.
sort – The field sort.
base – The base of the string representation of value .

Term mkConstArray ( const Sort & sort , const Term & val ) const 

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.

Term mkFloatingPointPosInf ( uint32_t exp , uint32_t sig ) const 

Create a positive infinity floating-point constant (SMT-LIB: +oo ).

Parameters :

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

Returns :

The floating-point constant.

Term mkFloatingPointNegInf ( uint32_t exp , uint32_t sig ) const 

Create a negative infinity floating-point constant (SMT-LIB: -oo ).

Parameters :

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

Returns :

The floating-point constant.

Term mkFloatingPointNaN ( uint32_t exp , uint32_t sig ) const 

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

Parameters :

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

Returns :

The floating-point constant.

Term mkFloatingPointPosZero ( uint32_t exp , uint32_t sig ) const 

Create a positive zero floating-point constant (SMT-LIB: +zero).

Parameters :

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

Returns :

The floating-point constant.

Term mkFloatingPointNegZero ( uint32_t exp , uint32_t sig ) const 

Create a negative zero floating-point constant (SMT-LIB: -zero).

Parameters :

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

Returns :

The floating-point constant.

Term mkRoundingMode ( RoundingMode rm ) const 

Create a rounding mode value.

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

Term mkFloatingPoint ( uint32_t exp , uint32_t sig , const Term & val ) const 

Create a floating-point value from a bit-vector given in IEEE-754 format.

Parameters :

exp – Size of the exponent.
sig – Size of the significand.
val – Value of the floating-point constant as a bit-vector term.

Returns :

The floating-point value.

Term mkFloatingPoint ( const Term & sign , const Term & exp , const Term & sig ) const 

Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).

Parameters :

sign – The sign bit.
exp – The bit-vector representing the exponent.
sig – The bit-vector representing the significand.

Returns :

The floating-point value.

Term mkCardinalityConstraint ( const Sort & sort , uint32_t upperBound ) const 

Create a cardinality constraint for an uninterpreted sort.

Warning

This function is experimental and may change in future versions.

Parameters :

sort – The sort the cardinality constraint is for.
upperBound – The upper bound on the cardinality of the sort.

Returns :

The cardinality constraint.

Term mkConst ( const Sort & sort , const std :: optional < std :: string > & symbol = std :: nullopt ) const 

Create a free constant.

Note that the returned term is always fresh, even if the same arguments were provided on a previous call to mkConst.

SMT-LIB:

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

Parameters :

sort – The sort of the constant.
symbol – The name of the constant (optional).

Returns :

The constant.

Term mkVar ( const Sort & sort , const std :: optional < std :: string > & symbol = std :: nullopt ) const 

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

Note that the returned term is always fresh, even if the same arguments were provided on a previous call to mkConst.

Parameters :

sort – The sort of the variable.
symbol – The name of the variable (optional).

Returns :

The variable.

DatatypeConstructorDecl mkDatatypeConstructorDecl ( const std :: string & name ) 

Create a datatype constructor declaration.

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

DatatypeDecl mkDatatypeDecl ( const std :: string & name , bool isCoDatatype = false ) 

Create a datatype declaration.

Parameters :

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

Returns :

The DatatypeDecl .

DatatypeDecl mkDatatypeDecl ( const std :: string & name , const std :: vector < Sort > & params , bool isCoDatatype = false ) 

Create a datatype declaration. Create sorts parameter with Solver::mkParamSort() .

Warning

This function is experimental and may change in future versions.

Parameters :

name – The name of the datatype.
params – A list of sort parameters.
isCoDatatype – True if a codatatype is to be constructed.

Returns :

The DatatypeDecl .

Term simplify ( const Term & t ) 

Simplify a formula without doing “much” work.

Does not involve the SAT Engine in the simplification, but uses the current definitions, and assertions. It also involves theory normalization.

Warning

This function is experimental and may change in future versions.

Parameters :: t – The formula to simplify.
Returns :: The simplified formula.

void assertFormula ( const Term & term ) const 

Assert a formula.

SMT-LIB:

(assert <term>)

Parameters :: term – The formula to assert.

Result checkSat ( ) const 

Check satisfiability.

SMT-LIB:

(check-sat)

Returns :: The result of the satisfiability check.

Result checkSatAssuming ( const Term & assumption ) const 

Check satisfiability assuming the given formula.

SMT-LIB:

(check-sat-assuming ( <prop_literal> ))

Parameters :: assumption – The formula to assume.
Returns :: The result of the satisfiability check.

Result checkSatAssuming ( const std :: vector < Term > & assumptions ) const 

Check satisfiability assuming the given formulas.

SMT-LIB:

(check-sat-assuming ( <prop_literal>+ ))

Parameters :: assumptions – The formulas to assume.
Returns :: The result of the satisfiability check.

Sort declareDatatype ( const std :: string & symbol , const std :: vector < DatatypeConstructorDecl > & ctors ) const 

Create datatype sort.

SMT-LIB:

                (declare-datatype <symbol> <datatype_decl>)

               

Parameters :

symbol – The name of the datatype sort.
ctors – The constructor declarations of the datatype sort.

Returns :

The datatype sort.

Term declareFun ( const std :: string & symbol , const std :: vector < Sort > & sorts , const Sort & sort , bool fresh = true ) const 

Declare n-ary function symbol.

SMT-LIB:

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

               

Parameters :

symbol – The name of the function.
sorts – The sorts of the parameters to this function.
sort – The sort of the return value of this function.
fresh – If true, then this method always returns a new Term . Otherwise, this method will always return the same Term for each call with the given sorts and symbol where fresh is false.

Returns :

The function.

Sort declareSort ( const std :: string & symbol , uint32_t arity , bool fresh = true ) const 

Declare uninterpreted sort.

SMT-LIB:

                (declare-sort <symbol> <numeral>)

               

Note

This corresponds to mkUninterpretedSort(const std::optional<std::string>&) const if arity = 0, and to mkUninterpretedSortConstructorSort(size_t arity, const std::optional<std::string>&) const if arity > 0.

Parameters :

symbol – The name of the sort.
arity – The arity of the sort.
fresh – If true, then this method always returns a new Sort . Otherwise, this method will always return the same Sort for each call with the given arity and symbol where fresh is false.

Returns :

The sort.

Term defineFun ( const std :: string & symbol , const std :: vector < Term > & bound_vars , const Sort & sort , const Term & term , bool global = false ) const 

Define n-ary function.

SMT-LIB:

(define-fun <function_def>)

Parameters :

symbol – The name of the function.
bound_vars – The parameters to this function.
sort – The sort of the return value of this function.
term – The function body.
global – Determines whether this definition is global (i.e., persists when popping the context).

Returns :

The function.

Term defineFunRec ( const std :: string & symbol , const std :: vector < Term > & bound_vars , const Sort & sort , const Term & term , bool global = false ) const 

Define recursive function.

SMT-LIB:

(define-fun-rec <function_def>)

Parameters :

symbol – The name of the function.
bound_vars – The parameters to this function.
sort – The sort of the return value of this function.
term – The function body.
global – Determines whether this definition is global (i.e., persists when popping the context).

Returns :

The function.

Term defineFunRec ( const Term & fun , const std :: vector < Term > & bound_vars , const Term & term , bool global = false ) const 

Define recursive function.

SMT-LIB:

(define-fun-rec <function_def>)

Create parameter fun with mkConst() .

Parameters :

fun – The sorted function.
bound_vars – The parameters to this function.
term – The function body.
global – Determines whether this definition is global (i.e., persists when popping the context).

Returns :

The function.

void defineFunsRec ( const std :: vector < Term > & funs , const std :: vector < std :: vector < Term > > & bound_vars , const std :: vector < Term > & terms , bool global = false ) const 

Define recursive functions.

SMT-LIB:

                (define-funs-rec
    ( <function_decl>_1 ... <function_decl>_n )
    ( <term>_1 ... <term>_n )
)

               

Create elements of parameter funs with Solver::mkConst() .

Parameters :

funs – The sorted functions.
bound_vars – The list of parameters to the functions.
terms – The list of function bodies of the functions.
global – Determines whether this definition is global (i.e., persists when popping the context).

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

Get the list of asserted formulas.

SMT-LIB:

(get-assertions)

Returns :: The list of asserted formulas.

std :: string getInfo ( const std :: string & flag ) const 

Get info from the solver.

SMT-LIB:

(get-info <info_flag>)

Returns :: The info.

std :: string getOption ( const std :: string & option ) const 

Get the value of a given option.

SMT-LIB:

(get-option <keyword>)

Parameters :: option – The option for which the value is queried.
Returns :: A string representation of the option value.

std :: vector < std :: string > getOptionNames ( ) const 

Get all option names that can be used with setOption() , getOption() and getOptionInfo() .

Returns :: All option names.

OptionInfo getOptionInfo ( const std :: string & option ) const 

Get some information about the given option.

Check the OptionInfo class for more details on which information is available.

Returns :: Information about the given option.

DriverOptions getDriverOptions ( ) const 

Get the driver options, which provide access to options that can not be communicated properly via getOption() and getOptionInfo() .

Returns :: A DriverOptions object.

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

Get the set of unsat (“failed”) assumptions.

SMT-LIB:

(get-unsat-assumptions)

Requires to enable option produce-unsat-assumptions .

Returns :: The set of unsat assumptions.

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

Get the unsatisfiable core.

SMT-LIB:

(get-unsat-core)

Requires to enable option produce-unsat-cores .

Note

In contrast to SMT-LIB, cvc5’s API does not distinguish between named and unnamed assertions when producing an unsatisfiable core. Additionally, the API allows this option to be called after a check with assumptions. A subset of those assumptions may be included in the unsatisfiable core returned by this function.

Returns :: A set of terms representing the unsatisfiable core.

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

Get the lemmas used to derive unsatisfiability.

SMT-LIB:

(get-unsat-core-lemmas)

Requires the SAT proof unsat core mode, so to enable option unsat-core-mode=sat-proof .

Warning

This function is experimental and may change in future versions.

Returns :: A set of terms representing the lemmas used to derive unsatisfiability.

std :: map < Term , Term > getDifficulty ( ) const 

Get a difficulty estimate for an asserted formula. This function is intended to be called immediately after any response to a checkSat.

Warning

This function is experimental and may change in future versions.

Returns :: A map from (a subset of) the input assertions to a real value that. is an estimate of how difficult each assertion was to solve. Unmentioned assertions can be assumed to have zero difficulty.

std :: pair < Result , std :: vector < Term > > getTimeoutCore ( ) const 

Get a timeout core, which computes a subset of the current assertions that cause a timeout. Note it does not require being proceeded by a call to checkSat.

SMT-LIB:

(get-timeout-core)

This function may make multiple checks for satisfiability internally, each limited by the timeout value given by :ref: timeout-core-timeout <lbl-option-timeout-core-timeout> .

Warning

This function is experimental and may change in future versions.

Returns :: The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of the current assertions that cause a timeout in the specified time :ref: timeout-core-timeout <lbl-option-timeout-core-timeout> . If the result is unsat, then the list of formulas correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the current assertions are satisfiable, and the list of formulas is empty.

std :: pair < Result , std :: vector < Term > > getTimeoutCoreAssuming ( const std :: vector < Term > & assumptions ) const 

Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions. Note it does not require being proceeded by a call to checkSat.

SMT-LIB:

(get-timeout-core (<assert>*))

Warning

This function is experimental and may change in future versions.

Parameters :: assumptions – The (non-empty) set of formulas to assume.
Returns :: The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of assumptions that cause a timeout when added to the current assertions in the specified time :ref: timeout-core-timeout <lbl-option-timeout-core-timeout> . If the result is unsat, then the list of formulas plus the current assertions correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the given assumptions plus the current assertions are satisfiable, and the list of formulas is empty.

std :: vector < Proof > getProof ( modes :: ProofComponent c = modes :: ProofComponent :: FULL ) const 

Get a proof associated with the most recent call to checkSat.

SMT-LIB:

(get-proof :c)

Requires to enable option produce-proofs . The string representation depends on the value of option produce-proofs .

Warning

This function is experimental and may change in future versions.

Parameters :: c – The component of the proof to return
Returns :: A vector of proofs.

std :: string proofToString ( Proof proof , modes :: ProofFormat format = modes :: ProofFormat :: DEFAULT ) const 

Prints a proof as a string in a selected proof format mode. Other aspects of printing are taken from the solver options.

Warning

This function is experimental and may change in future versions.

Parameters :

proof – A proof, usually obtained from Solver::getProof() .
format – The proof format used to print the proof. Must be modes::ProofFormat::NONE if the proof is from a component other than modes::ProofComponent::FULL .

Returns :

The string representation of the proof in the given format.

std :: vector < Term > getLearnedLiterals ( modes :: LearnedLitType t = modes :: LearnedLitType :: INPUT ) const 

Get a list of learned literals that are entailed by the current set of assertions.

Warning

This function is experimental and may change in future versions.

Parameters :: t – The type of learned literals to return
Returns :: A list of literals that were learned at top-level.

Term getValue ( const Term & term ) const 

Get the value of the given term in the current model.

SMT-LIB:

(get-value ( <term> ))

Parameters :: term – The term for which the value is queried.
Returns :: The value of the given term.

std :: vector < Term > getValue ( const std :: vector < Term > & terms ) const 

Get the values of the given terms in the current model.

SMT-LIB:

(get-value ( <term>* ))

Parameters :: terms – The terms for which the value is queried.
Returns :: The values of the given terms.

std :: vector < Term > getModelDomainElements ( const Sort & s ) const 

Get the domain elements of uninterpreted sort s in the current model. The current model interprets s as the finite sort whose domain elements are given in the return value of this function.

Parameters :: s – The uninterpreted sort in question.
Returns :: The domain elements of s in the current model.

bool isModelCoreSymbol ( const Term & v ) const 

This returns false if the model value of free constant v was not essential for showing the satisfiability of the last call to checkSat using the current model. This function will only return false (for any v ) if option model-cores* has been set.

Warning

This function is experimental and may change in future versions.

Parameters :: v – The term in question.
Returns :: True if v is a model core symbol.

std :: string getModel ( const std :: vector < Sort > & sorts , const std :: vector < Term > & consts ) const 

Get the model

SMT-LIB:

(get-model)

Requires to enable option produce-models .

Warning

This function is experimental and may change in future versions.

Parameters :

sorts – The list of uninterpreted sorts that should be printed in the model.
consts – The list of free constants that should be printed in the model. A subset of these may be printed based on isModelCoreSymbol() .

Returns :

A string representing the model.

Term getQuantifierElimination ( const Term & q ) const 

Do quantifier elimination.

SMT-LIB:

(get-qe <q>)

Note

Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.

Warning

This function is experimental and may change in future versions.

Parameters :

q – A quantified formula of the form \(Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)\) where \(Q\bar{x}\) is a set of quantified variables of the form \(Q x_1...x_k\) and \(P( x_1...x_i, y_1...y_j )\) is a quantifier-free formula

Returns :

A formula \(\phi\) such that, given the current set of formulas \(A\) asserted to this solver:

\((A \wedge q)\) and \((A \wedge \phi)\) are equivalent
\(\phi\) is quantifier-free formula containing only free variables in \(y_1...y_n\) .

Term getQuantifierEliminationDisjunct ( const Term & q ) const 

Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.

SMT-LIB:

(get-qe-disjunct <q>)

Note

Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.

Warning

This function is experimental and may change in future versions.

Parameters :

q – A quantified formula of the form \(Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)\) where \(Q\bar{x}\) is a set of quantified variables of the form \(Q x_1...x_k\) and \(P( x_1...x_i, y_1...y_j )\) is a quantifier-free formula

Returns :

A formula \(\phi\) such that, given the current set of formulas \(A\) asserted to this solver:

\((A \wedge q \implies A \wedge \phi)\) if \(Q\) is \(\forall\) , and \((A \wedge \phi \implies A \wedge q)\) if \(Q\) is \(\exists\)
\(\phi\) is quantifier-free formula containing only free variables in \(y_1...y_n\)
If \(Q\) is \(\exists\) , let \((A \wedge Q_n)\) be the formula \((A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge \neg (\phi \wedge Q_n))\) where for each \(i = 1...n\) , formula \((\phi \wedge Q_i)\) is the result of calling Solver::getQuantifierEliminationDisjunct() for \(q\) with the set of assertions \((A \wedge Q_{i-1})\) . Similarly, if \(Q\) is \(\forall\) , then let \((A \wedge Q_n)\) be \((A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge Q_n))\) where \((\phi \wedge Q_i)\) is the same as above. In either case, we have that \((\phi \wedge Q_j)\) will eventually be true or false, for some finite j.

void declareSepHeap ( const Sort & locSort , const Sort & dataSort ) const 

When using separation logic, this sets the location sort and the datatype sort to the given ones. This function should be invoked exactly once, before any separation logic constraints are provided.

Warning

This function is experimental and may change in future versions.

Parameters :

locSort – The location sort of the heap.
dataSort – The data sort of the heap.

Term getValueSepHeap ( ) const 

When using separation logic, obtain the term for the heap.

Warning

This function is experimental and may change in future versions.

Returns :: The term for the heap.

Term getValueSepNil ( ) const 

When using separation logic, obtain the term for nil.

Warning

This function is experimental and may change in future versions.

Returns :: The term for nil.

Term declarePool ( const std :: string & symbol , const Sort & sort , const std :: vector < Term > & initValue ) const 

Declare a symbolic pool of terms with the given initial value.

For details on how pools are used to specify instructions for quantifier instantiation, see documentation for the #INST_POOL kind.

SMT-LIB:

                (declare-pool <symbol> <sort> ( <term>* ))

               

Warning

This function is experimental and may change in future versions.

Parameters :

symbol – The name of the pool.
sort – The sort of the elements of the pool.
initValue – The initial value of the pool.

Returns :

The pool symbol.

Term declareOracleFun ( const std :: string & symbol , const std :: vector < Sort > & sorts , const Sort & sort , std :: function < Term ( const std :: vector < Term > & ) > fn ) const 

Declare an oracle function with reference to an implementation.

Oracle functions have a different semantics with respect to ordinary declared functions. In particular, for an input to be satisfiable, its oracle functions are implicitly universally quantified.

This function is used in part for implementing this command:

(declare-oracle-fun <sym> (<sort>*) <sort> <sym>)

In particular, the above command is implemented by constructing a function over terms that wraps a call to binary sym via a text interface.

Warning

This function is experimental and may change in future versions.

Parameters :

symbol – The name of the oracle
sorts – The sorts of the parameters to this function
sort – The sort of the return value of this function
fn – The function that implements the oracle function.

Returns :

The oracle function

void pop ( uint32_t nscopes = 1 ) const 

Pop (a) level(s) from the assertion stack.

SMT-LIB:

(pop <numeral>)

Parameters :: nscopes – The number of levels to pop.

Term getInterpolant ( const Term & conj ) const 

Get an interpolant

SMT-LIB:

(get-interpolant <conj>)

Requires option produce-interpolants to be set to a mode different from none .

Warning

This function is experimental and may change in future versions.

Parameters :: conj – The conjecture term.
Returns :: A Term \(I\) such that \(A \rightarrow I\) and \(I \rightarrow B\) are valid, where \(A\) is the current set of assertions and \(B\) is given in the input by conj , or the null term if such a term cannot be found.

Term getInterpolant ( const Term & conj , Grammar & grammar ) const 

Get an interpolant

SMT-LIB:

                (get-interpolant <conj> <grammar>)

               

Requires option produce-interpolants to be set to a mode different from none .

Warning

This function is experimental and may change in future versions.

Parameters :

conj – The conjecture term.
grammar – The grammar for the interpolant I.

Returns :

A Term \(I\) such that \(A \rightarrow I\) and \(I \rightarrow B\) are valid, where \(A\) is the current set of assertions and \(B\) is given in the input by conj , or the null term if such a term cannot be found.

Term getInterpolantNext ( ) const 

Get the next interpolant. Can only be called immediately after a successful call to get-interpolant or get-interpolant-next. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful.

SMT-LIB:

(get-interpolant-next)

Requires to enable incremental mode, and option produce-interpolants to be set to a mode different from none .

Warning

This function is experimental and may change in future versions.

Returns :: A Term \(I\) such that \(A \rightarrow I\) and \(I \rightarrow B\) are valid, where \(A\) is the current set of assertions and \(B\) is given in the input by conj , or the null term if such a term cannot be found.

Term getAbduct ( const Term & conj ) const 

Get an abduct.

SMT-LIB:

(get-abduct <conj>)

Requires to enable option produce-abducts .

Warning

This function is experimental and may change in future versions.

Parameters :: conj – The conjecture term.
Returns :: A term \(C\) such that \((A \wedge C)\) is satisfiable, and \((A \wedge \neg B \wedge C)\) is unsatisfiable, where \(A\) is the current set of assertions and \(B\) is given in the input by conj , or the null term if such a term cannot be found.

Term getAbduct ( const Term & conj , Grammar & grammar ) const 

Get an abduct.

SMT-LIB:

                (get-abduct <conj> <grammar>)

               

Requires to enable option produce-abducts .

Warning

This function is experimental and may change in future versions.

Parameters :

conj – The conjecture term.
grammar – The grammar for the abduct \(C\)

Returns :

A term C such that \((A \wedge C)\) is satisfiable, and \((A \wedge \neg B \wedge C)\) is unsatisfiable, where \(A\) is the current set of assertions and \(B\) is given in the input by conj , or the null term if such a term cannot be found.

Term getAbductNext ( ) const 

Get the next abduct. Can only be called immediately after a successful call to get-abduct or get-abduct-next. Is guaranteed to produce a syntactically different abduct wrt the last returned abduct if successful.

SMT-LIB:

(get-abduct-next)

Requires to enable incremental mode, and option produce-abducts .

Warning

This function is experimental and may change in future versions.

Returns :: A term C such that \((A \wedge C)\) is satisfiable, and \((A \wedge \neg B \wedge C)\) is unsatisfiable, where \(A\) is the current set of assertions and \(B\) is given in the input by the last call to getAbduct() , or the null term if such a term cannot be found.

void blockModel ( modes :: BlockModelsMode mode ) const 

Block the current model. Can be called only if immediately preceded by a SAT or INVALID query.

SMT-LIB:

(block-model)

Requires enabling option produce-models .

Warning

This function is experimental and may change in future versions.

Parameters :: mode – The mode to use for blocking.

void blockModelValues ( const std :: vector < Term > & terms ) const 

Block the current model values of (at least) the values in terms. Can be called only if immediately preceded by a SAT query.

SMT-LIB:

(block-model-values ( <terms>+ ))

Requires enabling option produce-models .

Warning

This function is experimental and may change in future versions.

Parameters :: terms – The model values to block.

std :: string getInstantiations ( ) const 

Warning

This function is experimental and may change in future versions.

Returns :: A string that contains information about all instantiations made by the quantifiers module.

void push ( uint32_t nscopes = 1 ) const 

Push (a) level(s) to the assertion stack.

SMT-LIB:

(push <numeral>)

Parameters :: nscopes – The number of levels to push.

void resetAssertions ( ) const 

Remove all assertions.

SMT-LIB:

(reset-assertions)

void setInfo ( const std :: string & keyword , const std :: string & value ) const 

Set info.

SMT-LIB:

(set-info <attribute>)

Parameters :

keyword – The info flag.
value – The value of the info flag.

void setLogic ( const std :: string & logic ) const 

Set logic.

SMT-LIB:

(set-logic <symbol>)

Parameters :: logic – The logic to set.

bool isLogicSet ( ) const 

Is logic set? Returns whether we called setLogic yet for this solver.

Returns :: whether we called setLogic yet for this solver.

std :: string getLogic ( ) const 

Get the logic set the solver.

Note

Asserts isLogicSet() .

Returns :: The logic used by the solver.

void setOption ( const std :: string & option , const std :: string & value ) const 

Set option.

SMT-LIB:

                (set-option :<option> <value>)

               

Parameters :

option – The option name.
value – The option value.

Term declareSygusVar ( const std :: string & symbol , const Sort & sort ) const 

Append symbol to the current list of universal variables.

SyGuS v2:

                (declare-var <symbol> <sort>)

               

Parameters :

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

Returns :

The universal variable.

Grammar mkGrammar ( const std :: vector < Term > & boundVars , const std :: vector < Term > & ntSymbols ) const 

Create a Sygus grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.

Parameters :

boundVars – The parameters to corresponding synth-fun/synth-inv.
ntSymbols – The pre-declaration of the non-terminal symbols.

Returns :

The grammar.

Term synthFun ( const std :: string & symbol , const std :: vector < Term > & boundVars , const Sort & sort ) const 

Synthesize n-ary function.

SyGuS v2:

                (synth-fun <symbol> ( <boundVars>* ) <sort>)

               

Parameters :

symbol – The name of the function.
boundVars – The parameters to this function.
sort – The sort of the return value of this function.

Returns :

The function.

Term synthFun ( const std :: string & symbol , const std :: vector < Term > & boundVars , Sort sort , Grammar & grammar ) const 

Synthesize n-ary function following specified syntactic constraints.

SyGuS v2:

                (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>)

               

Parameters :

symbol – The name of the function.
boundVars – The parameters to this function.
sort – The sort of the return value of this function.
grammar – The syntactic constraints.

Returns :

The function.

void addSygusConstraint ( const Term & term ) const 

Add a forumla to the set of Sygus constraints.

SyGuS v2:

(constraint <term>)

Parameters :: term – The formula to add as a constraint.

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

Get the list of sygus constraints.

Returns :: The list of sygus constraints.

void addSygusAssume ( const Term & term ) const 

Add a forumla to the set of Sygus assumptions.

SyGuS v2:

(assume <term>)

Parameters :: term – The formula to add as an assumption.

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

Get the list of sygus assumptions.

Returns :: The list of sygus assumptions.

void addSygusInvConstraint ( const Term & inv , const Term & pre , const Term & trans , const Term & post ) const 

Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.

SyGuS v2:

                (inv-constraint <inv> <pre> <trans> <post>)

               

Parameters :

inv – The function-to-synthesize.
pre – The pre-condition.
trans – The transition relation.
post – The post-condition.

SynthResult checkSynth ( ) const 

Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.

SyGuS v2:

(check-synth)

Returns :: The result of the check, which is “solution” if the check found a solution in which case solutions are available via getSynthSolutions, “no solution” if it was determined there is no solution, or “unknown” otherwise.

SynthResult checkSynthNext ( ) const 

Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. Must be called immediately after a successful call to check-synth or check-synth-next. Requires incremental mode.

SyGuS v2:

(check-synth-next)

Returns :: The result of the check, which is “solution” if the check found a solution in which case solutions are available via getSynthSolutions, “no solution” if it was determined there is no solution, or “unknown” otherwise.

Term getSynthSolution ( const Term & term ) const 

Get the synthesis solution of the given term. This function should be called immediately after the solver answers unsat for sygus input.

Parameters :: term – The term for which the synthesis solution is queried.
Returns :: The synthesis solution of the given term.

std :: vector < Term > getSynthSolutions ( const std :: vector < Term > & terms ) const 

Get the synthesis solutions of the given terms. This function should be called immediately after the solver answers unsat for sygus input.

Parameters :: terms – The terms for which the synthesis solutions is queried.
Returns :: The synthesis solutions of the given terms.

Term findSynth ( modes :: FindSynthTarget fst ) const 

Find a target term of interest using sygus enumeration, with no provided grammar.

The solver will infer which grammar to use in this call, which by default will be the grammars specified by the function(s)-to-synthesize in the current context.

SyGuS v2:

(find-synth :target)

Warning

This function is experimental and may change in future versions.

Parameters :: fst – The identifier specifying what kind of term to find
Returns :: The result of the find, which is the null term if this call failed.

Term findSynth ( modes :: FindSynthTarget fst , Grammar & grammar ) const 

Find a target term of interest using sygus enumeration with a provided grammar.

SyGuS v2:

                (find-synth :target G)

               

Warning

This function is experimental and may change in future versions.

Parameters :

fst – The identifier specifying what kind of term to find
grammar – The grammar for the term

Returns :

The result of the find, which is the null term if this call failed.

Term findSynthNext ( ) const 

Try to find a next target term of interest using sygus enumeration. Must be called immediately after a successful call to find-synth or find-synth-next.

SyGuS v2:

(find-synth-next)

Warning

This function is experimental and may change in future versions.

Returns :: The result of the find, which is the null term if this call failed.

Statistics getStatistics ( ) const 

Get a snapshot of the current state of the statistic values of this solver. The returned object is completely decoupled from the solver and will not change when the solver is used again.

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

void printStatisticsSafe ( int fd ) const : Print the statistics to the given file descriptor, suitable for usage in signal handlers.

bool isOutputOn ( const std :: string & tag ) const 

Determines if the output stream for the given tag is enabled. Tags can be enabled with the output option (and -o <tag> on the command line). Raises an exception when an invalid tag is given.

Returns :: True if the given tag is enabled.

std :: ostream & getOutput ( const std :: string & tag ) const 

Get an output stream for the given tag. Tags can be enabled with the output option (and -o <tag> on the command line). Raises an exception when an invalid tag is given.

Returns :: The output stream.

std :: string getVersion ( ) const 

Get a string representation of the version of this solver.

Returns :: The version string.

Friends

friend class parser::Cmd

friend class main::CommandExecutor