8000
Skip to content

cvc5.lean

Latest commit

 

History

History
3039 lines (2059 loc) · 96.1 KB

cvc5.lean

File metadata and controls

3039 lines (2059 loc) · 96.1 KB
/-
Copyright (c) 2023-2024 by the authors listed in the file AUTHORS and their
institutional affiliations. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Abdalrhman Mohamed, Adrien Champion
-/
import cvc5.Init
import cvc5.Kind
import cvc5.ProofRule
import cvc5.SkolemId
import cvc5.Types
@[export prod_mk_generic]
private def mkProd := @Prod.mk
namespace cvc5
namespace Kind
/-- Produces a string representation. -/
@[extern "kind_toString"]
protected opaque toString : Kind → String
instance : ToString Kind := ⟨Kind.toString⟩
/-- Produces a hash. -/
@[extern "kind_hash"]
protected opaque hash : Kind → UInt64
instance : Hashable Kind := ⟨Kind.hash⟩
end Kind
namespace SortKind
/-- Produces a string representation. -/
@[extern "sortKind_toString"]
protected opaque toString : SortKind → String
instance : ToString SortKind := ⟨SortKind.toString⟩
/-- Produces a hash. -/
@[extern "sortKind_hash"]
protected opaque hash : SortKind → UInt64
instance : Hashable SortKind := ⟨SortKind.hash⟩
end SortKind
namespace ProofRule
/-- Produces a string representation. -/
@[extern "proofRule_toString"]
protected opaque toString : ProofRule → String
instance : ToString ProofRule := ⟨ProofRule.toString⟩
/-- Produces a hash. -/
@[extern "proofRule_hash"]
protected opaque hash : ProofRule → UInt64
instance : Hashable ProofRule := ⟨ProofRule.hash⟩
end ProofRule
namespace SkolemId
/-- Produces a string representation. -/
@[extern "skolemId_toString"]
protected opaque toString : SkolemId → String
instance : ToString SkolemId := ⟨SkolemId.toString⟩
/-- Produces a hash. -/
@[extern "skolemId_hash"]
protected opaque hash : SkolemId → UInt64
instance : Hashable SkolemId := ⟨SkolemId.hash⟩
end SkolemId
namespace ProofRewriteRule
/-- Produces a string representation. -/
@[extern "proofRewriteRule_toString"]
protected opaque toString : ProofRewriteRule → String
instance : ToString ProofRewriteRule := ⟨ProofRewriteRule.toString⟩
/-- Produces a hash. -/
@[extern "proofRewriteRule_hash"]
protected opaque hash : ProofRewriteRule → UInt64
instance : Hashable ProofRewriteRule := ⟨ProofRewriteRule.hash⟩
end ProofRewriteRule
namespace UnknownExplanation
/-- Produces a string representation. -/
@[extern "unknownExplanation_toString"]
protected opaque toString : UnknownExplanation → String
instance : ToString UnknownExplanation := ⟨UnknownExplanation.toString⟩
/-- Produces a hash. -/
@[extern "unknownExplanation_hash"]
protected opaque hash : UnknownExplanation → UInt64
instance : Hashable UnknownExplanation := ⟨UnknownExplanation.hash⟩
end UnknownExplanation
namespace RoundingMode
/-- Produces a string representation. -/
@[extern "roundingMode_toString"]
protected opaque toString : RoundingMode → String
instance : ToString RoundingMode := ⟨RoundingMode.toString⟩
/-- Produces a hash. -/
@[extern "roundingMode_hash"]
protected opaque hash : RoundingMode → UInt64
instance : Hashable RoundingMode := ⟨RoundingMode.hash⟩
end RoundingMode
namespace BlockModelsMode
/-- Produces a string representation. -/
@[extern "blockModelsMode_toString"]
protected opaque toString : BlockModelsMode → String
instance : ToString BlockModelsMode := ⟨BlockModelsMode.toString⟩
/-- Produces a hash. -/
@[extern "blockModelsMode_hash"]
protected opaque hash : BlockModelsMode → UInt64
instance : Hashable BlockModelsMode := ⟨BlockModelsMode.hash⟩
end BlockModelsMode
namespace LearnedLitType
/-- Produces a string representation. -/
@[extern "learnedLitType_toString"]
protected opaque toString : LearnedLitType → String
instance : ToString LearnedLitType := ⟨LearnedLitType.toString⟩
/-- Produces a hash. -/
@[extern "learnedLitType_hash"]
protected opaque hash : LearnedLitType → UInt64
instance : Hashable LearnedLitType := ⟨LearnedLitType.hash⟩
end LearnedLitType
namespace ProofComponent
/-- Produces a string representation. -/
@[extern "proofComponent_toString"]
protected opaque toString : ProofComponent → String
instance : ToString ProofComponent := ⟨ProofComponent.toString⟩
/-- Produces a hash. -/
@[extern "proofComponent_hash"]
protected opaque hash : ProofComponent → UInt64
instance : Hashable ProofComponent := ⟨ProofComponent.hash⟩
end ProofComponent
namespace ProofFormat
/-- Produces a string representation. -/
@[extern "proofFormat_toString"]
protected opaque toString : ProofFormat → String
instance : ToString ProofFormat := ⟨ProofFormat.toString⟩
/-- Produces a hash. -/
@[extern "proofFormat_hash"]
protected opaque hash : ProofFormat → UInt64
instance : Hashable ProofFormat := ⟨ProofFormat.hash⟩
end ProofFormat
namespace FindSynthTarget
/-- Produces a string representation. -/
@[extern "findSynthTarget_toString"]
protected opaque toString : FindSynthTarget → String
instance : ToString FindSynthTarget := ⟨FindSynthTarget.toString⟩
/-- Produces a hash. -/
@[extern "findSynthTarget_hash"]
protected opaque hash : FindSynthTarget → UInt64
instance : Hashable FindSynthTarget := ⟨FindSynthTarget.hash⟩
end FindSynthTarget
namespace InputLanguage
/-- Produces a string representation. -/
@[extern "inputLanguage_toString"]
protected opaque toString : InputLanguage → String
instance : ToString InputLanguage := ⟨InputLanguage.toString⟩
/-- Produces a hash. -/
@[extern "inputLanguage_hash"]
protected opaque hash : InputLanguage → UInt64
instance : Hashable InputLanguage := ⟨InputLanguage.hash⟩
end InputLanguage
private opaque ResultImpl : NonemptyType.{0}
/-- Encapsulation of a three-valued solver result, with explanations. -/
def Result : Type := ResultImpl.type
instance Result.instNonemptyResult : Nonempty Result := ResultImpl.property
private opaque SynthResultImpl : NonemptyType.{0}
/-- Encapsulation of a three-valued solver result, with explanations. -/
def SynthResult : Type := SynthResultImpl.type
instance SynthResult.instNonemptySynthResult : Nonempty SynthResult := SynthResultImpl.property
private opaque SortImpl : NonemptyType.{0}
end cvc5
/-- The sort of a cvc5 term. -/
def cvc5.Sort : Type := cvc5.SortImpl.type
namespace cvc5
instance Sort.instNonemptySort : Nonempty cvc5.Sort := SortImpl.property
private opaque OpImpl : NonemptyType.{0}
/-- 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`.
-/
def Op : Type := OpImpl.type
instance Op.instNonemptyOp : Nonempty Op := OpImpl.property
private opaque TermImpl : NonemptyType.{0}
/-- A cvc5 term. -/
def Term : Type := TermImpl.type
instance Term.instNonemptyTerm : Nonempty Term := TermImpl.property
private opaque ProofImpl : NonemptyType.{0}
/-- 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.
-/
def Proof : Type := ProofImpl.type
instance Proof.instNonemptyProof : Nonempty Proof := ProofImpl.property
/-- Error type. -/
inductive Error where
| missingValue
| error (msg : String)
| recoverable (msg : String)
| unsupported (msg : String)
| option (msg : String)
deriving 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)`.
-/
abbrev EnvT (m : Type → Type) (α : Type) : Type :=
ExceptT Error m α
/-- Cvc5 environment monad in `BaseIO`. -/
abbrev Env (α : Type) := EnvT BaseIO α
namespace EnvT
-- functions used by the underlying C++ layer
section ffi variable [Monad m]
@[export env_pure]
private def env_pure (a : α) : Env α := return a
@[export env_bool]
private def env_bool (b : Bool) : Env Bool := return b
@[export env_uint64]
private def env_uint64 (u : UInt64) : Env UInt64 := return u
@[export env_throw]
private def env_throw (e : Error) : Env α := throw e
@[export env_throw_string]
private def env_throw_string (e : String) : Env α := throw <| (.error e)
end ffi
end EnvT
namespace Error
/-- String representation of an error. -/
protected def toString : Error → String :=
toString ∘ repr
/-- Panics on errors, otherwise yields the `ok` result. -/
def unwrap! [Inhabited α] : Except Error α → α
| .ok a => a
| .error e => panic! e.toString
instance : ToString Error :=
⟨Error.toString⟩
end Error
private opaque TermManagerImpl : NonemptyType.{0}
/-- Manager for cvc5 terms. -/
def TermManager : Type := TermManagerImpl.type
namespace TermManager
instance : Nonempty TermManager := TermManagerImpl.property
/-- Constructor. -/
extern_def new : Env TermManager
end TermManager
private opaque SolverImpl : NonemptyType.{0}
/-- A cvc5 solver. -/
def Solver : Type := SolverImpl.type
namespace Solver
instance : Nonempty Solver := SolverImpl.property
/-- Constructor.
- `tm` The associated term manager instance.
-/
extern_def new : (tm : TermManager) → Env Solver
end Solver
private opaque DatatypeConstructorDeclImpl : NonemptyType.{0}
/-- A cvc5 datatype constructor declaration.
A datatype constructor declaration is a specification used for creating a datatype constructor.
-/
def DatatypeConstructorDecl : Type := DatatypeConstructorDeclImpl.type
namespace DatatypeConstructorDecl
instance : Nonempty DatatypeConstructorDecl := DatatypeConstructorDeclImpl.property
/-- A string representation of this datatype constructor declaration. -/
protected extern_def toString : DatatypeConstructorDecl → String
instance : ToString DatatypeConstructorDecl := ⟨DatatypeConstructorDecl.toString⟩
end DatatypeConstructorDecl
private opaque DatatypeDeclImpl : NonemptyType.{0}
/-- 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.mkDatatypeSort`
- `Solver.mkDatatypeSorts`
-/
def DatatypeDecl : Type := DatatypeDeclImpl.type
namespace DatatypeDecl
instance : Nonempty DatatypeDecl := DatatypeDeclImpl.property
/-- Get a string representation of this datatype declaration. -/
protected extern_def toString : DatatypeDecl → String
instance : ToString DatatypeDecl := ⟨DatatypeDecl.toString⟩
end DatatypeDecl
private opaque DatatypeSelectorImpl : NonemptyType.{0}
/-- A cvc5 datatype selector. -/
def DatatypeSelector : Type := DatatypeSelectorImpl.type
namespace DatatypeSelector
instance : Nonempty DatatypeSelector := DatatypeSelectorImpl.property
/-- Gte the string representation of this datatype selector. -/
protected extern_def toString : DatatypeSelector → String
instance : ToString DatatypeSelector := ⟨DatatypeSelector.toString⟩
end DatatypeSelector
private opaque DatatypeConstructorImpl : NonemptyType.{0}
/-- A cvc5 datatype constructor. -/
def DatatypeConstructor : Type := DatatypeConstructorImpl.type
namespace DatatypeConstructor
instance : Nonempty DatatypeConstructor := DatatypeConstructorImpl.property
/-- A string representation of this datatype. -/
protected extern_def toString : DatatypeConstructor → String
instance : ToString DatatypeConstructor := ⟨DatatypeConstructor.toString⟩
end DatatypeConstructor
private opaque DatatypeImpl : NonemptyType.{0}
/-- A cvc5 datatype. -/
def Datatype : Type := DatatypeImpl.type
namespace Datatype
instance : Nonempty Datatype := DatatypeImpl.property
/-- A string representation of this datatype. -/
protected extern_def toString : Datatype → String
instance : ToString Datatype := ⟨Datatype.toString⟩
end Datatype
private opaque GrammarImpl : NonemptyType.{0}
/-- 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.
-/
def Grammar : Type := GrammarImpl.type
namespace Grammar
instance : Nonempty Grammar := GrammarImpl.property
/-- A string representation of this grammar. -/
protected extern_def toString : Grammar → String
instance : ToString Grammar := ⟨Grammar.toString⟩
end Grammar
private opaque CommandImpl : NonemptyType.{0}
/-- Encapsulation of a command.
Commands are constructed by the `InputParser` and can be invoked on the `Solver` and
`Command`.
-/
def Command : Type := CommandImpl.type
namespace Command
instance : Nonempty Command := CommandImpl.property
/-- Get a string representation of this command. -/
protected extern_def toString : Command → String
instance : ToString Command := ⟨Command.toString⟩
end Command
private opaque SymbolManagerImpl : NonemptyType.{0}
/-- 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.
-/
def SymbolManager : Type := SymbolManagerImpl.type
namespace SymbolManager
instance SymbolManager.instNonempty : Nonempty SymbolManager := SymbolManagerImpl.property
/-- Constructor.
- `tm` The associated term manager instance.
-/
extern_def new : (tm : TermManager) → Env SymbolManager
end SymbolManager
private opaque InputParserImpl : NonemptyType.{0}
/-- 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.
-/
def InputParser : Type := InputParserImpl.type
namespace InputParser
instance : Nonempty InputParser := InputParserImpl.property
/-- Construct an input parser with an initially empty symbol manager.
- `solver`: The solver (e.g. for constructing terms and sorts).
-/
private extern_def ofSolver : (solver : Solver) → Env InputParser
/-- Construct an input parser.
- `solver` The solver (e.g. for constructing terms and sorts).
- `sm` The symbol manager, which contains a symbol table that maps symbols to terms and sorts. Must
have a logic that is compatible with the solver.
-/
private extern_def ofSolverAndSM : (solver : Solver) → (sm : SymbolManager) → Env InputParser
@[inherit_doc ofSolverAndSM]
def new (solver : Solver) : (sm : Option SymbolManager := none) → Env InputParser
| none => ofSolver solver
| some sm => ofSolverAndSM solver sm
end InputParser
namespace Result
/-- Comparison for structural equality. -/
protected extern_def beq : Result → Result → Bool
instance : BEq Result := ⟨Result.beq⟩
/-- Hash function for cvc5 sorts. -/
protected extern_def hash : Result → UInt64
instance : Hashable Result := ⟨Result.hash⟩
/-- True if this result is from a satisfiable `checkSat` or `checkSatAssuming` query. -/
extern_def isSat : Result → Bool
/-- True if this result is from a unsatisfiable `checkSat` or `checkSatAssuming` query. -/
extern_def isUnsat : Result → Bool
/-- True if this result is from a `checkSat` or `checkSatAssuming` query and cvc5 was not able to
determine (un)satisfiability.
-/
extern_def isUnknown : Result → Bool
/-- An explanation for an unknown query result.
Note that if the result is (un)sat, this function returns `UnknownExplanation.UNKNOWN_REASON`.
-/
extern_def getUnknownExplanation : Result → UnknownExplanation
with
/-- An explanation for an unknown query result, `none` if the result in not unknown. -/
getUnknownExplanation? (res : Result) : Option UnknownExplanation :=
if ¬ res.isUnknown then none else res.getUnknownExplanation
/-- A string representation of this result. -/
protected extern_def toString : Result → String
instance : ToString Result := ⟨Result.toString⟩
end Result
namespace SynthResult
/-- A string representation of this synthesis result. -/
protected extern_def toString : SynthResult → String
instance : ToString SynthResult := ⟨SynthResult.toString⟩
/-- Hash function for synthesis results. -/
protected extern_def hash : SynthResult → UInt64
instance : Hashable SynthResult := ⟨SynthResult.hash⟩
/-- Equality of two synthesis results. -/
protected extern_def beq : SynthResult → SynthResult → Bool
instance : BEq SynthResult := ⟨SynthResult.beq⟩
/-- Determine if a given synthesis result is empty (a nullary result) and not an actual result
returned from a synthesis query.
-/
extern_def isNull : SynthResult → Bool
/-- True if the synthesis query has a solution. -/
extern_def hasSolution : SynthResult → Bool
/-- True if the synthesis query has no solution. In this case, it was determined that there was no
solution.
-/
extern_def hasNoSolution : SynthResult → Bool
/-- True if the result of the synthesis query could not be determined. -/
extern_def isUnknown : SynthResult → Bool
end SynthResult
section ffi_except_constructors
/-- 992E Only used by FFI to inject values. -/
@[export generic_except_ok]
private def mkExceptOk {α : Type} : α → Except Error α := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_bool]
private def mkExceptOkBool : Bool → Except Error Bool := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_i64]
private def mkExceptOkI64 : Int64 → Except Error Int64 := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_u64]
private def mkExceptOkU64 : Int64 → Except Error Int64 := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_u32]
private def mkExceptOkU32 : UInt32 → Except Error UInt32 := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_i32]
private def mkExceptOkI32 : Int32 → Except Error Int32 := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_u16]
private def mkExceptOkU16 : UInt16 → Except Error UInt16 := .ok
/-- Only used by FFI to inject values. -/
@[export except_ok_u8]
private def mkExceptOkU8 : UInt8 → Except Error UInt8 := .ok
/-- Only used by FFI to inject errors. -/
@[export generic_except_err]
private def mkExceptErr {α : Type} : Error → Except Error α := .error
/-- Only used by FFI to inject errors. -/
@[export generic_except_err_of_string]
private def mkExceptErrOfString {α : Type} : String → Except Error α := .error ∘ Error.error
end ffi_except_constructors
namespace DatatypeConstructorDecl
/-- The null datatype constructor declaration. -/
extern_def null : Unit → DatatypeConstructorDecl
/-- True if this `DatatypeConstructorDecl` is a null declaration. -/
extern_def isNull : DatatypeConstructorDecl → Bool
/-- Equality operator. -/
protected extern_def beq : DatatypeConstructorDecl → DatatypeConstructorDecl → Bool
instance : BEq DatatypeConstructorDecl := ⟨DatatypeConstructorDecl.beq⟩
/-- Hash function for datatype declarations. -/
protected extern_def hash : DatatypeConstructorDecl → UInt64
instance : Hashable DatatypeConstructorDecl := ⟨DatatypeConstructorDecl.hash⟩
/-- Add datatype selector declaration.
- `name` The name of the datatype selector declaration to add.
- `sort` The codomain sort of the datatype selector declaration to add.
-/
extern_def addSelector :
(dtCons : DatatypeConstructorDecl) → (name : String) → (sort : cvc5.Sort) →
Env DatatypeConstructorDecl
/-- Add datatype selector declaration whose codomain type is the datatype itself.
- `name` The name of the datatype selector declaration to add.
-/
extern_def addSelectorSelf :
(dtCons : DatatypeConstructorDecl) → (name : String) → Env DatatypeConstructorDecl
/-- Add datatype selector declaration whose codomain sort is an unresolved datatype with the given
name.
- `name` The name of the datatype selector declaration to add.
- `unresDatatypeName` The name of the unresolved datatype. The codomain of the selector will be the
resolved datatype with the given name
-/
extern_def addSelectorUnresolved :
(dtCons : DatatypeConstructorDecl) → (name : String) → (unresDatatypeName : String) →
Env DatatypeConstructorDecl
end DatatypeConstructorDecl
namespace DatatypeDecl
/-- The null datatype declaration. -/
extern_def null : Unit → DatatypeDecl
instance : Inhabited DatatypeDecl := ⟨null ()⟩
/-- Determine if this datatype declaration is nullary. -/
extern_def isNull : DatatypeDecl → Bool
/-- Equality operator. -/
protected extern_def beq : DatatypeDecl → DatatypeDecl → Bool
instance : BEq DatatypeDecl := ⟨DatatypeDecl.beq⟩
/-- Hash function for datatype declarations. -/
protected extern_def hash : DatatypeDecl → UInt64
instance : Hashable DatatypeDecl := ⟨DatatypeDecl.hash⟩
/-- Add datatype constructor declaration.
- `ctor` The datatype constructor declaration to add.
-/
extern_def addConstructor :
DatatypeDecl → (ctor : DatatypeConstructorDecl) → Env DatatypeDecl
/-- Get the number of constructors for this datatype declaration. -/
extern_def getNumConstructors : DatatypeDecl → Nat
/-- Determine if this datatype declaration is parametric.
**Warning**: this function is experimental and may change in future versions.
-/
extern_def isParametric : DatatypeDecl → Bool
/-- Get the name of this datatype declaration. -/
extern_def!? getName : DatatypeDecl → Except Error String
/-- Determine if this datatype declaration is resolved (has already been used to declare a
datatype).
-/
extern_def isResolved : DatatypeDecl → Env Bool
end DatatypeDecl
namespace DatatypeSelector
/-- The null datatype constructor. -/
extern_def null : Unit → DatatypeSelector
instance : Inhabited DatatypeSelector := ⟨null ()⟩
/-- True if this datatype is a null object. -/
extern_def isNull : DatatypeSelector → Bool
/-- Equality operator. -/
protected extern_def beq : DatatypeSelector → DatatypeSelector → Bool
instance : BEq DatatypeSelector := ⟨DatatypeSelector.beq⟩
/-- Hash function for datatype selectors. -/
protected extern_def hash : DatatypeSelector → UInt64
instance : Hashable DatatypeSelector := ⟨DatatypeSelector.hash⟩
7292
/-- Get the name of this datatype selector. -/
extern_def!? getName : DatatypeSelector → Except Error String
/-- 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`.
-/
extern_def getTerm : DatatypeSelector → Env Term
/-- 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`.
-/
extern_def getUpdaterTerm : DatatypeSelector → Env Term
/-- Get the codomain sort of this selector. -/
extern_def getCodomainSort : DatatypeSelector → Env cvc5.Sort
end DatatypeSelector
namespace DatatypeConstructor
/-- The null datatype constructor. -/
extern_def null : Unit → DatatypeConstructor
instance : Inhabited DatatypeConstructor := ⟨null ()⟩
/-- True if this datatype is a null object. -/
extern_def isNull : DatatypeConstructor → Bool
/-- Equality operator. -/
protected extern_def beq : DatatypeConstructor → DatatypeConstructor → Bool
instance : BEq DatatypeConstructor := ⟨DatatypeConstructor.beq⟩
/-- Hash function for datatype constructors. -/
protected extern_def hash : DatatypeConstructor → UInt64
instance : Hashable DatatypeConstructor := ⟨DatatypeConstructor.hash⟩
/-- Get the name of this datatype constructor. -/
extern_def!? getName : DatatypeConstructor → Except Error String
/-- 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`.
-/
extern_def getTerm : DatatypeConstructor → Env Term
/-- 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:
```smtlib
(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:
```smtlib
(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.
- `retSort` The desired return sort of the constructor.
-/
extern_def getInstantiatedTerm : DatatypeConstructor → (retSort : cvc5.Sort) → Env Term
/-- 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`.
-/
extern_def getTesterTerm : DatatypeConstructor → Env Term
/-- The number of selectors of this datatype constructor. -/
extern_def getNumSelectors : DatatypeConstructor → Nat
/-- 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.
- `name` The name of the datatype selector.
-/
extern_def getSelector : DatatypeConstructor → (name : String) → Env DatatypeSelector
/-- The datatype selector at index `idx`. -/
extern_def getSelectorAt :
(dtCons : DatatypeConstructor) → (idx : Fin dtCons.getNumSelectors) → DatatypeSelector
instance : GetElem DatatypeConstructor Nat DatatypeSelector
fun dt idx => idx < dt.getNumSelectors
where
getElem dt idx h := dt.getSelectorAt ⟨idx, h⟩
instance [Monad m] : ForIn m DatatypeConstructor DatatypeSelector where
forIn dtCons init fold := forIn' [:dtCons.getNumSelectors] init fun idx h_member acc =>
let selector := dtCons.getSelectorAt ⟨idx, h_member.upper⟩
fold selector acc
end DatatypeConstructor
namespace Datatype
/-- The null datatype. -/
extern_def null : Unit → Datatype
instance : Inhabited Datatype := ⟨null ()⟩
/-- True if this datatype is a null object. -/
extern_def isNull : Datatype → Bool
/-- Equality operator. -/
protected extern_def beq : Datatype → Datatype → Bool
instance : BEq Datatype := ⟨Datatype.beq⟩
/-- Hash function for datatypes. -/
protected extern_def hash : Datatype → UInt64
instance : Hashable Datatype := ⟨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.
- `name` The name of the datatype constructor.
-/
extern_def getConstructor : Datatype → (name : String) → Env DatatypeConstructor
/-- Get the number of constructors of this datatype. -/
extern_def getNumConstructors : Datatype → Nat
/-- Get the datatype constructor at a given index.
- `idx` The index of the datatype constructor to return.
-/
extern_def getConstructorAt :
(dt : Datatype) → (idx : Fin dt.getNumConstructors) → DatatypeConstructor
instance : GetElem Datatype Nat DatatypeConstructor
fun dt idx => idx < dt.getNumConstructors
where
getElem dt idx h := dt.getConstructorAt ⟨idx, h⟩
instance [Monad m] : ForIn m Datatype DatatypeConstructor where
forIn dt init fold := forIn' [:dt.getNumConstructors] init fun idx h_member acc =>
let constructor := dt.getConstructorAt ⟨idx, h_member.upper⟩
fold constructor acc
/-- 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.
- `name` The name of the datatype selector.
-/
extern_def getSelector : Datatype → (name : String) → Env DatatypeSelector
View remainder of file in raw view
0