Produces a string representation.
Equations
- cvc5.Kind.instToString = { toString := cvc5.Kind.toString }
Equations
- cvc5.Kind.instHashable = { hash := cvc5.Kind.hash }
Produces a string representation.
Equations
- cvc5.SortKind.instToString = { toString := cvc5.SortKind.toString }
Equations
- cvc5.SortKind.instHashable = { hash := cvc5.SortKind.hash }
Produces a string representation.
Equations
- cvc5.ProofRule.instToString = { toString := cvc5.ProofRule.toString }
Equations
Produces a string representation.
Equations
- cvc5.SkolemId.instToString = { toString := cvc5.SkolemId.toString }
Equations
- cvc5.SkolemId.instHashable = { hash := cvc5.SkolemId.hash }
Produces a string representation.
Equations
Produces a hash.
Equations
Produces a string representation.
Equations
Produces a hash.
Equations
Produces a string representation.
Equations
- cvc5.RoundingMode.instToString = { toString := cvc5.RoundingMode.toString }
Produces a hash.
Equations
Produces a string representation.
Equations
Produces a hash.
Equations
Produces a string representation.
Equations
- cvc5.LearnedLitType.instToString = { toString := cvc5.LearnedLitType.toString }
Produces a hash.
Equations
Produces a string representation.
Equations
- cvc5.ProofComponent.instToString = { toString := cvc5.ProofComponent.toString }
Produces a hash.
Equations
Produces a string representation.
Equations
- cvc5.ProofFormat.instToString = { toString := cvc5.ProofFormat.toString }
Equations
Produces a string representation.
Equations
Produces a hash.
Equations
Produces a string representation.
Equations
- cvc5.InputLanguage.instToString = { toString := cvc5.InputLanguage.toString }
Produces a hash.
Equations
Encapsulation of a three-valued solver result, with explanations.
Equations
Instances For
Encapsulation of a three-valued solver result, with explanations.
Equations
Instances For
A cvc5 proof.
Proofs are trees and every proof object corresponds to the root step of a proof. The branches of the root step are the premises of the step.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
- cvc5.instReprError.repr cvc5.Error.missingValue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "cvc5.Error.missingValue")).group prec✝
Instances For
Equations
- cvc5.instReprError = { reprPrec := cvc5.instReprError.repr }
Cvc5 environment monad transformer.
Most monadic functions in this API use the non-transformer monad cvc5.Env, where m := BaseIO.
When using an EnvT m α, do make sure m is such that MonadLiftT BaseIO m which gives
MonadLiftT Env (EnvT m).
Equations
- cvc5.EnvT m α = ExceptT cvc5.Error m α
Instances For
String representation of an error.
Equations
Instances For
Panics on errors, otherwise yields the ok result.
Equations
- cvc5.Error.unwrap! (Except.ok a) = a
- cvc5.Error.unwrap! (Except.error e) = panicWithPosWithDecl "cvc5" "cvc5.Error.unwrap!" 343 14 e.toString
Instances For
Equations
- cvc5.Error.instToString = { toString := cvc5.Error.toString }
Manager for cvc5 terms.
Equations
Instances For
Constructor.
tmThe associated term manager instance.
A cvc5 datatype constructor declaration.
A datatype constructor declaration is a specification used for creating a datatype constructor.
Instances For
A string representation of this datatype constructor declaration.
Equations
A cvc5 datatype declaration.
A datatype declaration is not itself a datatype (see Datatype), but a specification for creating a
datatype sort.
The interface for a datatype declaration coincides with the syntax for the SMT-LIB 2.6 command
declare-datatype, or a single datatype within the declare-datatypes command.
Datatype sorts can be constructed from a DatatypeDecl using:
Solver.mkDatatypeSortSolver.mkDatatypeSorts
Equations
Instances For
Get a string representation of this datatype declaration.
Equations
- cvc5.DatatypeDecl.instToString = { toString := cvc5.DatatypeDecl.toString }
A cvc5 datatype selector.
Instances For
Gte the string representation of this datatype selector.
Equations
A cvc5 datatype constructor.
Instances For
A string representation of this datatype.
Equations
A cvc5 datatype.
Equations
Instances For
A string representation of this datatype.
Equations
- cvc5.Datatype.instToString = { toString := cvc5.Datatype.toString }
A Sygus Grammar.
This class can be used to define a context-free grammar of terms. Its interface coincides with the definition of grammars in the SyGuS IF 2.1 standard.
Equations
Instances For
A string representation of this grammar.
Equations
- cvc5.Grammar.instToString = { toString := cvc5.Grammar.toString }
Encapsulation of a command.
Commands are constructed by the InputParser and can be invoked on the Solver and
Command.
Equations
Instances For
Get a string representation of this command.
Equations
- cvc5.Command.instToString = { toString := cvc5.Command.toString }
Symbol manager.
Internally, this class manages a symbol table and other meta-information pertaining to SMT2 file inputs (e.g. named assertions, declared functions, etc.).
A symbol manager can be modified by invoking commands, see Command.invoke.
A symbol manager can be provided when constructing an InputParser, in which case that
InputParser has symbols of this symbol manager preloaded.
The symbol manager's interface is otherwise not publicly available.
Equations
Instances For
Constructor.
tmThe associated term manager instance.
This type is the main interface for retrieving commands and expressions from an input using a parser.
After construction, it is expected that an input is first configured via, e.g.,
InputParser.setFileInput, InputParser.setStreamInput, InputParser.setStringInput or
InputParser.setIncrementalStringInput and InputParser.appendIncrementalStringInput. Then,
functions InputParser.nextCommand and InputParser.nextExpression can be invoked to parse the
input.
The input parser interacts with a symbol manager, which determines which symbols are defined in the current context, based on the background logic and user-defined symbols. If no symbol manager is provided, then the input parser will construct (an initially empty) one.
If provided, the symbol manager must have a logic that is compatible with the provided solver. That
is, if both the solver and symbol manager have their logics set (SymbolManager.isLogicSet and
Solver.isLogicSet), then their logics must be the same.
Upon setting an input source, if either the solver (resp. symbol manager) has its logic set, then the symbol manager (resp. solver) is set to use that logic, if its logic is not already set.
Equations
Instances For
Construct an input parser.
solverThe solver (e.g. for constructing terms and sorts).smThe symbol manager, which contains a symbol table that maps symbols to terms and sorts. Must have a logic that is compatible with the solver.
Equations
- cvc5.InputParser.new solver = cvc5.InputParser.ofSolver✝ solver
- cvc5.InputParser.new solver (some sm) = cvc5.InputParser.ofSolverAndSM✝ solver sm
Instances For
Comparison for structural equality.
Equations
- cvc5.Result.instBEq = { beq := cvc5.Result.beq }
Equations
- cvc5.Result.instHashable = { hash := cvc5.Result.hash }
True if this result is from a satisfiable checkSat or checkSatAssuming query.
True if this result is from a unsatisfiable checkSat or checkSatAssuming query.
True if this result is from a checkSat or checkSatAssuming query and cvc5 was not able to
determine (un)satisfiability.
An explanation for an unknown query result.
Note that if the result is (un)sat, this function returns UnknownExplanation.UNKNOWN_REASON.
An explanation for an unknown query result, none if the result in not unknown.
Equations
Instances For
A string representation of this result.
Equations
- cvc5.Result.instToString = { toString := cvc5.Result.toString }
A string representation of this synthesis result.
Equations
- cvc5.SynthResult.instToString = { toString := cvc5.SynthResult.toString }
Hash function for synthesis results.
Equations
Equality of two synthesis results.
Equations
Determine if a given synthesis result is empty (a nullary result) and not an actual result returned from a synthesis query.
True if the synthesis query has a solution.
True if the synthesis query has no solution. In this case, it was determined that there was no solution.
True if the result of the synthesis query could not be determined.
The null datatype constructor declaration.
True if this DatatypeConstructorDecl is a null declaration.
Equality operator.
Equations
Hash function for datatype declarations.
Equations
Add datatype selector declaration.
nameThe name of the datatype selector declaration to add.sortThe codomain sort of the datatype selector declaration to add.
Add datatype selector declaration whose codomain type is the datatype itself.
nameThe name of the datatype selector declaration to add.
Add datatype selector declaration whose codomain sort is an unresolved datatype with the given name.
nameThe name of the datatype selector declaration to add.unresDatatypeNameThe name of the unresolved datatype. The codomain of the selector will be the resolved datatype with the given name
The null datatype declaration.
Equations
- cvc5.DatatypeDecl.instInhabited = { default := cvc5.DatatypeDecl.null () }
Determine if this datatype declaration is nullary.
Equality operator.
Equations
Hash function for datatype declarations.
Equations
Add datatype constructor declaration.
ctorThe datatype constructor declaration to add.
Get the number of constructors for this datatype declaration.
Determine if this datatype declaration is parametric.
Warning: this function is experimental and may change in future versions.
Get the name of this datatype declaration.
Equations
- v0.getName! = cvc5.Error.unwrap! v0.getName
Instances For
Get the name of this datatype declaration.
Instances For
Get the name of this datatype declaration.
Determine if this datatype declaration is resolved (has already been used to declare a datatype).
The null datatype constructor.
Equations
True if this datatype is a null object.
Equality operator.
Equations
Hash function for datatype selectors.
Equations
Get the name of this datatype selector.
Equations
- v0.getName! = cvc5.Error.unwrap! v0.getName
Instances For
Get the name of this datatype selector.
Instances For
Get the name of this datatype selector.
Get the selector term of this datatype selector.
Selector terms are a class of function-like terms of selector sort (Sort.isDatatypeSelector), and
should be used as the first argument of terms of kind Kind.APPLY_SELECTOR.
Get the updater term of this datatype selector.
Similar to selectors, updater terms are a class of function-like terms of updater sort
(Sort.isDatatypeUpdater), and should be used as the first argument of terms of kind
Kind.APPLY_UPDATER.
Get the codomain sort of this selector.
The null datatype constructor.
Equations
True if this datatype is a null object.
Equality operator.
Equations
Hash function for datatype constructors.
Equations
Get the name of this datatype constructor.
Get the name of this datatype constructor.
Instances For
Get the name of this datatype constructor.
Equations
- v0.getName! = cvc5.Error.unwrap! v0.getName
Instances For
Get the constructor term of this datatype constructor.
Datatype constructors are a special class of function-like terms whose sort is datatype constructor
(Sort.isDatatypeConstructor). All datatype constructors, including nullary ones, should be used as
the first argument to terms whose kind is Kind.APPLY_CONSTRUCTOR. For example, the nil list can
be constructor by tm.mkTerm Kind.APPLY_CONSTRUCTOR #[t], where tm is a TermManager and t is
the term returned by this function.
This function should not be used for parametric datatypes. Instead, use the function
DatatypeConstructor.getInstantiatedTerm.
Get the constructor term of this datatype constructor whose return type is retSort.
This function is intended to be used on constructors of parametric datatypes and can be seen as returning the constructor term that has been explicitly cast to the given sort.
This function is required for constructors of parametric datatypes whose return type cannot be determined by type inference. For example, given:
(declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
The type of nil terms must be provided by the user. In SMT version 2.6, this is done via the syntax for qualified identifiers:
(as nil (List Int))
This function is equivalent of applying the above, where this DatatypeConstructor is the one
corresponding to nil, and retSort is (List Int).
The returned constructor term t is used to construct the above (nullary) application of nil with
TermManager::mkTerm(Kind::APPLY_CONSTRUCTOR, {t}).
Warning: this function is experimental and may change in future versions.
retSortThe desired return sort of the constructor.
Get the tester term of this datatype constructor.
Similar to constructors, testers are a class of function-like terms of tester sort
(Sort.isDatatypeTester) which should be used as the first argument of terms of kind
Kind.APPLY_TESTER.
The number of selectors of this datatype constructor.
Get the datatype selector with the given name.
This is a linear search through the selectors, so in case of multiple, similarly-named selectors, the first is returned.
nameThe name of the datatype selector.
The datatype selector at index idx.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- cvc5.Datatype.instInhabited = { default := cvc5.Datatype.null () }
True if this datatype is a null object.
Equations
- cvc5.Datatype.instBEq = { beq := cvc5.Datatype.beq }
Hash function for datatypes.
Equations
- cvc5.Datatype.instHashable = { hash := cvc5.Datatype.hash }
Get the datatype constructor with the given name.
This is a linear search through the constructors, so in case of multiple, similarly-named constructors, the first is returned.
nameThe name of the datatype constructor.
Get the number of constructors of this datatype.
Get the datatype constructor at a given index.
idxThe index of the datatype constructor to return.
Equations
- cvc5.Datatype.instGetElemNatDatatypeConstructorLtGetNumConstructors = { getElem := fun (dt : cvc5.Datatype) (idx : Nat) (h : idx < dt.getNumConstructors) => dt.getConstructorAt ⟨idx, h⟩ }
Equations
- One or more equations did not get rendered due to their size.
Get the datatype selector with the given name.
This is a linear search through the constructors and their selectors, so in case of multiple, similarly-named selectors, the first is returned.
nameThe name of the datatype selector.
Determine if this datatype is parametric.
Warning: this function is experimental and may change in future versions.
Determine if this datatype corresponds to a co-datatype.
Determine if this datatype corresponds to a tuple.
Determine if this datatype corresponds to a record.
Warning: this function is experimental and may change in future versions.
Determine if this datatype is well-founded.
If this datatype is not a codatatype, this returns false if thre are no values of this datatype that are of finite size.
Equations
- cvc5.Sort.instInhabited = { default := cvc5.Sort.null () }
Comparison for structural equality.
Equations
- cvc5.Sort.instBEq = { beq := cvc5.Sort.beq }
Greater than or equal comparison.
Equations
- cvc5.Sort.instOrd = { compare := cvc5.Sort.compare }
Equations
- cvc5.Sort.instHashable = { hash := cvc5.Sort.hash }
Determine if this is the null sort (cvc5.Sort).
Determine if this is the Boolean sort (SMT-LIB: Bool).
Determine if this is the Integer sort (SMT-LIB: Int).
Determine if this is the Real sort (SMT-LIB: Real).
Determine if this is the String sort (SMT-LIB: String).
Determine if this is the regular expression sort (SMT-LIB: RegLan).
Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).
Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).
Determine if this is a floating-point sort (SMT-LIB: (_ FloatingPoint eb sb)).
Determine if this is a datatype sort.
Determine if this is a datatype constructor sort.
Determine if this is a datatype selector sort.
Determine if this is a datatype tester sort.
Determine if this is a datatype updater sort.
Determine if this is a function sort.
Determine if this is a predicate sort.
A predicate sort is a function sort that maps to the Boolean sort. All predicate sorts are also function sorts.
Determine if this is a tuple sort.
Determine if this is a nullable sort.
Determine if this is a record sort.
Warning: this function is experimental and may change in future versions.
Determine if this is an array sort.
Determine if this is a finite field sort.
Determine if this is a Sequence sort.
Determine if this is an abstract sort.
Determine if this is an uninterpreted sort.
Determine if this is an uninterpreted sort constructor.
An uninterpreted sort constructor has arity > 0 and can be instantiated to construct uninterpreted
sorts with given sort parameters.
Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.
An instantiated sort is a sort that has been constructed from instantiating a sort with sort
arguments --- see also cvc5.Sort.instantiate.
A string representation of this sort.
Equations
- cvc5.Sort.instToString = { toString := cvc5.Sort.toString }
Equations
- cvc5.Sort.instRepr = { reprPrec := fun (self : cvc5.Sort) (x : Nat) => Std.Format.text self.toString }
Determine if this term has a symbol (a name).
For example, free constants and variables have symbols.
Equations
Instances For
Determine if this term has a symbol (a name).
For example, free constants and variables have symbols.
Equations
- v0.hasSymbol? = v0.hasSymbol.toOption
Instances For
Get the symbol of this sort.
The symbol of this sort is the string that was provided when consrtucting it via one of
Solver.mkUninterpretedSort, Solver.mkUnresolvedSort, or
Solver.mkUninterpretedSortConstructorSort.
Equations
Instances For
Get the symbol of this sort.
The symbol of this sort is the string that was provided when consrtucting it via one of
Solver.mkUninterpretedSort, Solver.mkUnresolvedSort, or
Solver.mkUninterpretedSortConstructorSort.
Get the symbol of this sort.
The symbol of this sort is the string that was provided when consrtucting it via one of
Solver.mkUninterpretedSort, Solver.mkUnresolvedSort, or
Solver.mkUninterpretedSortConstructorSort.
Equations
- v0.getSymbol? = v0.getSymbol.toOption
Instances For
The arity of a function sort.
Equations
Instances For
The arity of a function sort.
Equations
Instances For
The domain sorts of a function sort.
Equations
Instances For
The domain sorts of a function sort.
Equations
Instances For
The codomain sort of a function sort.
Equations
Instances For
The codomain sort of a function sort.
Equations
Instances For
The array index sort of an array index.
Equations
Instances For
The array index sort of an array index.
Equations
Instances For
The array element sort of an array index.
Equations
Instances For
The array element sort of an array index.
Equations
Instances For
The element sort of a set sort.
Equations
Instances For
The element sort of a set sort.
Equations
Instances For
The element sort of a bag sort.
Equations
Instances For
The element sort of a bag sort.
Equations
Instances For
The element sort of a sequence sort.
Equations
Instances For
The element sort of a sequence sort.
Equations
Instances For
The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.
Equations
Instances For
The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.
Equations
Instances For
The arity of an uninterpreted sort constructor sort.
Equations
Instances For
The arity of an uninterpreted sort constructor sort.
Equations
Instances For
The bit-width of the bit-vector sort.
Equations
Instances For
The bit-width of the bit-vector sort.
Equations
Instances For
The size of the finite field sort.
Equations
Instances For
The size of the finite field sort.
Equations
Instances For
The bit-width of the exponent of the floating-point sort.
Instances For
The bit-width of the exponent of the floating-point sort.
Equations
Instances For
The width of the significand of the floating-point sort.
Equations
Instances For
The width of the significand of the floating-point sort.
Equations
Instances For
The length of a tuple sort.
Equations
Instances For
The length of a tuple sort.
Equations
Instances For
The element sorts of a tuple sort.
Equations
- v0.getTupleSorts? = v0.getTupleSorts.toOption
Instances For
The element sorts of a tuple sort.
Equations
Instances For
The element sort of a nullable sort.
Equations
Instances For
The element sort of a nullable sort.
Equations
Instances For
Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
Equations
Instances For
Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
Equations
Instances For
Get the underlying datatype of a datatype sort.
Equations
Instances For
Get the underlying datatype of a datatype sort.
Equations
- v0.getDatatype? = v0.getDatatype.toOption
Instances For
Get the sorts used to instantiate the sort parameters of a parametric sort.
A parametric sort is a parametric datatype or an uninterpreted sort constructor sort.
See cvc5.Sort.instantiate.
Equations
Instances For
Get the sorts used to instantiate the sort parameters of a parametric sort.
A parametric sort is a parametric datatype or an uninterpreted sort constructor sort.
See cvc5.Sort.instantiate.
Equations
Instances For
Get the sorts used to instantiate the sort parameters of a parametric sort.
A parametric sort is a parametric datatype or an uninterpreted sort constructor sort.
See cvc5.Sort.instantiate.
Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
Create sort parameters with mkParamSort symbol.
paramsThe list of sort parameters to instantiate with.
Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
Create sort parameters with mkParamSort symbol.
paramsThe list of sort parameters to instantiate with.
Equations
- v0.instantiate? v1 = (v0.instantiate v1).toOption
Instances For
Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
Create sort parameters with mkParamSort symbol.
paramsThe list of sort parameters to instantiate with.
Equations
- v0.instantiate! v1 = cvc5.Error.unwrap! (v0.instantiate v1)
Instances For
Simultaneous substitution of Sorts.
Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sorts contains duplicates, the replacement earliest in
the vector takes priority.
Warning: This function is experimental and may change in future versions.
sortsThe sub-sorts to be substituted within this sort.replacementsThe sort replacing the substituted sub-sorts.
Equations
- v0.substitute? v1 v2 = (v0.substitute v1 v2).toOption
Instances For
Simultaneous substitution of Sorts.
Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sorts contains duplicates, the replacement earliest in
the vector takes priority.
Warning: This function is experimental and may change in future versions.
sortsThe sub-sorts to be substituted within this sort.replacementsThe sort replacing the substituted sub-sorts.
Simultaneous substitution of Sorts.
Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sorts contains duplicates, the replacement earliest in
the vector takes priority.
Warning: This function is experimental and may change in future versions.
sortsThe sub-sorts to be substituted within this sort.replacementsThe sort replacing the substituted sub-sorts.
Equations
- v0.substitute! v1 v2 = cvc5.Error.unwrap! (v0.substitute v1 v2)
Instances For
The arity of a datatype constructor sort.
Instances For
The arity of a datatype constructor sort.
Equations
Instances For
The domain sorts of a datatype constructor sort.
Instances For
The domain sorts of a datatype constructor sort.
Equations
Instances For
The codomain sort of a constructor sort.
Equations
Instances For
The codomain sort of a constructor sort.
Instances For
The domain sort of a datatype selector sort.
Instances For
The domain sort of a datatype selector sort.
Equations
Instances For
The codomain sort of a datatype selector sort.
Equations
Instances For
The codomain sort of a datatype selector sort.
Equations
Instances For
The domain sort of a datatype tester sort.
Instances For
The domain sort of a datatype tester sort.
Equations
Instances For
The codomain sort of a datatype tester sort.
Instances For
The codomain sort of a datatype tester sort.
Equations
Instances For
Get the arity of a datatype sort.
Number of type parameters if the datatype is parametric, 0 otherwise.
Equations
Instances For
Get the arity of a datatype sort.
Number of type parameters if the datatype is parametric, 0 otherwise.
Equations
Instances For
Equations
- cvc5.Op.instInhabited = { default := cvc5.Op.null () }
Equations
- cvc5.Op.instHashable = { hash := cvc5.Op.hash }
Equations
- cvc5.Op.instBEq = { beq := cvc5.Op.beq }
Determine if this operator is indexed.
Get the number of indices of this operator.
Get the index at position i of an indexed operator.
Get the string representation of this operator.
Equations
- cvc5.Op.instToString = { toString := cvc5.Op.toString }
Equations
- cvc5.Term.instInhabited = { default := cvc5.Term.null () }
Equations
- cvc5.Term.instBEq = { beq := cvc5.Term.beq }
Equations
- cvc5.Term.instOrd = { compare := cvc5.Term.compare }
Equations
- cvc5.Term.instHashable = { hash := cvc5.Term.hash }
Simultaneously replace terms with replacements in term.
terms: The terms to replace.replacements: The replacement terms.
In the case that terms contains duplicates, the replacement earliest in the array takes priority.
For example, calling substitute on f(x, y) with
terms := #[x, z]replacements := #[g(z), w]results in the termf(g(z), y).
NB: requires that terms and replacements are of equal size (they are interpreted as a 1:1
mapping).
NB: this replacement is applied during a pre-order traversal and only once (it is not run until fixed point).
Determine if this term has an operator.
Determine if this term has a symbol (a name).
For example, free constants and variables have symbols.
Equations
- v0.hasSymbol? = v0.hasSymbol.toOption
Instances For
Determine if this term has a symbol (a name).
For example, free constants and variables have symbols.
Equations
Instances For
Get the number of children of this term.
Equations
Instances For
Get the child term of this term at a given index.
Get the operator of a term with an operator.
Requires that this term has an operator (see hasOp).
Equations
- v0.getOp! = cvc5.Error.unwrap! v0.getOp
Instances For
Boolean and.
t1: A Boolean term.t2: A Boolean term.
Boolean or.
t1: A Boolean term.t2: A Boolean term.
Boolean exclusive or.
t1: A Boolean term.t2: A Boolean term.
Boolean implication.
t1: A Boolean term.t2: A Boolean term.
If-then-else.
cnd: The condition, a Boolean term.thn: The then term.els: The else term.
Get the sign of an integer or real value.
Returns 0 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.
NB: requires that this term is an integer or real value.
Equations
Instances For
Get the sign of an integer or real value.
Returns 0 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.
NB: requires that this term is an integer or real value.
Equations
Instances For
Get the sign of an integer or real value.
Returns 0 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.
NB: requires that this term is an integer or real value.
Determine if this term is an Int32 value.
NB: this will return true for integer constants and real constants that have integer value.
Get the Int32 representation of this integral value.
NB: requires that this term is an Int32 value (see isInt32Value).
Equations
- v0.getInt32Value? = v0.getInt32Value.toOption
Instances For
Get the Int32 representation of this integral value.
NB: requires that this term is an Int32 value (see isInt32Value).
Get the Int32 representation of this integral value.
NB: requires that this term is an Int32 value (see isInt32Value).
Equations
Instances For
Determine if this term is an UInt32 value.
NB: this will return true for integer constants and real constants that have integer value.
Get the UInt32 representation of this integral value.
NB: requires that this term is an UInt32 value (see isUInt32Value).
Get the UInt32 representation of this integral value.
NB: requires that this term is an UInt32 value (see isUInt32Value).
Equations
Instances For
Get the UInt32 representation of this integral value.
NB: requires that this term is an UInt32 value (see isUInt32Value).
Equations
Instances For
Determine if this term is an Int64 value.
NB: this will return true for integer constants and real constants that have integer value.
Get the Int64 representation of this integral value.
NB: requires that this term is an Int64 value (see isInt64Value).
Equations
- v0.getInt64Value? = v0.getInt64Value.toOption
Instances For
Get the Int64 representation of this integral value.
NB: requires that this term is an Int64 value (see isInt64Value).
Get the Int64 representation of this integral value.
NB: requires that this term is an Int64 value (see isInt64Value).
Equations
Instances For
Determine if this term is an UInt64 value.
NB: this will return true for integer constants and real constants that have integer value.
Get the UInt64 representation of this integral value.
NB: requires that this term is an UInt64 value (see isUInt64Value).
Get the UInt64 representation of this integral value.
NB: requires that this term is an UInt64 value (see isUInt64Value).
Equations
Instances For
Get the UInt64 representation of this integral value.
NB: requires that this term is an UInt64 value (see isUInt64Value).
Equations
Instances For
Determine if this real/integer constant term is an integral value.
Get the native integral value of an integral value.
Equations
Instances For
Get the native integral value of an integral value.
Equations
Instances For
Get the native integral value of an integral value.
Get the 32 bit integer representations of the numerator and denominator of a rational value.
NB: Requires that this term is a rational value and its numerator and denominator fit into 32
bit integer values (see Term.isReal32Value).
Get the 64 bit integer representations of the numerator and denominator of a rational value.
NB: Requires that this term is a rational value and its numerator and denominator fit into 64
bit integer values (see Term.isReal64Value).
Determine if this term is a rational value.
NB: A term of kind Kind.PI is not considered to be a real value.
Get a string representation of this rational value.
NB: Requires that this term is a rational value (see Term.isRealValue).
Get a string representation of this rational value.
NB: Requires that this term is a rational value (see Term.isRealValue).
Equations
- v0.getRealValue? = v0.getRealValue.toOption
Instances For
Get a string representation of this rational value.
NB: Requires that this term is a rational value (see Term.isRealValue).
Equations
Instances For
Get the native rational value of a real, rational-compatible value.
Equations
Instances For
Get the native rational value of a real, rational-compatible value.
Equations
Instances For
Determine if this term is a constant array.
Determine the base (element stored at all indices) of a constant array.
NB: requires that this term is a constant array (see isConstArray).
Equations
Instances For
Determine the base (element stored at all indices) of a constant array.
NB: requires that this term is a constant array (see isConstArray).
Determine the base (element stored at all indices) of a constant array.
NB: requires that this term is a constant array (see isConstArray).
Equations
Instances For
Determine if this term is a Boolean value.
Get the value of a Boolean term as a native Boolean value.
Requires term to have sort Bool.
Equations
Instances For
Get the value of a Boolean term as a native Boolean value.
Requires term to have sort Bool.
Equations
Instances For
Determine if this term is a bit-vector value.
Get the string representation of a bit-vector value.
Requires term to have a bit-vector sort.
base:2for binary,10for decimal, and16for hexadecimal.
Equations
- v0.getBitVectorValue? v1 = (v0.getBitVectorValue v1).toOption
Instances For
Get the string representation of a bit-vector value.
Requires term to have a bit-vector sort.
base:2for binary,10for decimal, and16for hexadecimal.
Equations
- v0.getBitVectorValue! v1 = cvc5.Error.unwrap! (v0.getBitVectorValue v1)
Instances For
Determine if this term is a finite field value.
Get the integer representation of a finite field value (base 10).
NB: asserts isFiniteFieldValue.
NB: uses the integer representative of smallest absolute value.
Equations
Instances For
Get the integer representation of a finite field value (base 10).
NB: asserts isFiniteFieldValue.
NB: uses the integer representative of smallest absolute value.
Equations
Instances For
Get the integer representation of a finite field value (base 10).
NB: asserts isFiniteFieldValue.
NB: uses the integer representative of smallest absolute value.
Determine if this term is an uninterpreted sort value.
Get a string representation of an uninterpreted sort value.
NB: asserts isUninterpretedSortValue.
Equations
Instances For
Get a string representation of an uninterpreted sort value.
NB: asserts isUninterpretedSortValue.
Get a string representation of an uninterpreted sort value.
NB: asserts isUninterpretedSortValue.
Equations
Instances For
Determine if this term is a tuple value.
Get a tuple value as a vector of terms.
NB: asserts isTupleValue.
Equations
- v0.getTupleValue? = v0.getTupleValue.toOption
Instances For
Determine if this term is a floating-point rounding mode value.
Get the RoundingMode value of a given rounding-mode value term.
NB: asserts isRoundingModeValue.
Get the RoundingMode value of a given rounding-mode value term.
NB: asserts isRoundingModeValue.
Equations
Instances For
Get the RoundingMode value of a given rounding-mode value term.
NB: asserts isRoundingModeValue.
Equations
Instances For
Determine if this term is a floating-point positive zero value (+zero).
Determine if this term is a floating-point negative zero value (-zero).
Determine if this term is a floating-point positive infinity value (+oo).
Determine if this term is a floating-point negative infinity value (-oo).
Determine if this term is a floating-point NaN.
Determine if this term is a floating-point value.
Get the representation of a floating-point value.
Returns a tuple of the floating-point value's exponent width, significand width, and a bit-vector value term.
NB: asserts isFloatingPointValue.
Equations
Instances For
Get the representation of a floating-point value.
Returns a tuple of the floating-point value's exponent width, significand width, and a bit-vector value term.
NB: asserts isFloatingPointValue.
Equations
Instances For
Get the representation of a floating-point value.
Returns a tuple of the floating-point value's exponent width, significand width, and a bit-vector value term.
NB: asserts isFloatingPointValue.
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 whole AST is:
(union (singleton c_1) ... (union (singleton c_{n-1}) (singleton c_n))))
where c_1 ... c_n are values ordered by id such that c_1 > ... > c_n.
NB: a universe set term (Kind.SET_UNIVERSE) is not considered to be a set value.
Get a set value as an array of terms.
NB: asserts isSetValue.
Equations
- v0.getSetValue? = v0.getSetValue.toOption
Instances For
Determine if this term is a sequence value.
A term is a sequence value if it has kind 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 array #[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 as Solver.getValue and Solver.simplify.
Get a sequence value as a vector of terms.
Equations
Instances For
Get a sequence value as a vector of terms.
Equations
Instances For
Determine if this term is a cardinality constraint.
Equations
Instances For
Get a cardinality constraint as a pair of its sort and upper bound.
NB: asserts isCardinalityConstraint.
Equations
Instances For
Get a cardinality constraint as a pair of its sort and upper bound.
NB: asserts isCardinalityConstraint.
Get a cardinality constraint as a pair of its sort and upper bound.
NB: asserts isCardinalityConstraint.
Equations
Instances For
Determine if this term is a real algebraic number.
Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable.
NB: asserts isRealAlgebraicNumber.
vThe variable over which to express the polynomial.
Equations
Instances For
Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable.
NB: asserts isRealAlgebraicNumber.
vThe variable over which to express the polynomial.
Get the defining polynomial for a real algebraic number term, expressed in terms of the given variable.
NB: asserts isRealAlgebraicNumber.
vThe variable over which to express the polynomial.
Equations
Instances For
Get the lower bound for a real algebraic number value.
NB: asserts isRealAlgebraicNumber.
Instances For
Get the lower bound for a real algebraic number value.
NB: asserts isRealAlgebraicNumber.
Get the lower bound for a real algebraic number value.
NB: asserts isRealAlgebraicNumber.
Equations
Instances For
Get the upper bound for a real algebraic number value.
NB: asserts isRealAlgebraicNumber.
Equations
Instances For
Get the upper bound for a real algebraic number value.
NB: asserts isRealAlgebraicNumber.
Instances For
Get the upper bound for a real algebraic number value.
NB: asserts isRealAlgebraicNumber.
Get skolem identifier of this term.
Requires isSkolem.
Equations
- v0.getSkolemId? = v0.getSkolemId.toOption
Instances For
Get the skolem indices of this term.
Requires isSkolem.
Returns the skolem indices of this term. This is a 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.
Equations
Instances For
Get the skolem indices of this term.
Requires isSkolem.
Returns the skolem indices of this term. This is a 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.
Get the skolem indices of this term.
Requires isSkolem.
Returns the skolem indices of this term. This is a 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.
Equations
Instances For
Equations
- t.forIn b f = cvc5.Term.forIn.loop✝ t f t.getNumChildren ⋯ b
Instances For
Equations
- cvc5.Term.instForInOfMonad = { forIn := fun {β : Type ?u.2} => cvc5.Term.forIn }
Get the children of a term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A string representation of this term.
Equations
- cvc5.Term.instToString = { toString := cvc5.Term.toString }
Equations
- cvc5.Proof.instInhabited = { default := cvc5.Proof.null () }
Get the proof rule used by the root step of the root.
Get the proof rewrite rule used by the root step of the proof.
Requires that getRule does not return ProofRule.DSL_REWRITE or ProofRule.REWRITE.
Equations
Instances For
Get the proof rewrite rule used by the root step of the proof.
Requires that getRule does not return ProofRule.DSL_REWRITE or ProofRule.REWRITE.
Get the proof rewrite rule used by the root step of the proof.
Requires that getRule does not return ProofRule.DSL_REWRITE or ProofRule.REWRITE.
Equations
Instances For
The conclusion of the root step of the proof.
The premises of the root step of the proof.
The arguments of the root step of the proof as a vector of terms.
Some of those terms might be strings.
Operator overloading for referential equality of two proofs.
Equations
- cvc5.Proof.instBEq = { beq := cvc5.Proof.beq }
Equations
- cvc5.Proof.instHashable = { hash := cvc5.Proof.hash }
Get the Boolean sort.
Get the Integer sort.
Get the Real sort.
Get the regular expression sort.
Get the rounding mode sort.
Get the string sort.
Create an array sort.
indexSortThe array index sort.elemSortThe array element sort.
Create a bit-vector sort.
sizeThe bit-width of the bit-vector sort.
Create a floating-point sort.
expThe bit-width of the exponent of the floating-point sort.sigThe bit-width of the significand of the floating-point sort.
Create a finite-field sort from a given string of base n.
sizeThe modulus of the field. Must be a prime.baseThe base of the string representation ofsize.
Create a finite-field sort.
sizeThe modulus of the field in base 10. Must be a prime.
Equations
- tm.mkFiniteFieldSort size = tm.mkFiniteFieldSortOfString (toString size)
Instances For
Create function sort.
sortsThe sort of the function arguments.codomainThe sort of the function return value.
Create a skolem.
id: The skolem identifier.indices: The indices of the skolem.
Get the number of indices for a skolem id.
id: The skolem id.
Equations
- v0.getNumIndicesForSkolemId! v1 = cvc5.Error.unwrap! (v0.getNumIndicesForSkolemId v1)
Instances For
Get the number of indices for a skolem id.
id: The skolem id.
Get the number of indices for a skolem id.
id: The skolem id.
Equations
- v0.getNumIndicesForSkolemId? v1 = (v0.getNumIndicesForSkolemId v1).toOption
Instances For
Create a predicate sort.
This is equivalent to calling mkFunctionSort with Boolean sort as the codomain.
sortsThe list of sorts of the predicate.
Create a tuple sort.
sortsThe sorts of the elements of the tuple.
Create a record sort.
Warning: This function is experimental and may change in future versions.
fieldsThe list of fields of the record.
Create an uninterpreted sort constructor sort.
An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
arityThe arity of the sort (must be > 0).symbolThe symbol of the sort.
Create a set parameter.
elemSortThe sort of the set elements.
Create a set parameter.
elemSortThe sort of the set elements.
Create a set parameter.
elemSortThe sort of the set elements.
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
arguments sorts. For example, SortKind.ARRAY_SORT and SortKind.BITVECTOR_SORT can be passed as
the kind k to this function, while SortKind.INTEGER_SORT and SortKind.STRING_SORT cannot.
NB: Providing the kind SortKind.ABSTRACT_SORT as an argument to this function returns the
(fully) unspecified sort, denoted ?.
NB: 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 SortKind.ARRAY_SORT.
Create an uninterpreted sort.
symbolThe name of the sort.
Create an unresolved datatype sort.
This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.
symbolThe name of the sort.arityThe number of sort parameters of the sort.
Create a nullable sort.
sortThe sort of the element of the nullable.
Create a sort parameter.
symbolThe name of the sort.
Warning: This function is experimental and may change in future versions.
Create a Boolean constant.
b: The Boolean constant.
Create a Boolean true constant.
Create a Boolean false constant.
Create a constant representing the number Pi.
Create an integer-value term.
s: the string representation of the constant, may represent an integer such as ("123").
Create a real-value term.
s: the string representation of the constant, may represent an integer ("123") or a real constant ("12.34","12/34").
Create a real-value term from numerator/denominator Int-s.
Equations
Instances For
Create a regular expression all (re.all) term.
Create a regular expression allchar (re.allchar) term.
Create a regular expression none (re.none) term.
Create a constant representing an empty set of the given sort.
sortThe sort of the set elements.
Create a constant representing an empty bag of the given sort.
sortThe sort of the bag elements.
Create a separation logic empty term.
Create a separation logic nil term.
sortThe sort of the nil term.
Warning: this function is experimental and may change in future versions.
Create a string constant from a String.
The string may contain SMT-LIB-compatible escape sequences like \u1234 to encode unicode
characters.
sThe string this constant represents.useEscSequencesDetermines whether escape sequences insshould be converted to the corresponding unicode characters, defaultfalse.
Create an empty sequence of the given element sort.
sortThe element sort of the sequence.
Create a universe set of the given sort.
sortThe sort of the set elements.
Create a bit-vector constant of given size and value.
The given value must fit into a bit-vector of the given size.
sizeThe bit-width of the bit-vector sort.valThe value of the constant.
Create a bit-vector constant of a given bit-width from a given string of base 2, 10, or 16.
The given value must fit into a bit-vector of the given size.
sizeThe bit-width of the bit-vector sort.sThe string representation of the constant.valThe base of the string representation:2for binary,10for decimal, and16for hexadecimal.
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 range [0,size). If it is outside this
range, it will be reduced modulo size before being constructed.
valueThe string representation of the constant.sortThe field sort.baseThe base of the string representation ofvalue, default10.
Equations
- tm.mkFiniteFieldElem value sort = tm.mkFiniteFieldElemOfString (toString value) sort
Instances For
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 range [0,size). If it is outside this
range, it will be reduced modulo size before being constructed.
valueThe string representation of the constant.sortThe field sort.baseThe base of the string representation ofvalue, default10.
Create a constant array with the provided constant value stored at every index.
sortThe sort of the constant array (must be an array sort).valThe constant value to store (must match the sort's element sort).
Create a positive infinity floating-point constant (SMT-LIB: +oo).
expNumber of bits in the exponent.sigNumber of bits in the significand.
Create a negative infinity floating-point constant (SMT-LIB: -oo).
expNumber of bits in the exponent.sigNumber of bits in the significand.
Create a not-a-number floating-point constant (SMT-LIB: NaN).
expNumber of bits in the exponent.sigNumber of bits in the significand.
Create a positive zero floating-point constant (SMT-LIB: +zero).
expNumber of bits in the exponent.sigNumber of bits in the significand.
Create a negative zero floating-point constant (SMT-LIB: -zero).
expNumber of bits in the exponent.sigNumber of bits in the significand.
Create a rounding mode value.
rmThe floating point rounding mode this constant represents.
Create a floating-point value from a bit-vector given in IEEE-754 format.
expSize of the exponent.sigSize of the significand.valValue of the floating-point constant as a bit-vector term.
Create a floating-point value from its three IEEE-754 bit-vector value components.
signThe sign bit.expThe bit-vector representing the exponent.sigThe bit-vector representing the significand.
Create a cardinality constraint for an uninterpreted sort.
Warning: this function is experimental and may change in future versions.
sortThe sort the cardinality constraint is for.upperBoundThe upper bound on the cardinality of the sort.
Create a tuple term.
termsThe elements in the tuple.
Create a nullable some term.
termThe element value.
Create a selector for nullable term.
termA nullable term.
Create a null tester for a nullable term.
termA nullable term.
Create a some tester for a nullable term.
termA nullable term.
Create a constant representing a null of the given sort.
sortThe sort of the nullable element.
Create a term that lifts kind to nullable terms.
kindThe lifted operator.argsThe arguments of the lifted operator.
Example: if we have the term ((_ nullable.lift +) x y), with x and y of type (Nullable Int),
then kind would be Kind.ADD, and args would be #[x, y]. This function would return
(nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)
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.
sortThe sort of the constant.symbolThe name of the constant (optional).
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 mkVar.
sortThe sort of the variable.symbolThe name of the variable (optional).
Create operator of Kind:
Kind.BITVECTOR_EXTRACTKind.BITVECTOR_REPEATKind.BITVECTOR_ROTATE_LEFTKind.BITVECTOR_ROTATE_RIGHTKind.BITVECTOR_SIGN_EXTENDKind.BITVECTOR_ZERO_EXTENDKind.DIVISIBLEKind.FLOATINGPOINT_TO_FP_FROM_FPKind.FLOATINGPOINT_TO_FP_FROM_IEEE_BVKind.FLOATINGPOINT_TO_FP_FROM_REALKind.FLOATINGPOINT_TO_FP_FROM_SBVKind.FLOATINGPOINT_TO_FP_FROM_UBVKind.FLOATINGPOINT_TO_SBVKind.FLOATINGPOINT_TO_UBVKind.INT_TO_BITVECTORKind.TUPLE_PROJECT
See cvc5.Kind for a description of the parameters.
kindThe kind of the operator.argsThe arguments (indices) of the operator.
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.
Equations
Instances For
Create operator of Kind:
Kind.BITVECTOR_EXTRACTKind.BITVECTOR_REPEATKind.BITVECTOR_ROTATE_LEFTKind.BITVECTOR_ROTATE_RIGHTKind.BITVECTOR_SIGN_EXTENDKind.BITVECTOR_ZERO_EXTENDKind.DIVISIBLEKind.FLOATINGPOINT_TO_FP_FROM_FPKind.FLOATINGPOINT_TO_FP_FROM_IEEE_BVKind.FLOATINGPOINT_TO_FP_FROM_REALKind.FLOATINGPOINT_TO_FP_FROM_SBVKind.FLOATINGPOINT_TO_FP_FROM_UBVKind.FLOATINGPOINT_TO_SBVKind.FLOATINGPOINT_TO_UBVKind.INT_TO_BITVECTORKind.TUPLE_PROJECT
See cvc5.Kind for a description of the parameters.
kindThe kind of the operator.argsThe arguments (indices) of the operator.
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.
Create operator of kind Kind.DIVISIBLE to support arbitrary precision integers.
See cvc5.Kind for a description of the parameters.
kindThe kind of the operator.argThe string argument to this operator.
Create a datatype constructor declaration.
nameThe name of the datatype constructor.
Create a datatype declaration.
nameThe name of the datatype.paramsA list of sort parameters.isCoDatatypeTrue if a codatatype is to be constructed.
Create a datatype sort.
dtypeDeclThe datatype declaration from which the sort is created.
Create a vector of datatype sorts.
The names of the datatype declarations must be distinct.
dtypeDeclsThe datatype declarations from which the sort is created.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Runs Env code in the IO monad, throws cvc5.Errors as IO.Errors.
Equations
- code.runIO = do let __do_lift ← liftM code.run match __do_lift with | Except.ok res => pure res | Except.error e => throw (IO.Error.userError (toString e))
Instances For
Determine if this is the null grammar.
Physical equality of two grammars.
Equations
- cvc5.Grammar.instBEq = { beq := cvc5.Grammar.beq }
Equations
- cvc5.Grammar.instHashable = { hash := cvc5.Grammar.hash }
True if the command is null.
Get the name for this command, e.g., "assert".
Invoke the command on the solver and symbol manager sm, prints the result to a string.
solverThe solver to invoke the command on.smThe symbol manager to invoke the command on.
Determine if the logic of this symbol manager has been set.
Get the logic configured for this symbol manager.
Asserts SymbolManager.isLogicSet.
Get the list of sorts that have been declared via declare-sort commands.
These are the sorts that are printed as part of a response to a get-model command.
Get the list of terms that have been declared via declare-fun and declare-const.
These are the terms that are printed in response to a get-model command.
Get a mapping from terms to names that have been given to them via the :named attribute.
Get the associated symbol manager of this input parser.
Is this parser done reading input?
Configure given file as input.
fileNameThe name of the file to configure.langThe input language of the input string, defaultInputLanguage::SMT_LIB_2_6.
Configure a given concrete input string as the input to this parser.
inputThe input string.langThe input language of the input string, defaultInputLanguage::SMT_LIB_2_6.nameThe name to use as input stream name for error messages, default"lean-cvc5".
Configure that we will be feeding strings to this parser via appendIncrementalStringInput.
langThe input language, defaultInputLanguage::SMT_LIB_2_6.nameThe name of the stream, for use in error messages, default"lean-cvc5".
Append string to the input being parsed by this parser. Should be called after calling
setIncrementalStringInput.
inputThe input string.
Parse and returns the next command if any, or none if the parser is at end-of-input.
Equations
Instances For
Parse and return the next command.
Will initialize the logic to "ALL" or the forced logic if no logic is set prior to this point and a command is read that requires initializing the logic.
Parse and return the next term. Requires setting the logic prior to this point.
Get a string representation of the version of this solver.
Remove all assertions.
Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables.
If applySubs is true, then for example, if (= x 0) was asserted to this solver, this function
may replace occurrences of x with 0.
tThe term to simplify.applySubsTrue to apply substitutions for solved variables.
Declare n-ary function symbol.
SMT-LIB:
\verbatim embed:rst:leading-asterisk .. code:: smtlib
(declare-fun <symbol> ( <sort>* ) <sort>)
\endverbatim
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.
Check satisfiability.
Declare uninterpreted sort.
(declare-sort <symbol> <numeral>)
symbol: The name of the sort.arity: The arity of the sort.fresh: If true, then this function always returns a new sort. Otherwise, it will always return the same sort for each call with the given arity and symbol wherefreshisfalse.
Define n-ary function.
(define-fun <function_def>)
symbol: The name of the function.boundVars: The parameters to this function.sort: The sort of the return value of this function.body: The function body.global: Determines whether this definition is global (i.e. persists when popping the context).
Define recursive function.
(define-fun-rec <function_def>)
symbol: The name of the function.boundVars: The parameters to this function.sort: The sort of the return value of this function.body: The function body.global: Determines whether this definition is global (i.e. persists when popping the context).
Define recursive function.
(define-fun-rec <function_def>)
Create parameter fn with TermManager.mkConst.
fn: The sorted function.bound_vars: The parameters to this function.termThe function body.globalDetermines whether this definition is global (i.e. persists when popping the context).
Define recursive functions.
(define-funs-rec
( <function_decl>_1 ... <function_decl>_n )
( <body>_1 ... <body>_n )
)
funs: The sorted functions, each created withTermManager.mkConst.boundVars: The list of parameters to the functions.bodies: The list of function bodies of the functions.global: Determines whether this definition is global (i.e. persists when popping the context).
Create datatype sort.
(declare-datatype <symbol> <datatype_decl>)
symbol: The name of the datatype sort.ctors: The constructor declarations of the datatype sort.
Get the unsatisfiable core.
SMT-LIB:
\verbatim embed:rst:leading-asterisk .. code:: smtlib
(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.
Get the lemmas used to derive unsatisfiability.
(get-unsat-core-lemmas)
Requires the SAT proof unsat core mode, so to enable option unsat-cores-mode=sat-proof.
Warning: this function is experimental and may change in future versions.
Get a timeout core.
This function computes a subset of the current assertions that couse a timeout. It may make multiple
checks for satisfiability internally, each limited by the timeout value given by
timeout-core-timeout.
If the result is unknown and the reason is timeout, then returned the set of assertions corresponds
to a subset of the current assertions that cause a timeout in the specified time
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 returned set of assertions is empty.
(get-timeout-core)
Warning: this function is experimental and may change in future versions.
Get a timeout core of the given assumptions.
This function computes a subset of the current assertions that couse a timeout when added to the
current assertions timeout-core-timeout.
If the result is unknown and the reason is timeout, then returned the set of assertions corresponds
to a subset of the given assertions that cause a timeout when added to the current assertions in the
specified time timeout-core-timeout. If the result is unsat, then the set of assumptions together
with 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 returned set of assertions is empty.
NB: this command does not require being preceeded by a call to checkSat.
(get-timeout-core (<assert>*))
Warning: this function is experimental and may change in future versions.
Get a proof associated with the most recent call to checkSat.
Requires to enable option produce-proofs.
(get-proof :c)
NB: requires to enable option produce-proofs.
Warning: this function is experimental and may change in future versions.
c: The component of the proof to return.
Get the values of the given terms in the current model.
SMT-LIB:
\verbatim embed:rst:leading-asterisk .. code:: smtlib
(get-value ( <term>* ))
\endverbatim
terms: The terms for which the values are queried.
Get the domain elements of an uninterpreted sort in the current model.
The current model interprets the uninterpreted sort s as a finite sort whose domain elements are given in the return value of this function.
s: The uninterpreted sort in question.
Determine if the model value of the given free constant was essential for showing
satisfiability of the last checkSat query based on the current model.
For any free constant v, this will only return false if model-cores has been set to true.
Warning: this function is experimental and may change in future versions.
v: The term in question.
Get the model.
(get-model)
Requires to enable option produce-models.
Warning: this function is experimental and may change in future versions.
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 onisModelCoreSymbol.
Do quantifier elimination.
(get-qe <q>)
NB: Quantifier elimination is only complete for logics such as LRA, LIA, and BV.
Warning: this function is experimental and may change in future versions.
q: A quantified formula of the formQX_1 ... QX_n, P(x_1...x_i, y_1...y_j)whereQXis a set of quantified variables of the formQ x_1...x_kandP(x_1...x_i, y_1...y_j)is a quantifier-free formula.
Returns a formula Φ such that, given the current set of formulas A asserted to this solver:
(a ∧ Q)and (A ∧ Φ) are equivalent, andΦis a quantifier-free formula containing only free variables iny_1...y_n.
Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.
(get-qe-disjunct <q>)
NB: Quantifier elimination is only complete for logics such as LRA, LIA, and BV.
Warning: this function is experimental and may change in future versions.
q: A quantified formula of the formQX_1 ... QX_n, P(x_1...x_i, y_1...y_j)whereQXis a set of quantified variables of the formQ x_1...x_kandP(x_1...x_i, y_1...y_j)is a quantifier-free formula.
Returns a formula Φ such that, given the current set of formulas A asserted to this solver:
A ∧ q → A ∧ ΦifQis∀, andA ∧ Φ → A ∧ qifQis∃;Φis a quantifier-free formula containing only free variables iny_1...y_n;if
Qis∃, letA ∧ Q_nbe the formulaA ∧ ¬ (Φ ∧ Q_1) ∧ ... ∧ ¬ (Φ ∧ Q_n)where for eachi ∈ [1, n], formulaΦ ∧ Q_iis the result of callinggetQuantifierEliminationDisjunctforqwith the set of assertionsA ∧ Q_{i-1}.Similarly, if
Qis∀, then letA ∧ Q_nbeA ∧ (Φ ∧ Q_1) ∧ ... ∧ (Φ ∧ Q_n)whereΦ ∧ Q_iis the same as above.In either case, we have that
Φ ∧ Q_jwill eventually be true or false, for some finitej.
When using separation logic, 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.
locSort: The location sort of the heap.dataSort: The data sort of the heap.
When using separation logic, obtain the term for the heap.
Warning: this function is experimental and may change in future versions.
When using separation logic, obtain the term for nil.
Warning: this function is experimental and may change in future versions.
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
Kind.INST_POOL
(declare-pool <symbol> <sort> ( <term>* ))
Warning: this function is experimental and may change in future versions.
symbol: The name of the pool.sort: The sort of the elements of the pool.initValueThe initial value of the pool.
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.
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.
TODO #
Causes the tests to crash in a very weird way, see cvc5Test/Unit/ApiSolverOracleFun.lean.
Get an interpolant if one exists, the null term otherwise.
Given that A → B is valid, this function determines a term I over the shared variables of A and B, such that A → I and I → B are valid. A is the current set of assertions and B is the conjecture, given as conj.
(get-interpolant <symbol> <conj>)
NB: in SMT-LIB, <symbol> assigns a symbol to the interpolant.
NB: Requires option produce-interpolants to be set to a mode different from none.
Warning: this function is experimental and may change in future versions.
conj: The conjecture term.
Get an interpolant if one exists, the null term otherwise.
Given that A → B is valid, this function determines a term I over the shared variables of A
and B, such that A → I and I → B are valid. I is constructed from the given grammar. A is
the current set of assertions and B is the conjecture, given as conj.
(get-interpolant <symbol> <conj> <grammar>)
NB: in SMT-LIB, <symbol> assigns a symbol to the interpolant.
NB: Requires option produce-interpolants to be set to a mode different from none.
Warning: this function is experimental and may change in future versions.
conj: The conjecture term.grammar: The grammar for the interpolantI.
Get an interpolant if one exists, the null term otherwise.
Given that A → B is valid, this function determines a term I over the shared variables of A
and B, such that A → I and I → B are valid. If a grammar G is provided, I is constructed
from G. A is the current set of assertions and B is the conjecture, given as conj.
(get-interpolant <symbol> <conj>)
(get-interpolant <symbol> <conj> <grammar>)
NB: in SMT-LIB, <symbol> assigns a symbol to the interpolant.
NB: Requires option produce-interpolants to be set to a mode different from none.
Warning: this function is experimental and may change in future versions.
conj: The conjecture term.grammar: The optional grammar for the interpolantI.
Equations
- solver.getInterpolant conj (some grammar_2) = solver.getInterpolantOfGrammar conj grammar_2
- solver.getInterpolant conj grammar = solver.getInterpolantSimple conj
Instances For
Get the next interpolant if any, the null term otherwise.
Can only be called immediately after a successful call to getInterpolant,
getInterpolantOfGrammar, getInterpolant?, getInterpolantNext, or getInterpolantNext. It is
guaranteed to produce a syntactically different interpolant w.r.t. the last returned interpolant
if successful.
(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 → I and I → B and 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.
Get an abduct if one exists, the null term otherwise.
(get-abduct <conj> <grammar>)
NB: Requires to enable option produce-abducts.
Warning: this function is experimental and may change in future versions.
conj: The conjecture term.grammar: The grammar for the abductC.
Returns a term C such that A ∧ C is satisfiable, and A ∧ ¬B ∧ 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.
Get an abduct if one exists.
(get-abduct <conj>)
(get-abduct <conj> <grammar>)
NB: Requires to enable option produce-abducts.
Warning: this function is experimental and may change in future versions.
conj: The conjecture term.grammar: The optional grammar for the abductC.
Returns a term C such that A ∧ C is satisfiable, and A ∧ ¬B ∧ 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.
Equations
- solver.getAbduct conj (some grammar_2) = solver.getAbductOfGrammar conj grammar_2
- solver.getAbduct conj grammar = cvc5.Solver.getAbductSimple✝ solver conj
Instances For
Get the next interpolant if any, the null term otherwise.
Can only be called immediately after a successful call to getAbduct, getAbductOfGrammar,
getAbduct?, getAbductNext, or getAbductNext?. It is guaranteed to produce a syntactically
different abduct w.r.t. the last returned abduct if successful.
(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 ∧ C is satisfiable, and A ∧ ¬B ∧ C is unsatisfiable, where A is
the current set of assertions and B is given in the input by the last call to a getAbduct-like
function, or the null term if such a term cannot be found.
Block the current model. Can be called only if immediately preceded by a SAT or INVALID query.
(block-model)
NB: requires enabling option produce-models.
Warning: this function is experimental and may change in future versions.
mode: The mode to use for blocking.
Block the current model values of (at least) the values in terms.
Can be called only if immediately preceded by a SAT query.
(block-model-values ( <term>+ ))
NB: requires enabling option produce-models.
Warning: this function is experimental and may change in future versions.
terms: The model values to block.
Produce a string containing information about all instantiations made by the quantifier module.
Warning: this function is experimental and may change in future versions.
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.
proof: A proof, usually obtained fromgetProof.format: The proof format used to print the proof. Must beProofFormat.NONEif the proof is from a component other thanProofComponent.FULL.
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.
t: The type of learned literals to return.
Create a Sygus grammar.
The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.
boundVarsThe parameters to corresponding synth-fun/synth-inv.ntSymbolsThe pre-declaration of the non-terminal symbols.
Synthesizes an n-ary function with optional syntactic constraints to verify.
(synth-fun <symbol> ( <boundVars>* ) <sort>)
(synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>)
symbolThe name of the function.boundVarsThe parameters to this function.sortThe sort of the return value of this function.grammarThe optional syntactic constraints.
Equations
- solver.synthFun symbol boundVars sort (some grammar_2) = cvc5.Solver.synthFunWithGrammar✝ solver symbol boundVars sort grammar_2
- solver.synthFun symbol boundVars sort grammar = cvc5.Solver.synthFunWithoutGrammar✝ solver symbol boundVars sort
Instances For
Append \p symbol to the current list of universal variables.
SyGuS v2:
(declare-var <symbol> <sort>)
sortThe sort of the universal variable.symbolThe name of the universal variable.
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>)
invThe function-to-synthesize.preThe pre-condition.transThe transition relation.postThe post-condition.
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.
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.
Get the synthesis solution of the given term.
This function should be called immediately after the solver answers unsat for sygus input.
termThe term for which the synthesis solution is queried.
Get the synthesis solutions of the given terms.
This function should be called immediately after the solver answers unsat for sygus input.
termsThe terms for which the synthesis solutions is queried.
Find a target term of interest using sygus enumeration with an optional grammar.
SyGuS v2:
(find-synth)
(find-synth :target G)
fstThe identifier specifying what kind of term to find.grammarThe optional grammar for the term. Ifnone, 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.
Returns the result of the find, which is the null term if the call failed.
Warning: this function is experimental and may change in future versions.
Equations
- solver.findSynth fst (some grammar_2) = cvc5.Solver.findSynthWithGrammar✝ solver fst grammar_2
- solver.findSynth fst grammar = cvc5.Solver.findSynthWithoutGrammar✝ solver fst
Instances For
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)
Returns the result of the find, which is the null term if this call failed.
Warning: this function is experimental and may change in future versions.