Sort constructors live in the Srt namespace and are all in the Env monad.
#eval Env.runIO do
let b ← Srt.bool
let r ← Srt.real
let mapBoolReal ← b.arrayTo r
-- alternatively
let mapBoolReal' ← r.arrayFrom b
let ff ← Srt.finiteField 7
let f1 ← Srt.function #[b] r
let f2 ← Srt.function #[r, b] r
println! "b := {b}"
println! "r := {r}"
println! "mapBoolReal := {mapBoolReal}"
println! "mapBoolReal' := {mapBoolReal'}"
println! "ff := {ff}"
println! "f1 := {f1}"
println! "f2 := {f2}"
Srt
Cvc.lean associates some Lean types to cvc5-sorts Srt through the ToTyp class.
The sort a Lean type denotes, which lets it index terms.
For a declared datatype, name it and declare it in the scope before use:
instance : ToTyp Pair := ⟨.datatype "Pair"⟩.
Instance Constructor
Cvc.ToTyp.mk
ToTyp α specifies a Typ-value for α that corresponds to a Srt.Marginal noteBut is not a Srt as constructing one requires to be in Env: a Srt value is tied to a specific manager. This lets us go from compatible Lean types to Srt easily.
#eval Env.runIO do
let b ← Srt.of Bool
println! "b := {b}"
let i ← Srt.of Int
println! "i := {i}"
let r ← Srt.of Rat
println! "r := {r}"
let bv ← Srt.of (BitVec 8)
println! "bv := {bv}"
let f1 ← Srt.of (Int → Bool → Rat)
println! "f1 := {f1}"
Some cvc5-sorts do not map nicely to builtin Lean types however, so cvc.lean has a few custom types with ToTyp instances.Marginal noteIn the following, Float refers to Cvc.Float, not the Lean builtin type for floating point numbers. Here are a few examples:
#eval Env.runIO do
let f ← Srt.of (Float 8 24)
println! "f := {f}"
let arr ← Srt.of (TotalMap Int Rat)
println! "arr := {arr}"
let ff ← Srt.of (FiniteField 7)
println! "ff := {ff}"
let bag ← Srt.of (Bag (Float 8 24))
println! "bag := {bag}"