@[extern kind_toString]

opaque cvc5.Kind.toString : Kind → String

Produces a string representation.

instance cvc5.Kind.instToString : ToString Kind

Equations

• cvc5.Kind.instToString = { toString := cvc5.Kind.toString }

@[extern kind_hash]

opaque cvc5.Kind.hash : Kind → UInt64

Produces a hash.

instance cvc5.Kind.instHashable : Hashable Kind

Equations

• cvc5.Kind.instHashable = { hash := cvc5.Kind.hash }

@[extern sortKind_toString]

opaque cvc5.SortKind.toString : SortKind → String

Produces a string representation.

instance cvc5.SortKind.instToString : ToString SortKind

Equations

• cvc5.SortKind.instToString = { toString := cvc5.SortKind.toString }

@[extern sortKind_hash]

opaque cvc5.SortKind.hash : SortKind → UInt64

Produces a hash.

instance cvc5.SortKind.instHashable : Hashable SortKind

Equations

• cvc5.SortKind.instHashable = { hash := cvc5.SortKind.hash }

@[extern proofRule_toString]

opaque cvc5.ProofRule.toString : ProofRule → String

Produces a string representation.

instance cvc5.ProofRule.instToString : ToString ProofRule

Equations

• cvc5.ProofRule.instToString = { toString := cvc5.ProofRule.toString }

@[extern proofRule_hash]

opaque cvc5.ProofRule.hash : ProofRule → UInt64

Produces a hash.

instance cvc5.ProofRule.instHashable : Hashable ProofRule

Equations

• cvc5.ProofRule.instHashable = { hash := cvc5.ProofRule.hash }

@[extern skolemId_toString]

opaque cvc5.SkolemId.toString : SkolemId → String

Produces a string representation.

instance cvc5.SkolemId.instToString : ToString SkolemId

Equations

• cvc5.SkolemId.instToString = { toString := cvc5.SkolemId.toString }

@[extern skolemId_hash]

opaque cvc5.SkolemId.hash : SkolemId → UInt64

Produces a hash.

instance cvc5.SkolemId.instHashable : Hashable SkolemId

Equations

• cvc5.SkolemId.instHashable = { hash := cvc5.SkolemId.hash }

@[extern proofRewriteRule_toString]

opaque cvc5.ProofRewriteRule.toString : ProofRewriteRule → String

Produces a string representation.

instance cvc5.ProofRewriteRule.instToString : ToString ProofRewriteRule

Equations

• cvc5.ProofRewriteRule.instToString = { toString := cvc5.ProofRewriteRule.toString }

@[extern proofRewriteRule_hash]

opaque cvc5.ProofRewriteRule.hash : ProofRewriteRule → UInt64

Produces a hash.

instance cvc5.ProofRewriteRule.instHashable : Hashable ProofRewriteRule

Equations

• cvc5.ProofRewriteRule.instHashable = { hash := cvc5.ProofRewriteRule.hash }

@[extern unknownExplanation_toString]

opaque cvc5.UnknownExplanation.toString : UnknownExplanation → String

Produces a string representation.

instance cvc5.UnknownExplanation.instToString : ToString UnknownExplanation

Equations

• cvc5.UnknownExplanation.instToString = { toString := cvc5.UnknownExplanation.toString }

@[extern unknownExplanation_hash]

opaque cvc5.UnknownExplanation.hash : UnknownExplanation → UInt64

Produces a hash.

instance cvc5.UnknownExplanation.instHashable : Hashable UnknownExplanation

Equations

• cvc5.UnknownExplanation.instHashable = { hash := cvc5.UnknownExplanation.hash }

@[extern roundingMode_toString]

opaque cvc5.RoundingMode.toString : RoundingMode → String

Produces a string representation.

instance cvc5.RoundingMode.instToString : ToString RoundingMode

Equations

• cvc5.RoundingMode.instToString = { toString := cvc5.RoundingMode.toString }

@[extern roundingMode_hash]

opaque cvc5.RoundingMode.hash : RoundingMode → UInt64

Produces a hash.

instance cvc5.RoundingMode.instHashable : Hashable RoundingMode

Equations

• cvc5.RoundingMode.instHashable = { hash := cvc5.RoundingMode.hash }

@[extern blockModelsMode_toString]

opaque cvc5.BlockModelsMode.toString : BlockModelsMode → String

Produces a string representation.

instance cvc5.BlockModelsMode.instToString : ToString BlockModelsMode

Equations

• cvc5.BlockModelsMode.instToString = { toString := cvc5.BlockModelsMode.toString }

@[extern blockModelsMode_hash]

opaque cvc5.BlockModelsMode.hash : BlockModelsMode → UInt64

Produces a hash.

instance cvc5.BlockModelsMode.instHashable : Hashable BlockModelsMode

Equations

• cvc5.BlockModelsMode.instHashable = { hash := cvc5.BlockModelsMode.hash }

@[extern learnedLitType_toString]

opaque cvc5.LearnedLitType.toString : LearnedLitType → String

Produces a string representation.

instance cvc5.LearnedLitType.instToString : ToString LearnedLitType

Equations

• cvc5.LearnedLitType.instToString = { toString := cvc5.LearnedLitType.toString }

@[extern learnedLitType_hash]

opaque cvc5.LearnedLitType.hash : LearnedLitType → UInt64

Produces a hash.

instance cvc5.LearnedLitType.instHashable : Hashable LearnedLitType

Equations

• cvc5.LearnedLitType.instHashable = { hash := cvc5.LearnedLitType.hash }

@[extern proofComponent_toString]

opaque cvc5.ProofComponent.toString : ProofComponent → String

Produces a string representation.

instance cvc5.ProofComponent.instToString : ToString ProofComponent

Equations

• cvc5.ProofComponent.instToString = { toString := cvc5.ProofComponent.toString }

@[extern proofComponent_hash]

opaque cvc5.ProofComponent.hash : ProofComponent → UInt64

Produces a hash.

instance cvc5.ProofComponent.instHashable : Hashable ProofComponent

Equations

• cvc5.ProofComponent.instHashable = { hash := cvc5.ProofComponent.hash }

@[extern proofFormat_toString]

opaque cvc5.ProofFormat.toString : ProofFormat → String

Produces a string representation.

instance cvc5.ProofFormat.instToString : ToString ProofFormat

Equations

• cvc5.ProofFormat.instToString = { toString := cvc5.ProofFormat.toString }

@[extern proofFormat_hash]

opaque cvc5.ProofFormat.hash : ProofFormat → UInt64

Produces a hash.

instance cvc5.ProofFormat.instHashable : Hashable ProofFormat

Equations

• cvc5.ProofFormat.instHashable = { hash := cvc5.ProofFormat.hash }

@[extern findSynthTarget_toString]

opaque cvc5.FindSynthTarget.toString : FindSynthTarget → String

Produces a string representation.

instance cvc5.FindSynthTarget.instToString : ToString FindSynthTarget

Equations

• cvc5.FindSynthTarget.instToString = { toString := cvc5.FindSynthTarget.toString }

@[extern findSynthTarget_hash]

opaque cvc5.FindSynthTarget.hash : FindSynthTarget → UInt64

Produces a hash.

instance cvc5.FindSynthTarget.instHashable : Hashable FindSynthTarget

Equations

• cvc5.FindSynthTarget.instHashable = { hash := cvc5.FindSynthTarget.hash }

@[extern inputLanguage_toString]

opaque cvc5.InputLanguage.toString : InputLanguage → String

Produces a string representation.

instance cvc5.InputLanguage.instToString : ToString InputLanguage

Equations

• cvc5.InputLanguage.instToString = { toString := cvc5.InputLanguage.toString }

@[extern inputLanguage_hash]

opaque cvc5.InputLanguage.hash : InputLanguage → UInt64

Produces a hash.

instance cvc5.InputLanguage.instHashable : Hashable InputLanguage

Equations

• cvc5.InputLanguage.instHashable = { hash := cvc5.InputLanguage.hash }

def cvc5.Result : Type

Encapsulation of a three-valued solver result, with explanations.

Equations

• cvc5.Result = cvc5.ResultImpl✝.type

instance cvc5.Result.instNonemptyResult : Nonempty Result

def cvc5.Sort : Type

The sort of a cvc5 term.

Equations

• cvc5.Sort = cvc5.SortImpl✝.type

instance cvc5.Sort.instNonemptySort : Nonempty «Sort»

def cvc5.Op : Type

A cvc5 operator.

An operator is a term that represents certain operators, instantiated with its required parameters, e.g., a Term of kind Kind.BITVECTOR_EXTRACT.

Equations

• cvc5.Op = cvc5.OpImpl✝.type

instance cvc5.Op.instNonemptyOp : Nonempty Op

def cvc5.Term : Type

A cvc5 term.

Equations

• cvc5.Term = cvc5.TermImpl✝.type

instance cvc5.Term.instNonemptyTerm : Nonempty Term

def cvc5.Proof : Type

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

• cvc5.Proof = cvc5.ProofImpl✝.type

instance cvc5.Proof.instNonemptyProof : Nonempty Proof

def cvc5.TermManager : Type

Manager for cvc5 terms.

Equations

• cvc5.TermManager = cvc5.TermManagerImpl✝.type

instance cvc5.TermManager.instNonemptyTermManager : Nonempty TermManager

inductive cvc5.Error : Type

Error type.

• missingValue : Error
• error (msg : String) : Error
• recoverable (msg : String) : Error
• unsupported (msg : String) : Error
• option (msg : String) : Error

instance cvc5.instReprError : Repr Error

Equations

• cvc5.instReprError = { reprPrec := cvc5.reprError✝ }

def cvc5.Solver : Type

A cvc5 solver.

Equations

• cvc5.Solver = cvc5.SolverImpl✝.type

instance cvc5.Solver.instNonemptySolver : Nonempty Solver

@[reducible, inline]

abbrev cvc5.SolverT (m : Type → Type u_1) (α : Type) : Type u_1

Solver error/state-monad transformer.

Equations

• cvc5.SolverT m = ExceptT cvc5.Error (StateT cvc5.Solver m)

@[reducible, inline]

abbrev cvc5.SolverM (α : Type) : Type

Solver error/state-monad wrapped in IO.

Equations

• cvc5.SolverM = cvc5.SolverT IO

def cvc5.Error.toString : Error → String

String representation of an error.

Equations

• cvc5.Error.toString = toString ∘ repr

def cvc5.Error.unwrap! {α : Type u_1} [Inhabited α] : Except Error α → α

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!" 311 14 e.toString

instance cvc5.Error.instToString : ToString Error

Equations

• cvc5.Error.instToString = { toString := cvc5.Error.toString }

@[extern result_beq]

opaque cvc5.Result.beq : Result → Result → Bool

Comparison for structural equality.

instance cvc5.Result.instBEq : BEq Result

Equations

• cvc5.Result.instBEq = { beq := cvc5.Result.beq }

@[extern result_hash]

opaque cvc5.Result.hash : Result → UInt64

Hash function for cvc5 sorts.

instance cvc5.Result.instHashable : Hashable Result

Equations

• cvc5.Result.instHashable = { hash := cvc5.Result.hash }

@[extern result_isSat]

opaque cvc5.Result.isSat : Result → Bool

True if this result is from a satisfiable checkSat or checkSatAssuming query.

@[extern result_isUnsat]

opaque cvc5.Result.isUnsat : Result → Bool

True if this result is from a unsatisfiable checkSat or checkSatAssuming query.

@[extern result_isUnknown]

opaque cvc5.Result.isUnknown : Result → Bool

True if this result is from a checkSat or checkSatAssuming query and cvc5 was not able to determine (un)satisfiability.

@[extern result_getUnknownExplanation]

opaque cvc5.Result.getUnknownExplanation : Result → UnknownExplanation

An explanation for an unknown query result.

Note that if the result is (un)sat, this function returns UnknownExplanation.UNKNOWN_REASON.

def cvc5.Result.getUnknownExplanation? (res : Result) : Option UnknownExplanation

An explanation for an unknown query result, none if the result in not unknown.

Equations

• res.getUnknownExplanation? = if ¬res.isUnknown = true then none else some res.getUnknownExplanation

@[extern result_toString]

opaque cvc5.Result.toString : Result → String

A string representation of this result.

instance cvc5.Result.instToString : ToString Result

Equations

• cvc5.Result.instToString = { toString := cvc5.Result.toString }

@[extern sort_null]

opaque cvc5.Sort.null : Unit → «Sort»

The null sort.

instance cvc5.Sort.instInhabited : Inhabited «Sort»

Equations

• cvc5.Sort.instInhabited = { default := cvc5.Sort.null () }

@[extern sort_beq]

opaque cvc5.Sort.beq : «Sort» → «Sort» → Bool

Comparison for structural equality.

instance cvc5.Sort.instBEq : BEq «Sort»

Equations

• cvc5.Sort.instBEq = { beq := cvc5.Sort.beq }

@[extern sort_blt]

opaque cvc5.Sort.blt : «Sort» → «Sort» → Bool

Less than comparison.

@[extern sort_bgt]

opaque cvc5.Sort.bgt : «Sort» → «Sort» → Bool

Greater than comparison.

@[extern sort_ble]

opaque cvc5.Sort.ble : «Sort» → «Sort» → Bool

Less than or equal comparison.

@[extern sort_bge]

opaque cvc5.Sort.bge : «Sort» → «Sort» → Bool

Greater than or equal comparison.

def cvc5.Sort.compare (s1 s2 : «Sort») : Ordering

Comparison of two sorts.

Equations

• s1.compare s2 = if s1.beq s2 = true then Ordering.eq else if s1.bgt s2 = true then Ordering.gt else Ordering.lt

instance cvc5.Sort.instOrd : Ord «Sort»

Equations

• cvc5.Sort.instOrd = { compare := cvc5.Sort.compare }

instance cvc5.Sort.instLT : LT «Sort»

Equations

• cvc5.Sort.instLT = { lt := fun (x1 x2 : cvc5.Sort) => x1.blt x2 = true }

instance cvc5.Sort.instDecidableLT : DecidableLT «Sort»

Equations

• s1.instDecidableLT s2 = if h : s1.blt s2 = true then isTrue h else isFalse h

instance cvc5.Sort.instLE : LE «Sort»

Equations

• cvc5.Sort.instLE = { le := fun (x1 x2 : cvc5.Sort) => x1.ble x2 = true }

instance cvc5.Sort.instDecidableLE : DecidableLE «Sort»

Equations

• s1.instDecidableLE s2 = if h : s1.ble s2 = true then isTrue h else isFalse h

@[extern sort_hash]

opaque cvc5.Sort.hash : «Sort» → UInt64

Hash function for cvc5 sorts.

instance cvc5.Sort.instHashable : Hashable «Sort»

Equations

• cvc5.Sort.instHashable = { hash := cvc5.Sort.hash }

@[extern sort_getKind]

opaque cvc5.Sort.getKind : «Sort» → SortKind

Get the kind of this sort.

@[extern sort_isNull]

opaque cvc5.Sort.isNull : «Sort» → Bool

Determine if this is the null sort (cvc5.Sort).

@[extern sort_isBoolean]

opaque cvc5.Sort.isBoolean : «Sort» → Bool

Determine if this is the Boolean sort (SMT-LIB: Bool).

@[extern sort_isInteger]

opaque cvc5.Sort.isInteger : «Sort» → Bool

Determine if this is the Integer sort (SMT-LIB: Int).

@[extern sort_isReal]

opaque cvc5.Sort.isReal : «Sort» → Bool

Determine if this is the Real sort (SMT-LIB: Real).

@[extern sort_isString]

opaque cvc5.Sort.isString : «Sort» → Bool

Determine if this is the String sort (SMT-LIB: String).

@[extern sort_isRegExp]

opaque cvc5.Sort.isRegExp : «Sort» → Bool

Determine if this is the regular expression sort (SMT-LIB: RegLan).

@[extern sort_isRoundingMode]

opaque cvc5.Sort.isRoundingMode : «Sort» → Bool

Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).

@[extern sort_isBitVector]

opaque cvc5.Sort.isBitVector : «Sort» → Bool

Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).

@[extern sort_isFloatingPoint]

opaque cvc5.Sort.isFloatingPoint : «Sort» → Bool

Determine if this is a floating-point sort (SMT-LIB: (_ FloatingPoint eb sb)).

@[extern sort_isDatatype]

opaque cvc5.Sort.isDatatype : «Sort» → Bool

Determine if this is a datatype sort.

@[extern sort_isDatatypeConstructor]

opaque cvc5.Sort.isDatatypeConstructor : «Sort» → Bool

Determine if this is a datatype constructor sort.

@[extern sort_isDatatypeSelector]

opaque cvc5.Sort.isDatatypeSelector : «Sort» → Bool

Determine if this is a datatype selector sort.

@[extern sort_isDatatypeTester]

opaque cvc5.Sort.isDatatypeTester : «Sort» → Bool

Determine if this is a datatype tester sort.

@[extern sort_isDatatypeUpdater]

opaque cvc5.Sort.isDatatypeUpdater : «Sort» → Bool

Determine if this is a datatype updater sort.

@[extern sort_isFunction]

opaque cvc5.Sort.isFunction : «Sort» → Bool

Determine if this is a function sort.

@[extern sort_isPredicate]

opaque cvc5.Sort.isPredicate : «Sort» → Bool

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.

@[extern sort_isTuple]

opaque cvc5.Sort.isTuple : «Sort» → Bool

Determine if this is a tuple sort.

@[extern sort_isNullable]

opaque cvc5.Sort.isNullable : «Sort» → Bool

Determine if this is a nullable sort.

@[extern sort_isRecord]

opaque cvc5.Sort.isRecord : «Sort» → Bool

Determine if this is a record sort.

Warning: this function is experimental and may change in future versions.

@[extern sort_isArray]

opaque cvc5.Sort.isArray : «Sort» → Bool

Determine if this is an array sort.

@[extern sort_isFiniteField]

opaque cvc5.Sort.isFiniteField : «Sort» → Bool

Determine if this is a finite field sort.

@[extern sort_isSet]

opaque cvc5.Sort.isSet : «Sort» → Bool

Determine if this is a Set sort.

@[extern sort_isBag]

opaque cvc5.Sort.isBag : «Sort» → Bool

Determine if this is a Bag sort.

@[extern sort_isSequence]

opaque cvc5.Sort.isSequence : «Sort» → Bool

Determine if this is a Sequence sort.

@[extern sort_isAbstract]

opaque cvc5.Sort.isAbstract : «Sort» → Bool

Determine if this is an abstract sort.

@[extern sort_isUninterpretedSort]

opaque cvc5.Sort.isUninterpretedSort : «Sort» → Bool

Determine if this is an uninterpreted sort.

@[extern sort_isUninterpretedSortConstructor]

opaque cvc5.Sort.isUninterpretedSortConstructor : «Sort» → Bool

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.

@[extern sort_isInstantiated]

opaque cvc5.Sort.isInstantiated : «Sort» → Bool

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.

@[extern sort_toString]

opaque cvc5.Sort.toString : «Sort» → String

A string representation of this sort.

@[extern sort_hasSymbol]

opaque cvc5.Sort.hasSymbol : «Sort» → Except Error Bool

Determine if this term has a symbol (a name).

For example, free constants and variables have symbols.

def cvc5.Sort.hasSymbol? (v0 : «Sort») : Option Bool

Determine if this term has a symbol (a name).

For example, free constants and variables have symbols.

Equations

• v0.hasSymbol? = v0.hasSymbol.toOption

def cvc5.Sort.hasSymbol! (v0 : «Sort») : Bool

Determine if this term has a symbol (a name).

For example, free constants and variables have symbols.

Equations

• v0.hasSymbol! = cvc5.Error.unwrap! v0.hasSymbol

def cvc5.Sort.getSymbol! (v0 : «Sort») : String

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! = cvc5.Error.unwrap! v0.getSymbol

def cvc5.Sort.getSymbol? (v0 : «Sort») : Option String

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

@[extern sort_getSymbol]

opaque cvc5.Sort.getSymbol : «Sort» → Except Error String

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.

def cvc5.Sort.getFunctionArity? (v0 : «Sort») : Option Nat

The arity of a function sort.

Equations

• v0.getFunctionArity? = v0.getFunctionArity.toOption

@[extern sort_getFunctionArity]

opaque cvc5.Sort.getFunctionArity : «Sort» → Except Error Nat

The arity of a function sort.

def cvc5.Sort.getFunctionArity! (v0 : «Sort») : Nat

The arity of a function sort.

Equations

• v0.getFunctionArity! = cvc5.Error.unwrap! v0.getFunctionArity

@[extern sort_getFunctionDomainSorts]

opaque cvc5.Sort.getFunctionDomainSorts : «Sort» → Except Error (Array «Sort»)

The domain sorts of a function sort.

def cvc5.Sort.getFunctionDomainSorts! (v0 : «Sort») : Array «Sort»

The domain sorts of a function sort.

Equations

• v0.getFunctionDomainSorts! = cvc5.Error.unwrap! v0.getFunctionDomainSorts

def cvc5.Sort.getFunctionDomainSorts? (v0 : «Sort») : Option (Array «Sort»)

The domain sorts of a function sort.

Equations

• v0.getFunctionDomainSorts? = v0.getFunctionDomainSorts.toOption

def cvc5.Sort.getFunctionCodomainSort! (v0 : «Sort») : «Sort»

The codomain sort of a function sort.

Equations

• v0.getFunctionCodomainSort! = cvc5.Error.unwrap! v0.getFunctionCodomainSort

def cvc5.Sort.getFunctionCodomainSort? (v0 : «Sort») : Option «Sort»

The codomain sort of a function sort.

Equations

• v0.getFunctionCodomainSort? = v0.getFunctionCodomainSort.toOption

@[extern sort_getFunctionCodomainSort]

opaque cvc5.Sort.getFunctionCodomainSort : «Sort» → Except Error «Sort»

The codomain sort of a function sort.

@[extern sort_getArrayIndexSort]

opaque cvc5.Sort.getArrayIndexSort : «Sort» → Except Error «Sort»

The array index sort of an array index.

def cvc5.Sort.getArrayIndexSort? (v0 : «Sort») : Option «Sort»

The array index sort of an array index.

Equations

• v0.getArrayIndexSort? = v0.getArrayIndexSort.toOption

def cvc5.Sort.getArrayIndexSort! (v0 : «Sort») : «Sort»

The array index sort of an array index.

Equations

• v0.getArrayIndexSort! = cvc5.Error.unwrap! v0.getArrayIndexSort

@[extern sort_getArrayElementSort]

opaque cvc5.Sort.getArrayElementSort : «Sort» → Except Error «Sort»

The array element sort of an array index.

def cvc5.Sort.getArrayElementSort? (v0 : «Sort») : Option «Sort»

The array element sort of an array index.

Equations

• v0.getArrayElementSort? = v0.getArrayElementSort.toOption

def cvc5.Sort.getArrayElementSort! (v0 : «Sort») : «Sort»

The array element sort of an array index.

Equations

• v0.getArrayElementSort! = cvc5.Error.unwrap! v0.getArrayElementSort

@[extern sort_getSetElementSort]

opaque cvc5.Sort.getSetElementSort : «Sort» → Except Error «Sort»

The element sort of a set sort.

def cvc5.Sort.getSetElementSort? (v0 : «Sort») : Option «Sort»

The element sort of a set sort.

Equations

• v0.getSetElementSort? = v0.getSetElementSort.toOption

def cvc5.Sort.getSetElementSort! (v0 : «Sort») : «Sort»

The element sort of a set sort.

Equations

• v0.getSetElementSort! = cvc5.Error.unwrap! v0.getSetElementSort

@[extern sort_getBagElementSort]

opaque cvc5.Sort.getBagElementSort : «Sort» → Except Error «Sort»

The element sort of a bag sort.

def cvc5.Sort.getBagElementSort? (v0 : «Sort») : Option «Sort»

The element sort of a bag sort.

Equations

• v0.getBagElementSort? = v0.getBagElementSort.toOption

def cvc5.Sort.getBagElementSort! (v0 : «Sort») : «Sort»

The element sort of a bag sort.

Equations

• v0.getBagElementSort! = cvc5.Error.unwrap! v0.getBagElementSort

def cvc5.Sort.getSequenceElementSort! (v0 : «Sort») : «Sort»

The element sort of a sequence sort.

Equations

• v0.getSequenceElementSort! = cvc5.Error.unwrap! v0.getSequenceElementSort

@[extern sort_getSequenceElementSort]

opaque cvc5.Sort.getSequenceElementSort : «Sort» → Except Error «Sort»

The element sort of a sequence sort.

def cvc5.Sort.getSequenceElementSort? (v0 : «Sort») : Option «Sort»

The element sort of a sequence sort.

Equations

• v0.getSequenceElementSort? = v0.getSequenceElementSort.toOption

@[extern sort_getAbstractedKind]

opaque cvc5.Sort.getAbstractedKind : «Sort» → Except Error SortKind

The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.

def cvc5.Sort.getAbstractedKind? (v0 : «Sort») : Option SortKind

The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.

Equations

• v0.getAbstractedKind? = v0.getAbstractedKind.toOption

def cvc5.Sort.getAbstractedKind! (v0 : «Sort») : SortKind

The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.

Equations

• v0.getAbstractedKind! = cvc5.Error.unwrap! v0.getAbstractedKind

def cvc5.Sort.getUninterpretedSortConstructorArity? (v0 : «Sort») : Option UInt32

The arity of an uninterpreted sort constructor sort.

Equations

• v0.getUninterpretedSortConstructorArity? = v0.getUninterpretedSortConstructorArity.toOption

@[extern sort_getUninterpretedSortConstructorArity]

opaque cvc5.Sort.getUninterpretedSortConstructorArity : «Sort» → Except Error UInt32

The arity of an uninterpreted sort constructor sort.

def cvc5.Sort.getUninterpretedSortConstructorArity! (v0 : «Sort») : UInt32

The arity of an uninterpreted sort constructor sort.

Equations

• v0.getUninterpretedSortConstructorArity! = cvc5.Error.unwrap! v0.getUninterpretedSortConstructorArity

@[extern sort_getBitVectorSize]

opaque cvc5.Sort.getBitVectorSize : «Sort» → Except Error UInt32

The bit-width of the bit-vector sort.

def cvc5.Sort.getBitVectorSize! (v0 : «Sort») : UInt32

The bit-width of the bit-vector sort.

Equations

• v0.getBitVectorSize! = cvc5.Error.unwrap! v0.getBitVectorSize

def cvc5.Sort.getBitVectorSize? (v0 : «Sort») : Option UInt32

The bit-width of the bit-vector sort.

Equations

• v0.getBitVectorSize? = v0.getBitVectorSize.toOption

def cvc5.Sort.getFiniteFieldSize? (v0 : «Sort») : Option Nat

The size of the finite field sort.

Equations

• v0.getFiniteFieldSize? = v0.getFiniteFieldSize.toOption

def cvc5.Sort.getFiniteFieldSize! (v0 : «Sort») : Nat

The size of the finite field sort.

Equations

• v0.getFiniteFieldSize! = cvc5.Error.unwrap! v0.getFiniteFieldSize

@[extern sort_getFiniteFieldSize]

opaque cvc5.Sort.getFiniteFieldSize : «Sort» → Except Error Nat

The size of the finite field sort.

def cvc5.Sort.getFloatingPointExponentSize? (v0 : «Sort») : Option UInt32

The bit-width of the exponent of the floating-point sort.

Equations

• v0.getFloatingPointExponentSize? = v0.getFloatingPointExponentSize.toOption

@[extern sort_getFloatingPointExponentSize]

opaque cvc5.Sort.getFloatingPointExponentSize : «Sort» → Except Error UInt32

The bit-width of the exponent of the floating-point sort.

def cvc5.Sort.getFloatingPointExponentSize! (v0 : «Sort») : UInt32

The bit-width of the exponent of the floating-point sort.

Equations

• v0.getFloatingPointExponentSize! = cvc5.Error.unwrap! v0.getFloatingPointExponentSize

@[extern sort_getFloatingPointSignificandSize]

opaque cvc5.Sort.getFloatingPointSignificandSize : «Sort» → Except Error UInt32

The width of the significand of the floating-point sort.

def cvc5.Sort.getFloatingPointSignificandSize? (v0 : «Sort») : Option UInt32

The width of the significand of the floating-point sort.

Equations

• v0.getFloatingPointSignificandSize? = v0.getFloatingPointSignificandSize.toOption

def cvc5.Sort.getFloatingPointSignificandSize! (v0 : «Sort») : UInt32

The width of the significand of the floating-point sort.

Equations

• v0.getFloatingPointSignificandSize! = cvc5.Error.unwrap! v0.getFloatingPointSignificandSize

def cvc5.Sort.getTupleLength! (v0 : «Sort») : UInt32

The length of a tuple sort.

Equations

• v0.getTupleLength! = cvc5.Error.unwrap! v0.getTupleLength

@[extern sort_getTupleLength]

opaque cvc5.Sort.getTupleLength : «Sort» → Except Error UInt32

The length of a tuple sort.

def cvc5.Sort.getTupleLength? (v0 : «Sort») : Option UInt32

The length of a tuple sort.

Equations

• v0.getTupleLength? = v0.getTupleLength.toOption

@[extern sort_getTupleSorts]

opaque cvc5.Sort.getTupleSorts : «Sort» → Except Error (Array «Sort»)

The element sorts of a tuple sort.

def cvc5.Sort.getTupleSorts! (v0 : «Sort») : Array «Sort»

The element sorts of a tuple sort.

Equations

• v0.getTupleSorts! = cvc5.Error.unwrap! v0.getTupleSorts

def cvc5.Sort.getTupleSorts? (v0 : «Sort») : Option (Array «Sort»)

The element sorts of a tuple sort.

Equations

• v0.getTupleSorts? = v0.getTupleSorts.toOption

@[extern sort_getNullableElementSort]

opaque cvc5.Sort.getNullableElementSort : «Sort» → Except Error «Sort»

The element sort of a nullable sort.

def cvc5.Sort.getNullableElementSort! (v0 : «Sort») : «Sort»

The element sort of a nullable sort.

Equations

• v0.getNullableElementSort! = cvc5.Error.unwrap! v0.getNullableElementSort

def cvc5.Sort.getNullableElementSort? (v0 : «Sort») : Option «Sort»

The element sort of a nullable sort.

Equations

• v0.getNullableElementSort? = v0.getNullableElementSort.toOption

@[extern sort_getUninterpretedSortConstructor]

opaque cvc5.Sort.getUninterpretedSortConstructor : «Sort» → Except Error «Sort»

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

def cvc5.Sort.getUninterpretedSortConstructor! (v0 : «Sort») : «Sort»

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

Equations

• v0.getUninterpretedSortConstructor! = cvc5.Error.unwrap! v0.getUninterpretedSortConstructor

def cvc5.Sort.getUninterpretedSortConstructor? (v0 : «Sort») : Option «Sort»

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

Equations

• v0.getUninterpretedSortConstructor? = v0.getUninterpretedSortConstructor.toOption

def cvc5.Sort.instantiate? (v0 : «Sort») (v1 : Array «Sort») : Option «Sort»

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

Create sort parameters with TermManager.mkParamSort symbol.

• params The list of sort parameters to instantiate with.

Equations

• v0.instantiate? v1 = (v0.instantiate v1).toOption

def cvc5.Sort.instantiate! (v0 : «Sort») (v1 : Array «Sort») : «Sort»

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

Create sort parameters with TermManager.mkParamSort symbol.

• params The list of sort parameters to instantiate with.

Equations

• v0.instantiate! v1 = cvc5.Error.unwrap! (v0.instantiate v1)

@[extern sort_instantiate]

opaque cvc5.Sort.instantiate : «Sort» → (params : Array «Sort») → Except Error «Sort»

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

Create sort parameters with TermManager.mkParamSort symbol.

• params The list of sort parameters to instantiate with.

def cvc5.Sort.substitute! (v0 : «Sort») (v1 v2 : Array «Sort») : «Sort»

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.

• sorts The sub-sorts to be substituted within this sort.
• replacements The sort replacing the substituted sub-sorts.

Equations

• v0.substitute! v1 v2 = cvc5.Error.unwrap! (v0.substitute v1 v2)

def cvc5.Sort.substitute? (v0 : «Sort») (v1 v2 : Array «Sort») : Option «Sort»

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.

• sorts The sub-sorts to be substituted within this sort.
• replacements The sort replacing the substituted sub-sorts.

Equations

• v0.substitute? v1 v2 = (v0.substitute v1 v2).toOption

@[extern sort_substitute]

opaque cvc5.Sort.substitute : «Sort» → (sorts replacements : Array «Sort») → Except Error «Sort»

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.

• sorts The sub-sorts to be substituted within this sort.
• replacements The sort replacing the substituted sub-sorts.

instance cvc5.Sort.instToString : ToString «Sort»

Equations

• cvc5.Sort.instToString = { toString := cvc5.Sort.toString }

instance cvc5.Sort.instRepr : Repr «Sort»

Equations

• cvc5.Sort.instRepr = { reprPrec := fun (self : cvc5.Sort) (x : Nat) => Std.Format.text self.toString }

@[extern op_null]

opaque cvc5.Op.null : Unit → Op

The null operator.

instance cvc5.Op.instInhabited : Inhabited Op

Equations

• cvc5.Op.instInhabited = { default := cvc5.Op.null () }

@[extern op_beq]

opaque cvc5.Op.beq : Op → Op → Bool

Syntactic equality operator.

instance cvc5.Op.instBEq : BEq Op

Equations

• cvc5.Op.instBEq = { beq := cvc5.Op.beq }

@[extern op_getKind]

opaque cvc5.Op.getKind : Op → Kind

Get the kind of this operator.

@[extern op_isNull]

opaque cvc5.Op.isNull : Op → Bool

Determine if this operator is nullary.

@[extern op_isIndexed]

opaque cvc5.Op.isIndexed : Op → Bool

Determine if this operator is indexed.

@[extern op_getNumIndices]

opaque cvc5.Op.getNumIndices : Op → Nat

Get the number of indices of this operator.

@[extern op_get]

opaque cvc5.Op.get (op : Op) : Fin op.getNumIndices → Term

Get the index at position i of an indexed operator.

@[extern op_toString]

opaque cvc5.Op.toString : Op → String

Get the string representation of this operator.

instance cvc5.Op.instGetElemNatTermLtGetNumIndices : GetElem Op Nat Term fun (op : Op) (i : Nat) => i < op.getNumIndices

Equations

• cvc5.Op.instGetElemNatTermLtGetNumIndices = { getElem := fun (op : cvc5.Op) (i : Nat) (h : i < op.getNumIndices) => op.get ⟨i, h⟩ }

instance cvc5.Op.instToString : ToString Op

Equations

• cvc5.Op.instToString = { toString := cvc5.Op.toString }

@[extern term_null]

opaque cvc5.Term.null : Unit → Term

The null term.

instance cvc5.Term.instInhabited : Inhabited Term

Equations

• cvc5.Term.instInhabited = { default := cvc5.Term.null () }

@[extern term_beq]

opaque cvc5.Term.beq : Term → Term → Bool

Syntactic equality operator.

instance cvc5.Term.instBEq : BEq Term

Equations

• cvc5.Term.instBEq = { beq := cvc5.Term.beq }

@[extern term_hash]

opaque cvc5.Term.hash : Term → UInt64

instance cvc5.Term.instHashable : Hashable Term

Equations

• cvc5.Term.instHashable = { hash := cvc5.Term.hash }

@[extern term_isNull]

opaque cvc5.Term.isNull : Term → Bool

Determine if this term is nullary.

@[extern term_getKind]

opaque cvc5.Term.getKind : Term → Kind

Get the kind of this term.

@[extern term_getSort]

opaque cvc5.Term.getSort : Term → «Sort»

Get the sort of this term.

@[extern term_hasOp]

opaque cvc5.Term.hasOp : Term → Bool

Determine if this term has an operator.

@[extern term_hasSymbol]

opaque cvc5.Term.hasSymbol : Term → Bool

Determine if this term has a symbol (a name).

For example, free constants and variables have symbols.

@[extern term_getId]

opaque cvc5.Term.getId : Term → Nat

Get the id of this term.

@[extern term_getNumChildren]

opaque cvc5.Term.getNumChildren : Term → Nat

Get the number of children of this term.

@[extern term_isSkolem]

opaque cvc5.Term.isSkolem : Term → Bool

Is this term a skolem?

@[extern term_get]

opaque cvc5.Term.get (t : Term) : Fin t.getNumChildren → Term

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

def cvc5.Term.getOp? (v0 : Term) : Option Op

Get the operator of a term with an operator.

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

Equations

• v0.getOp? = v0.getOp.toOption

@[extern term_getOp]

opaque cvc5.Term.getOp : Term → Except Error Op

Get the operator of a term with an operator.

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

def cvc5.Term.getOp! (v0 : Term) : Op

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

@[extern term_getBooleanValue]

opaque cvc5.Term.getBooleanValue : Term → Except Error Bool

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

Requires term to have sort Bool.

def cvc5.Term.getBooleanValue! (v0 : Term) : Bool

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

Requires term to have sort Bool.

Equations

• v0.getBooleanValue! = cvc5.Error.unwrap! v0.getBooleanValue

def cvc5.Term.getBooleanValue? (v0 : Term) : Option Bool

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

Requires term to have sort Bool.

Equations

• v0.getBooleanValue? = v0.getBooleanValue.toOption

@[extern term_getBitVectorValue]

opaque cvc5.Term.getBitVectorValue : Term → UInt32 → Except Error String

Get the string representation of a bit-vector value.

Requires term to have a bit-vector sort.

• base: 2 for binary, 10 for decimal, and 16 for hexadecimal.

def cvc5.Term.getBitVectorValue? (v0 : Term) (v1 : UInt32) : Option String

Get the string representation of a bit-vector value.

Requires term to have a bit-vector sort.

• base: 2 for binary, 10 for decimal, and 16 for hexadecimal.

Equations

• v0.getBitVectorValue? v1 = (v0.getBitVectorValue v1).toOption

def cvc5.Term.getBitVectorValue! (v0 : Term) (v1 : UInt32) : String

Get the string representation of a bit-vector value.

Requires term to have a bit-vector sort.

• base: 2 for binary, 10 for decimal, and 16 for hexadecimal.

Equations

• v0.getBitVectorValue! v1 = cvc5.Error.unwrap! (v0.getBitVectorValue v1)

def cvc5.Term.getIntegerValue! (v0 : Term) : Int

Get the native integral value of an integral value.

Equations

• v0.getIntegerValue! = cvc5.Error.unwrap! v0.getIntegerValue

@[extern term_getIntegerValue]

opaque cvc5.Term.getIntegerValue : Term → Except Error Int

Get the native integral value of an integral value.

def cvc5.Term.getIntegerValue? (v0 : Term) : Option Int

Get the native integral value of an integral value.

Equations

• v0.getIntegerValue? = v0.getIntegerValue.toOption

def cvc5.Term.getRationalValue! (v0 : Term) : Std.Internal.Rat

Get the native rational value of a real, rational-compatible value.

Equations

• v0.getRationalValue! = cvc5.Error.unwrap! v0.getRationalValue

@[extern term_getRationalValue]

opaque cvc5.Term.getRationalValue : Term → Except Error Std.Internal.Rat

Get the native rational value of a real, rational-compatible value.

def cvc5.Term.getRationalValue? (v0 : Term) : Option Std.Internal.Rat

Get the native rational value of a real, rational-compatible value.

Equations

• v0.getRationalValue? = v0.getRationalValue.toOption

def cvc5.Term.getSymbol! (v0 : Term) : String

Get the symbol of this term.

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

The symbol of the term is the string that was provided when constructing it via TermManager.mkConst or TermManager.mkVar.

Equations

• v0.getSymbol! = cvc5.Error.unwrap! v0.getSymbol

def cvc5.Term.getSymbol? (v0 : Term) : Option String

Get the symbol of this term.

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

The symbol of the term is the string that was provided when constructing it via TermManager.mkConst or TermManager.mkVar.

Equations

• v0.getSymbol? = v0.getSymbol.toOption

@[extern term_getSymbol]

opaque cvc5.Term.getSymbol : Term → Except Error String

Get the symbol of this term.

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

The symbol of the term is the string that was provided when constructing it via TermManager.mkConst or TermManager.mkVar.

def cvc5.Term.getSkolemId? (v0 : Term) : Option SkolemId

Get skolem identifier of this term.

Requires isSkolem.

Equations

• v0.getSkolemId? = v0.getSkolemId.toOption

@[extern term_getSkolemId]

opaque cvc5.Term.getSkolemId : Term → Except Error SkolemId

Get skolem identifier of this term.

Requires isSkolem.

def cvc5.Term.getSkolemId! (v0 : Term) : SkolemId

Get skolem identifier of this term.

Requires isSkolem.

Equations

• v0.getSkolemId! = cvc5.Error.unwrap! v0.getSkolemId

def cvc5.Term.getSkolemIndices? (v0 : Term) : Option (Array Term)

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

• v0.getSkolemIndices? = v0.getSkolemIndices.toOption

@[extern term_getSkolemIndices]

opaque cvc5.Term.getSkolemIndices : Term → Except Error (Array Term)

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.

def cvc5.Term.getSkolemIndices! (v0 : Term) : Array Term

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

• v0.getSkolemIndices! = cvc5.Error.unwrap! v0.getSkolemIndices

instance cvc5.Term.instGetElemNatLtGetNumChildren : GetElem Term Nat Term fun (t : Term) (i : Nat) => i < t.getNumChildren

Equations

• cvc5.Term.instGetElemNatLtGetNumChildren = { getElem := fun (t : cvc5.Term) (i : Nat) (h : i < t.getNumChildren) => t.get ⟨i, h⟩ }

def cvc5.Term.forIn {m : Type u → Type u_1} {β : Type u} [Monad m] (t : Term) (b : β) (f : Term → β → m (ForInStep β)) : m β

Equations

• t.forIn b f = cvc5.Term.forIn.loop t f t.getNumChildren ⋯ b

def cvc5.Term.forIn.loop {m : Type u → Type u_1} {β : Type u} [Monad m] (t : Term) (f : Term → β → m (ForInStep β)) (i : Nat) (h : i ≤ t.getNumChildren) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.
• cvc5.Term.forIn.loop t f 0 x b = pure b

instance cvc5.Term.instForIn {m : Type u_1 → Type u_2} : ForIn m Term Term

Equations

• cvc5.Term.instForIn = { forIn := fun {β : Type ?u.10} [Monad m] => cvc5.Term.forIn }

def cvc5.Term.getChildren (t : Term) : Array Term

Get the children of a term.

Equations

• One or more equations did not get rendered due to their size.

def cvc5.Term.not? (v0 : Term) : Option Term

Boolean negation.

Equations

• v0.not? = v0.not.toOption

@[extern term_not]

opaque cvc5.Term.not (t : Term) : Except Error Term

Boolean negation.

def cvc5.Term.not! (v0 : Term) : Term

Boolean negation.

Equations

• v0.not! = cvc5.Error.unwrap! v0.not

@[extern term_and]

opaque cvc5.Term.and (lft rgt : Term) : Except Error Term

Boolean and.

def cvc5.Term.and! (v0 v1 : Term) : Term

Boolean and.

Equations

• v0.and! v1 = cvc5.Error.unwrap! (v0.and v1)

def cvc5.Term.and? (v0 v1 : Term) : Option Term

Boolean and.

Equations

• v0.and? v1 = (v0.and v1).toOption

def cvc5.Term.or! (v0 v1 : Term) : Term

Boolean or.

Equations

• v0.or! v1 = cvc5.Error.unwrap! (v0.or v1)

def cvc5.Term.or? (v0 v1 : Term) : Option Term

Boolean or.

Equations

• v0.or? v1 = (v0.or v1).toOption

@[extern term_or]

opaque cvc5.Term.or (lft rgt : Term) : Except Error Term

Boolean or.

@[extern term_xor]

opaque cvc5.Term.xor (lft rgt : Term) : Except Error Term

Boolean exclusive or.

def cvc5.Term.xor! (v0 v1 : Term) : Term

Boolean exclusive or.

Equations

• v0.xor! v1 = cvc5.Error.unwrap! (v0.xor v1)

def cvc5.Term.xor? (v0 v1 : Term) : Option Term

Boolean exclusive or.

Equations

• v0.xor? v1 = (v0.xor v1).toOption

def cvc5.Term.eq? (v0 v1 : Term) : Option Term

Equality.

Equations

• v0.eq? v1 = (v0.eq v1).toOption

@[extern term_eq]

opaque cvc5.Term.eq (lft rgt : Term) : Except Error Term

Equality.

def cvc5.Term.eq! (v0 v1 : Term) : Term

Equality.

Equations

• v0.eq! v1 = cvc5.Error.unwrap! (v0.eq v1)

def cvc5.Term.imp? (v0 v1 : Term) : Option Term

Boolean implication.

Equations

• v0.imp? v1 = (v0.imp v1).toOption

def cvc5.Term.imp! (v0 v1 : Term) : Term

Boolean implication.

Equations

• v0.imp! v1 = cvc5.Error.unwrap! (v0.imp v1)

@[extern term_imp]

opaque cvc5.Term.imp (lft rgt : Term) : Except Error Term

Boolean implication.

@[extern term_ite]

opaque cvc5.Term.ite (cnd thn els : Term) : Except Error Term

If-then-else.

• cnd: condition, must be a Boolean term;
• thn: then-branch of some sort S;
• els: else-branch of the same sort S.

def cvc5.Term.ite! (v0 v1 v2 : Term) : Term

If-then-else.

• cnd: condition, must be a Boolean term;
• thn: then-branch of some sort S;
• els: else-branch of the same sort S.

Equations

• v0.ite! v1 v2 = cvc5.Error.unwrap! (v0.ite v1 v2)

def cvc5.Term.ite? (v0 v1 v2 : Term) : Option Term

If-then-else.

• cnd: condition, must be a Boolean term;
• thn: then-branch of some sort S;
• els: else-branch of the same sort S.

Equations

• v0.ite? v1 v2 = (v0.ite v1 v2).toOption

@[extern term_toString]

opaque cvc5.Term.toString : Term → String

A string representation of this term.

instance cvc5.Term.instToString : ToString Term

Equations

• cvc5.Term.instToString = { toString := cvc5.Term.toString }

@[extern proof_null]

opaque cvc5.Proof.null : Unit → Proof

The null proof.

instance cvc5.Proof.instInhabited : Inhabited Proof

Equations

• cvc5.Proof.instInhabited = { default := cvc5.Proof.null () }

@[extern proof_getRule]

opaque cvc5.Proof.getRule : Proof → ProofRule

Get the proof rule used by the root step of the root.

def cvc5.Proof.getRewriteRule? (v0 : Proof) : Option ProofRewriteRule

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

• v0.getRewriteRule? = v0.getRewriteRule.toOption

@[extern proof_getRewriteRule]

opaque cvc5.Proof.getRewriteRule : Proof → Except Error ProofRewriteRule

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.

def cvc5.Proof.getRewriteRule! (v0 : Proof) : ProofRewriteRule

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

• v0.getRewriteRule! = cvc5.Error.unwrap! v0.getRewriteRule

@[extern proof_getResult]

opaque cvc5.Proof.getResult : Proof → Term

The conclusion of the root step of the proof.

@[extern proof_getChildren]

opaque cvc5.Proof.getChildren : Proof → Array Proof

The premises of the root step of the proof.

@[extern proof_getArguments]

opaque cvc5.Proof.getArguments : Proof → Array Term

The arguments of the root step of the proof as a vector of terms.

Some of those terms might be strings.

@[extern proof_beq]

opaque cvc5.Proof.beq : Proof → Proof → Bool

Operator overloading for referential equality of two proofs.

instance cvc5.Proof.instBEq : BEq Proof

Equations

• cvc5.Proof.instBEq = { beq := cvc5.Proof.beq }

@[extern proof_hash]

opaque cvc5.Proof.hash : Proof → UInt64

Hash function for proofs.

instance cvc5.Proof.instHashable : Hashable Proof

Equations

• cvc5.Proof.instHashable = { hash := cvc5.Proof.hash }

@[extern termManager_new]

opaque cvc5.TermManager.new : BaseIO TermManager

Constructor.

@[extern termManager_getBooleanSort]

opaque cvc5.TermManager.getBooleanSort : TermManager → «Sort»

Get the Boolean sort.

@[extern termManager_getIntegerSort]

opaque cvc5.TermManager.getIntegerSort : TermManager → «Sort»

Get the Integer sort.

@[extern termManager_getRealSort]

opaque cvc5.TermManager.getRealSort : TermManager → «Sort»

Get the Real sort.

@[extern termManager_getRegExpSort]

opaque cvc5.TermManager.getRegExpSort : TermManager → «Sort»

Get the regular expression sort.

@[extern termManager_getRoundingModeSort]

opaque cvc5.TermManager.getRoundingModeSort : TermManager → «Sort»

Get the rounding mode sort.

@[extern termManager_getStringSort]

opaque cvc5.TermManager.getStringSort : TermManager → «Sort»

Get the string sort.

def cvc5.TermManager.mkArraySort! (v0 : TermManager) (v1 v2 : «Sort») : «Sort»

Create an array sort.

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

Equations

• v0.mkArraySort! v1 v2 = cvc5.Error.unwrap! (v0.mkArraySort v1 v2)

def cvc5.TermManager.mkArraySort? (v0 : TermManager) (v1 v2 : «Sort») : Option «Sort»

Create an array sort.

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

Equations

• v0.mkArraySort? v1 v2 = (v0.mkArraySort v1 v2).toOption

@[extern termManager_mkArraySort]

opaque cvc5.TermManager.mkArraySort : TermManager → (indexSort elemSort : «Sort») → Except Error «Sort»

Create an array sort.

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

def cvc5.TermManager.mkBitVectorSort! (v0 : TermManager) (v1 : UInt32) : «Sort»

Create a bit-vector sort.

• size The bit-width of the bit-vector sort.

Equations

• v0.mkBitVectorSort! v1 = cvc5.Error.unwrap! (v0.mkBitVectorSort v1)

def cvc5.TermManager.mkBitVectorSort? (v0 : TermManager) (v1 : UInt32) : Option «Sort»

Create a bit-vector sort.

• size The bit-width of the bit-vector sort.

Equations

• v0.mkBitVectorSort? v1 = (v0.mkBitVectorSort v1).toOption

@[extern termManager_mkBitVectorSort]

opaque cvc5.TermManager.mkBitVectorSort : TermManager → (size : UInt32) → Except Error «Sort»

Create a bit-vector sort.

• size The bit-width of the bit-vector sort.

def cvc5.TermManager.mkFloatingPointSort? (v0 : TermManager) (v1 v2 : UInt32) : Option «Sort»

Create a floating-point sort.

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

Equations

• v0.mkFloatingPointSort? v1 v2 = (v0.mkFloatingPointSort v1 v2).toOption

@[extern termManager_mkFloatingPointSort]

opaque cvc5.TermManager.mkFloatingPointSort : TermManager → (exp sig : UInt32) → Except Error «Sort»

Create a floating-point sort.

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

def cvc5.TermManager.mkFloatingPointSort! (v0 : TermManager) (v1 v2 : UInt32) : «Sort»

Create a floating-point sort.

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

Equations

• v0.mkFloatingPointSort! v1 v2 = cvc5.Error.unwrap! (v0.mkFloatingPointSort v1 v2)

@[reducible, inline]

abbrev cvc5.TermManager.mkFiniteFieldSort (tm : TermManager) (size : Nat) : Except Error «Sort»

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

• size The modulus of the field. Must be a prime.

Equations

• tm.mkFiniteFieldSort = (fun (x : String) => cvc5.TermManager.mkFiniteFieldSortFromString✝ tm x) ∘ toString

@[reducible, inline]

abbrev cvc5.TermManager.mkFiniteFieldSort! (tm : TermManager) (size : Nat) : «Sort»

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

• size The modulus of the field. Must be a prime.

Equations

• tm.mkFiniteFieldSort! = cvc5.Error.unwrap! ∘ (fun (x : String) => cvc5.TermManager.mkFiniteFieldSortFromString✝ tm x) ∘ toString

@[reducible, inline]

abbrev cvc5.TermManager.mkFiniteFieldSort? (tm : TermManager) (size : Nat) : Option «Sort»

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

• size The modulus of the field. Must be a prime.

Equations

• tm.mkFiniteFieldSort? = Except.toOption ∘ (fun (x : String) => cvc5.TermManager.mkFiniteFieldSortFromString✝ tm x) ∘ toString

def cvc5.TermManager.mkFunctionSort? (v0 : TermManager) (v1 : Array «Sort») (v2 : «Sort») : Option «Sort»

Create function sort.

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

Equations

• v0.mkFunctionSort? v1 v2 = (v0.mkFunctionSort v1 v2).toOption

@[extern termManager_mkFunctionSort]

opaque cvc5.TermManager.mkFunctionSort : TermManager → (sorts : Array «Sort») → (codomain : «Sort») → Except Error «Sort»

Create function sort.

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

def cvc5.TermManager.mkFunctionSort! (v0 : TermManager) (v1 : Array «Sort») (v2 : «Sort») : «Sort»

Create function sort.

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

Equations

• v0.mkFunctionSort! v1 v2 = cvc5.Error.unwrap! (v0.mkFunctionSort v1 v2)

def cvc5.TermManager.mkPredicateSort! (v0 : TermManager) (v1 : Array «Sort») : «Sort»

Create a predicate sort.

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

• sorts The list of sorts of the predicate.

Equations

• v0.mkPredicateSort! v1 = cvc5.Error.unwrap! (v0.mkPredicateSort v1)

def cvc5.TermManager.mkPredicateSort? (v0 : TermManager) (v1 : Array «Sort») : Option «Sort»

Create a predicate sort.

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

• sorts The list of sorts of the predicate.

Equations

• v0.mkPredicateSort? v1 = (v0.mkPredicateSort v1).toOption

@[extern termManager_mkPredicateSort]

opaque cvc5.TermManager.mkPredicateSort : TermManager → (sorts : Array «Sort») → Except Error «Sort»

Create a predicate sort.

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

• sorts The list of sorts of the predicate.

def cvc5.TermManager.mkTupleSort! (v0 : TermManager) (v1 : Array «Sort») : «Sort»

Create a tuple sort.

• sorts The sorts of the elements of the tuple.

Equations

• v0.mkTupleSort! v1 = cvc5.Error.unwrap! (v0.mkTupleSort v1)

def cvc5.TermManager.mkTupleSort? (v0 : TermManager) (v1 : Array «Sort») : Option «Sort»

Create a tuple sort.

• sorts The sorts of the elements of the tuple.

Equations

• v0.mkTupleSort? v1 = (v0.mkTupleSort v1).toOption

@[extern termManager_mkTupleSort]

opaque cvc5.TermManager.mkTupleSort : TermManager → (sorts : Array «Sort») → Except Error «Sort»

Create a tuple sort.

• sorts The sorts of the elements of the tuple.

def cvc5.TermManager.mkUninterpretedSortConstructorSort? (v0 : TermManager) (v1 : Nat) (v2 : String) : Option «Sort»

Create an uninterpreted sort constructor sort.

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

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

Equations

• v0.mkUninterpretedSortConstructorSort? v1 v2 = (v0.mkUninterpretedSortConstructorSort v1 v2).toOption

@[extern termManager_mkUninterpretedSortConstructorSort]

opaque cvc5.TermManager.mkUninterpretedSortConstructorSort : TermManager → (arity : Nat) → (symbol : String) → Except Error «Sort»

Create an uninterpreted sort constructor sort.

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

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

def cvc5.TermManager.mkUninterpretedSortConstructorSort! (v0 : TermManager) (v1 : Nat) (v2 : String) : «Sort»

Create an uninterpreted sort constructor sort.

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

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

Equations

• v0.mkUninterpretedSortConstructorSort! v1 v2 = cvc5.Error.unwrap! (v0.mkUninterpretedSortConstructorSort v1 v2)

def cvc5.TermManager.mkSetSort! (v0 : TermManager) (v1 : «Sort») : «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

Equations

• v0.mkSetSort! v1 = cvc5.Error.unwrap! (v0.mkSetSort v1)

@[extern termManager_mkSetSort]

opaque cvc5.TermManager.mkSetSort : TermManager → (sort : «Sort») → Except Error «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

def cvc5.TermManager.mkSetSort? (v0 : TermManager) (v1 : «Sort») : Option «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

Equations

• v0.mkSetSort? v1 = (v0.mkSetSort v1).toOption

def cvc5.TermManager.mkBagSort! (v0 : TermManager) (v1 : «Sort») : «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

Equations

• v0.mkBagSort! v1 = cvc5.Error.unwrap! (v0.mkBagSort v1)

def cvc5.TermManager.mkBagSort? (v0 : TermManager) (v1 : «Sort») : Option «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

Equations

• v0.mkBagSort? v1 = (v0.mkBagSort v1).toOption

@[extern termManager_mkBagSort]

opaque cvc5.TermManager.mkBagSort : TermManager → (sort : «Sort») → Except Error «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

def cvc5.TermManager.mkSequenceSort? (v0 : TermManager) (v1 : «Sort») : Option «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

Equations

• v0.mkSequenceSort? v1 = (v0.mkSequenceSort v1).toOption

def cvc5.TermManager.mkSequenceSort! (v0 : TermManager) (v1 : «Sort») : «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

Equations

• v0.mkSequenceSort! v1 = cvc5.Error.unwrap! (v0.mkSequenceSort v1)

@[extern termManager_mkSequenceSort]

opaque cvc5.TermManager.mkSequenceSort : TermManager → (sort : «Sort») → Except Error «Sort»

Create a set parameter.

• elemSort The sort of the set elements.

@[extern termManager_mkAbstractSort]

opaque cvc5.TermManager.mkAbstractSort : TermManager → (k : SortKind) → Except Error «Sort»

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.

def cvc5.TermManager.mkAbstractSort? (v0 : TermManager) (v1 : SortKind) : Option «Sort»

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.

Equations

• v0.mkAbstractSort? v1 = (v0.mkAbstractSort v1).toOption

def cvc5.TermManager.mkAbstractSort! (v0 : TermManager) (v1 : SortKind) : «Sort»

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.

Equations

• v0.mkAbstractSort! v1 = cvc5.Error.unwrap! (v0.mkAbstractSort v1)

@[extern termManager_mkUninterpretedSort]

opaque cvc5.TermManager.mkUninterpretedSort : TermManager → (symbol : String) → «Sort»

Create an uninterpreted sort.

• symbol The name of the sort.

@[extern termManager_mkNullableSort]

opaque cvc5.TermManager.mkNullableSort : TermManager → (sort : «Sort») → Except Error «Sort»

Create a nullable sort.

• sort The sort of the element of the nullable.

def cvc5.TermManager.mkNullableSort? (v0 : TermManager) (v1 : «Sort») : Option «Sort»

Create a nullable sort.

• sort The sort of the element of the nullable.

Equations

• v0.mkNullableSort? v1 = (v0.mkNullableSort v1).toOption

def cvc5.TermManager.mkNullableSort! (v0 : TermManager) (v1 : «Sort») : «Sort»

Create a nullable sort.

• sort The sort of the element of the nullable.

Equations

• v0.mkNullableSort! v1 = cvc5.Error.unwrap! (v0.mkNullableSort v1)

@[extern termManager_mkParamSort]

opaque cvc5.TermManager.mkParamSort : TermManager → (symbol : String) → «Sort»

Create a sort parameter.

• symbol The name of the sort.

Warning: This function is experimental and may change in future versions.

@[extern termManager_mkBoolean]

opaque cvc5.TermManager.mkBoolean : TermManager → (b : Bool) → Term

Create a Boolean constant.

• b: The Boolean constant.

def cvc5.TermManager.mkInteger (tm : TermManager) : Int → Term

Create an integer-value term.

Equations

• tm.mkInteger = cvc5.Error.unwrap! ∘ cvc5.TermManager.mkIntegerFromString✝ tm ∘ toString

def cvc5.TermManager.mkReal (tm : TermManager) (num : Int) (den : Int := 1) (den_ne_0 : den ≠ 0 := by simp <;> omega) : Term

Create a real-value term from numerator/denominator Int-s.

Equations

• tm.mkReal num (Int.ofNat 0) den_ne_0 = match ⋯.elim with | (num, den) => tm.mkRealOfRat (Std.Internal.mkRat num den)
• tm.mkReal num (Int.ofNat den_2) den_ne_0 = tm.mkRealOfRat (Std.Internal.mkRat num den_2)
• tm.mkReal num (Int.negSucc denMinus1) den_ne_0 = tm.mkRealOfRat (Std.Internal.mkRat (-num) denMinus1.succ)

def cvc5.TermManager.mkRealOfRat (tm : TermManager) (rat : Std.Internal.Rat) : Term

Create a real-value term from a Std.Internal.Rat.

Equations

• tm.mkRealOfRat rat = cvc5.Error.unwrap! (cvc5.TermManager.mkRealFromString✝ tm (toString "" ++ toString rat.num ++ toString "/" ++ toString rat.den ++ toString ""))

@[extern termManager_mkOpOfIndices]

opaque cvc5.TermManager.mkOpOfIndices : TermManager → (kind : Kind) → (args : optParam (Array Nat) #[]) → Except Error Op

Create operator of Kind:

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

See cvc5.Kind for a description of the parameters.

• kind The kind of the operator.
• args The 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.

def cvc5.TermManager.mkOpOfIndices? (v0 : TermManager) (v1 : Kind) (v2 : Array Nat) : Option Op

Create operator of Kind:

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

See cvc5.Kind for a description of the parameters.

• kind The kind of the operator.
• args The 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

• v0.mkOpOfIndices? v1 v2 = (v0.mkOpOfIndices v1 v2).toOption

def cvc5.TermManager.mkOpOfIndices! (v0 : TermManager) (v1 : Kind) (v2 : Array Nat) : Op

Create operator of Kind:

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

See cvc5.Kind for a description of the parameters.

• kind The kind of the operator.
• args The 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

• v0.mkOpOfIndices! v1 v2 = cvc5.Error.unwrap! (v0.mkOpOfIndices v1 v2)

@[reducible, inline]

abbrev cvc5.TermManager.mkOp : TermManager → (kind : Kind) → (args : optParam (Array Nat) #[]) → Except Error Op

Create operator of Kind:

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

See cvc5.Kind for a description of the parameters.

• kind The kind of the operator.
• args The 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

• @cvc5.TermManager.mkOp = @cvc5.TermManager.mkOpOfIndices

@[reducible, inline]

abbrev cvc5.TermManager.mkOp! (v0 : TermManager) (v1 : Kind) (v2 : Array Nat) : Op

Create operator of Kind:

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

See cvc5.Kind for a description of the parameters.

• kind The kind of the operator.
• args The 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

• cvc5.TermManager.mkOp! = cvc5.TermManager.mkOpOfIndices!

@[reducible, inline]

abbrev cvc5.TermManager.mkOp? (v0 : TermManager) (v1 : Kind) (v2 : Array Nat) : Option Op

Create operator of Kind:

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

See cvc5.Kind for a description of the parameters.

• kind The kind of the operator.
• args The 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

• cvc5.TermManager.mkOp? = cvc5.TermManager.mkOpOfIndices?

def cvc5.TermManager.mkOpOfString! (v0 : TermManager) (v1 : Kind) (v2 : String) : Op

Create operator of kind:

• Kind.DIVISIBLE (to support arbitrary precision integers)

See cvc5.Kind for a description of the parameters.

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

Equations

• v0.mkOpOfString! v1 v2 = cvc5.Error.unwrap! (v0.mkOpOfString v1 v2)

def cvc5.TermManager.mkOpOfString? (v0 : TermManager) (v1 : Kind) (v2 : String) : Option Op

Create operator of kind:

• Kind.DIVISIBLE (to support arbitrary precision integers)

See cvc5.Kind for a description of the parameters.

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

Equations

• v0.mkOpOfString? v1 v2 = (v0.mkOpOfString v1 v2).toOption

@[extern termManager_mkOpOfString]

opaque cvc5.TermManager.mkOpOfString : TermManager → (kind : Kind) → (arg : String) → Except Error Op

Create operator of kind:

• Kind.DIVISIBLE (to support arbitrary precision integers)

See cvc5.Kind for a description of the parameters.

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

def cvc5.TermManager.mkTerm! (v0 : TermManager) (v1 : Kind) (v2 : Array Term) : Term

Create n-ary term of given kind.

• kind The kind of the term.
• children The children of the term.

Equations

• v0.mkTerm! v1 v2 = cvc5.Error.unwrap! (v0.mkTerm v1 v2)

@[extern termManager_mkTerm]

opaque cvc5.TermManager.mkTerm : TermManager → (kind : Kind) → (children : optParam (Array Term) #[]) → Except Error Term

Create n-ary term of given kind.

• kind The kind of the term.
• children The children of the term.

def cvc5.TermManager.mkTerm? (v0 : TermManager) (v1 : Kind) (v2 : Array Term) : Option Term

Create n-ary term of given kind.

• kind The kind of the term.
• children The children of the term.

Equations

• v0.mkTerm? v1 v2 = (v0.mkTerm v1 v2).toOption

@[extern termManager_mkTermOfOp]

opaque cvc5.TermManager.mkTermOfOp : TermManager → (op : Op) → (children : optParam (Array Term) #[]) → Except Error Term

Create n-ary term of given kind from a given operator.

Create operators with mkOp.

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

def cvc5.TermManager.mkTermOfOp? (v0 : TermManager) (v1 : Op) (v2 : Array Term) : Option Term

Create n-ary term of given kind from a given operator.

Create operators with mkOp.

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

Equations

• v0.mkTermOfOp? v1 v2 = (v0.mkTermOfOp v1 v2).toOption

def cvc5.TermManager.mkTermOfOp! (v0 : TermManager) (v1 : Op) (v2 : Array Term) : Term

Create n-ary term of given kind from a given operator.

Create operators with mkOp.

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

Equations

• v0.mkTermOfOp! v1 v2 = cvc5.Error.unwrap! (v0.mkTermOfOp v1 v2)

@[extern solver_getVersion]

opaque cvc5.Solver.getVersion {m : Type → Type u_1} [Monad m] : SolverT m String

Get a string representation of the version of this solver.

@[extern solver_setOption]

opaque cvc5.Solver.setOption {m : Type → Type u_1} [Monad m] (option value : String) : SolverT m Unit

Set option.

• option: The option name.
• value: The option value.

@[extern solver_resetAssertions]

opaque cvc5.Solver.resetAssertions {m : Type → Type u_1} [Monad m] : SolverT m Unit

Remove all assertions.

@[extern solver_setLogic]

opaque cvc5.Solver.setLogic {m : Type → Type u_1} [Monad m] (logic : String) : SolverT m Unit

Set logic.

• logic: The logic to set.

@[extern solver_simplify]

opaque cvc5.Solver.simplify {m : Type → Type u_1} [Monad m] (term : Term) (applySubs : Bool := false) : SolverT m Term

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.

• t The term to simplify.
• applySubs True to apply substitutions for solved variables.

@[extern solver_declareFun]

opaque cvc5.Solver.declareFun {m : Type → Type u_1} [Monad m] (symbol : String) (sorts : Array «Sort») (sort : «Sort») (fresh : Bool := true) : SolverT m Term

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.

@[extern solver_assertFormula]

opaque cvc5.Solver.assertFormula {m : Type → Type u_1} [Monad m] : Term → SolverT m Unit

Assert a formula.

• term: The formula to assert.

@[extern solver_checkSat]

opaque cvc5.Solver.checkSat {m : Type → Type u_1} [Monad m] : SolverT m Result

Check satisfiability.

@[extern solver_checkSatAssuming]

opaque cvc5.Solver.checkSatAssuming {m : Type → Type u_1} [Monad m] (assumptions : Array Term) : SolverT m Result

Check satisfiability assuming the given formulas.

• assumptions: The formulas to assume.

@[extern solver_getProof]

opaque cvc5.Solver.getProof {m : Type → Type u_1} [Monad m] : SolverT m (Array Proof)

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

Requires to enable option produce-proofs.

@[extern solver_getValue]

opaque cvc5.Solver.getValue {m : Type → Type u_1} [Monad m] (term : Term) : SolverT m Term

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

SMT-LIB:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(get-value ( <term>* ))

\endverbatim

• terms: The term for which the value is queried.

@[extern solver_getValues]

opaque cvc5.Solver.getValues {m : Type → Type u_1} [Monad m] (terms : Array Term) : SolverT m (Array Term)

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.

@[extern solver_proofToString]

opaque cvc5.Solver.proofToString {m : Type → Type u_1} [Monad m] : Proof → SolverT m String

Prints a proof as a string in a selected proof format mode.

Other aspects of printing are taken from the solver options.

• proof: A proof, usually obtained from getProof.

@[extern solver_parseCommands]

opaque cvc5.Solver.parseCommands {m : Type → Type u_1} [Monad m] : String → SolverT m Unit

Parse a string containing SMT-LIB commands.

Commands that produce a result such as (check-sat), (get-model), ... are executed but the results are ignored.

def cvc5.Solver.run {m : Type → Type u_1} [Monad m] {α : Type} (tm : TermManager) (query : SolverT m α) : m (Except Error α)

Run a query given a term manager tm.

Equations

• One or more equations did not get rendered due to their size.

def cvc5.Solver.run! {m : Type → Type u_1} [Monad m] {α : Type} [Inhabited α] (tm : TermManager) (query : SolverT m α) : m α

Run a query given a term manager tm.

Equations

• One or more equations did not get rendered due to their size.