Functions and monads for term, term building, SMT etc. helpers and monads

structure Cvc.Term (α : Type) : Type

Type-safe cvc5 terms, input type expected to be IsSrt for most uses.

• No direct constructor exposed publicly, users must go through the Term.Build monadic constructors.

• ofUnsafe :: (
• hasSymbols : Bool

  True if the term mentions symbols.

• toUnsafe : cvc5.Term

  Underlying unsafe term.

• )

@[reducible, inline]

abbrev Cvc.Formula : Type

Abbreviation for a Term Bool.

Equations

• Cvc.Formula = Cvc.Term Bool

@[reducible, inline]

abbrev Cvc.Term.Bool : Type

Boolean terms: Term Bool.

Equations

• Cvc.Term.Bool = Cvc.Term Bool

@[reducible, inline]

abbrev Cvc.Term.Int : Type

Integer terms: Term Int.

Equations

• Cvc.Term.Int = Cvc.Term Int

@[reducible, inline]

abbrev Cvc.Term.Real : Type

Real/Rat terms: Term Rat.

Equations

• Cvc.Term.Real = Cvc.Term Rat

@[reducible, inline]

abbrev Cvc.Term.String : Type

String terms: Term String.

Equations

• Cvc.Term.String = Cvc.Term String

@[reducible, inline]

abbrev Cvc.Term.Array (α β : Type) : Type

Array terms.

Equations

• Cvc.Term.Array α β = Cvc.Term (Cvc.TMap α β)

@[reducible, inline]

abbrev Cvc.Term.Seq (α : Type) : Type

Sequence terms.

Equations

• Cvc.Term.Seq α = Cvc.Term (Array α)

@[reducible, inline]

abbrev Cvc.Term.Fun (α β : Type) : Type

Function terms.

Equations

• Cvc.Term.Fun α β = Cvc.Term (α → β)

@[reducible, inline]

abbrev Cvc.Term.Prod (α β : Type) : Type

Product terms.

Equations

• Cvc.Term.Prod α β = Cvc.Term (α × β)

@[reducible, inline]

abbrev Cvc.Term.srt {α : Type} [A : IsSrt α] (term : Term α) : Srt

Sort of some term.

Note that due to strong-typing, this function does not perform any FFI.

Equations

• Cvc.Term.srt = Cvc.𝕂 (Cvc.IsSrt.srt α)

theorem Cvc.Term.srt_bij {α : Type} [A : IsSrt α] (term : Term α) : α = term.srt.toType

def Cvc.Term.retype {α : Type} [A : IsSrt α] (term : Term α) : Term term.srt.toType

Re-types t in terms of the type of t.srt.

Equations

• term.retype = ⋯ ▸ term

def Cvc.Term.inspectSrt {α : Type} [A : IsSrt α] (term : Term α) {β : Sort u_1} (f : (srt : Srt) → Term srt.toType → β) : β

Helper for dependent-pattern-matching the sort of a term.

Equations

• term.inspectSrt f = f term.srt term.retype

def Cvc.Term.toSmtString {α : Type} (term : Term α) : String

SMT-LIB string representation.

Equations

• term.toSmtString = term.toUnsafe.toString

instance Cvc.Term.instToString {α : Type} : ToString (Term α)

Equations

• Cvc.Term.instToString = { toString := Cvc.Term.toSmtString }

Term building

structure Cvc.Term.Build.State : Type

State of the term builder monad.

• mk' :: (
• manager : cvc5.TermManager

  Term manager.

• logic : Logic.Builder

  Logic builder, used to track the logic necessary to express the terms actually built.

  Updated when building terms.

• )

def Cvc.Term.Build.State.ofManager (manager : cvc5.TermManager) (logic : Logic.Builder := Logic.Builder.mk) : State

Constructor from a term manager.

Equations

• Cvc.Term.Build.State.ofManager manager logic = { manager := manager, logic := logic }

def Cvc.Term.Build.State.mk : BaseIO State

Creates a new term builder state.

Equations

• Cvc.Term.Build.State.mk = (fun (manager : cvc5.TermManager) => Cvc.Term.Build.State.ofManager manager) <$> cvc5.TermManager.new

@[reducible, inline]

abbrev Cvc.Term.BuildT (m : Type → Type u) (α : Type) : Type u

Term-building error-state-monad transformer.

Equations

• Cvc.Term.BuildT m = Cvc.ResT (StateT Cvc.Term.Build.State m)

@[reducible, inline]

abbrev Cvc.Term.BuildIO (α : Type) : Type

Term-building error-state-monad in IO.

Equations

• Cvc.Term.BuildIO = Cvc.Term.BuildT IO

@[reducible, inline]

abbrev Cvc.Term.Build (α : Type) : Type

Plain term-building error-state-monad.

Equations

• Cvc.Term.Build = Cvc.Term.BuildT Id

instance Cvc.Term.BuildT.instMonadLiftExceptErrorBuild : MonadLift (Except cvc5.Error) Build

Equations

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

instance Cvc.Term.BuildT.instMonadLiftBuildOfMonad {m : Type → Type u_1} [Monad m] : MonadLift Build (BuildT m)

Equations

• Cvc.Term.BuildT.instMonadLiftBuildOfMonad = { monadLift := fun {α : Type} (code : Cvc.Term.Build α) (state : Cvc.Term.Build.State) => pure (code state) }

instance Cvc.Term.BuildT.instMonadLiftBuildIOOfMonadOfMonadLiftTIO {m : Type → Type u_1} [Monad m] [MonadLiftT IO m] : MonadLift BuildIO (BuildT m)

Equations

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

def Cvc.Term.BuildT.runWith' {m : Type → Type u_1} {α : Type} (build : BuildT m α) (state : Build.State) : m (Except Error α × Build.State)

Runs term-building code with a specific build state.

Equations

• build.runWith' state = build state

def Cvc.Term.BuildT.runWith {m : Type → Type u_1} [Monad m] {α : Type} (build : BuildT m α) (state : Build.State) : m (Except Error α)

Runs term-building code with a specific build state.

Equations

• build.runWith state = Prod.fst <$> build.runWith' state

def Cvc.Term.BuildT.run' {m : Type → Type u_1} [Monad m] {α : Type} [MonadLiftT BaseIO m] (build : BuildT m α) (state? : Option Build.State := none) : m (Except Error α × Build.State)

Runs term-building code, creates an initial build state if none is provided.

Equations

• build.run' (some state) = do let y ← pure state (fun (state : Cvc.Term.Build.State) => build state) y
• build.run' state? = do let y ← liftM Cvc.Term.Build.State.mk (fun (state : Cvc.Term.Build.State) => build state) y

def Cvc.Term.BuildT.run {m : Type → Type u_1} [Monad m] {α : Type} [MonadLiftT BaseIO m] (build : BuildT m α) (state? : Option Build.State := none) : m (Except Error α)

Runs term-building code, creates an initial build state if none is provided.

Equations

• build.run state? = Prod.fst <$> build.run' state?

def Cvc.Term.BuildT.runIO' {α : Type} (build : BuildIO α) (state? : Option Build.State := none) : IO (α × Build.State)

Runs term-building code in IO, creates an initial build state if none is provided

Equations

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

def Cvc.Term.BuildT.runIO {α : Type} (build : BuildIO α) (state? : Option Build.State := none) : IO α

Runs term-building code in IO, creates an initial build state if none is provided

Equations

• Cvc.Term.runIO build state? = Prod.fst <$> Cvc.Term.runIO' build state?

def Cvc.Srt.toSort (srt : Srt) : Term.Build cvc5.Sort

Conversion to unsafe sorts.

• function sorts are flattened:
  
  srt → srt' → srt'' → nonFunSrt becomes #[srt, srt', srt''] → nonFunSrt

Equations

• srt.toSort = Cvc.Term.managerDoM✝ fun (tm : cvc5.TermManager) => Cvc.Srt.toSort.aux srt tm srt 10000

@[irreducible]

def Cvc.Srt.toSort.aux (srt : Srt) (tm : cvc5.TermManager) (srt' : Srt) (maxRec : Nat) : Term.Build cvc5.Sort

Equations

• One or more equations did not get rendered due to their size.
• Cvc.Srt.toSort.aux srt tm srt' 0 = Cvc.throwInternal (toString "[Srt.toSort] maximum depth reached on `" ++ toString srt ++ toString "`")
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.bool maxRec.succ = pure tm.getBooleanSort
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.int maxRec.succ = pure tm.getIntegerSort
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.real maxRec.succ = pure tm.getRealSort
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.regex maxRec.succ = pure tm.getRegExpSort
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.string maxRec.succ = pure tm.getStringSort
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.roundingMode maxRec.succ = pure tm.getRoundingModeSort
• Cvc.Srt.toSort.aux srt tm (Cvc.Srt.finiteField size) maxRec.succ = liftM (tm.mkFiniteFieldSort size)
• Cvc.Srt.toSort.aux srt tm (Cvc.Srt.bitVec size) maxRec.succ = liftM (tm.mkBitVectorSort ↑size)
• Cvc.Srt.toSort.aux srt tm (Cvc.Srt.float exp sig) maxRec.succ = liftM (tm.mkFloatingPointSort exp sig)
• Cvc.Srt.toSort.aux srt tm (Cvc.Srt.uninterpreted name) maxRec.succ = pure (tm.mkUninterpretedSort name)
• Cvc.Srt.toSort.aux srt tm elm.bag maxRec.succ = do let __do_lift ← Cvc.Srt.toSort.aux srt tm elm maxRec liftM (tm.mkBagSort __do_lift)
• Cvc.Srt.toSort.aux srt tm elm.seq maxRec.succ = do let __do_lift ← Cvc.Srt.toSort.aux srt tm elm maxRec liftM (tm.mkSequenceSort __do_lift)
• Cvc.Srt.toSort.aux srt tm elm.set maxRec.succ = do let __do_lift ← Cvc.Srt.toSort.aux srt tm elm maxRec liftM (tm.mkSetSort __do_lift)
• Cvc.Srt.toSort.aux srt tm Cvc.Srt.unit maxRec.succ = liftM (tm.mkTupleSort #[])
• Cvc.Srt.toSort.aux srt tm (Cvc.Srt.abstract _k) maxRec.succ = Cvc.throwInternal (toString "[Srt.toSort] todo `" ++ toString (Cvc.Srt.abstract _k) ++ toString "`")

@[irreducible]

def Cvc.Srt.toSort.flattenFun (srt : Srt) (tm : cvc5.TermManager) (maxRec : Nat) (doms : Array cvc5.Sort) (cod : Srt) : Term.Build (Array cvc5.Sort × cvc5.Sort)

Equations

• Cvc.Srt.toSort.flattenFun srt tm maxRec doms (dom.function cod) = do let dom ← Cvc.Srt.toSort.aux srt tm dom maxRec Cvc.Srt.toSort.flattenFun srt tm maxRec (doms.push dom) cod
• Cvc.Srt.toSort.flattenFun srt tm maxRec doms x✝ = do let __do_lift ← Cvc.Srt.toSort.aux srt tm x✝ maxRec pure (doms, __do_lift)

Term creation API

def Cvc.Term.bool (b : Bool) : Build Term.Bool

Builds a constant Boolean term.

Equations

• Cvc.Term.bool b = Cvc.Term.managerDo✝ fun (tm : cvc5.TermManager) => { hasSymbols := false, toUnsafe := tm.mkBoolean b }

def Cvc.Term.boolVal? (t : Term.Bool) : Option Bool

Retrieves the value of a constant Boolean term.

Equations

• Cvc.Term.boolVal? t = t.toUnsafe.getBooleanValue?

def Cvc.Term.boolVal (t : Term.Bool) : Res Bool

Retrieves the value of a constant Boolean term.

Equations

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

def Cvc.Term.int (i : Int) : Build Term.Int

Builds a constant integer term.

Equations

• Cvc.Term.int i = do Cvc.Term.logicDo✝ Cvc.Logic.Builder.int Cvc.Term.managerDo✝ fun (tm : cvc5.TermManager) => { hasSymbols := false, toUnsafe := tm.mkInteger i }

def Cvc.Term.intVal? (t : Term.Int) : Option Int

Retrieves the value of a constant integer term.

Equations

• Cvc.Term.intVal? t = t.toUnsafe.getIntegerValue?

def Cvc.Term.intVal (t : Term.Int) : Res Int

Retrieves the value of a constant integer term.

Equations

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

def Cvc.Term.ratVal? (t : Term.Real) : Res (Option Rat)

Retrieves the value of a constant rational/real term.

Equations

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

def Cvc.Term.ratVal (t : Term.Real) : Res Rat

Retrieves the value of a constant rational/real term.

Equations

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

def Cvc.Term.mkNot (term : Term.Bool) : Build Term.Bool

Builds the Boolean negation of a term.

Equations

• Cvc.Term.mkNot term = Cvc.Term.mk✝ term.hasSymbols cvc5.Kind.NOT #[term.toUnsafe]

def Cvc.Term.not (term : Term.Bool) : Build Term.Bool

Builds the Boolean negation of a term.

Equations

• Cvc.Term.not = Cvc.Term.mkNot

def Cvc.Term.ite {α : Type} [IsSrt α] (cnd : Term.Bool) (thn els : Term α) : Build (Term α)

Builds an if-then-else term.

Equations

• Cvc.Term.ite cnd thn els = Cvc.Term.mk✝ (decide (cnd.hasSymbols = true ∨ thn.hasSymbols = true ∨ els.hasSymbols = true)) cvc5.Kind.ITE #[cnd.toUnsafe, thn.toUnsafe, els.toUnsafe]

n-ary operators (2 ≤ n)

def Cvc.Term.mkAnd (terms : Array (Term Bool)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a conjunction term.

Equations

• Cvc.Term.mkAnd terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.AND (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.and (lft rgt : Term Bool) : Build Formula

Builds a conjunction term.

Equations

• lft.and rgt = Cvc.Term.mkAnd #[lft, rgt] ⋯

def Cvc.Term.mkOr (terms : Array (Term Bool)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a disjunction term.

Equations

• Cvc.Term.mkOr terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.OR (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.or (lft rgt : Term Bool) : Build Formula

Builds a disjunction term.

Equations

• lft.or rgt = Cvc.Term.mkOr #[lft, rgt] ⋯

def Cvc.Term.mkXor (terms : Array (Term Bool)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds an exclusive-disjunction term.

Equations

• Cvc.Term.mkXor terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.XOR (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.xor (lft rgt : Term Bool) : Build Formula

Builds an exclusive-disjunction term.

Equations

• lft.xor rgt = Cvc.Term.mkXor #[lft, rgt] ⋯

def Cvc.Term.mkImplies (terms : Array (Term Bool)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a disjunction term.

Equations

• Cvc.Term.mkImplies terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.IMPLIES (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.implies (lft rgt : Term Bool) : Build Formula

Builds a disjunction term.

Equations

• lft.implies rgt = Cvc.Term.mkImplies #[lft, rgt] ⋯

def Cvc.Term.mkEqual {α : Type} (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds an equality term.

Equations

• Cvc.Term.mkEqual terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.EQUAL (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.equal {α : Type} (lft rgt : Term α) : Build Formula

Builds an equality term.

Equations

• lft.equal rgt = Cvc.Term.mkEqual #[lft, rgt] ⋯

def Cvc.Term.mkDistinct {α : Type} (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a pairwise-distinct term.

Equations

• Cvc.Term.mkDistinct terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.DISTINCT (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.distinct {α : Type} (lft rgt : Term α) : Build Formula

Builds a pairwise-distinct term.

Equations

• lft.distinct rgt = Cvc.Term.mkDistinct #[lft, rgt] ⋯

@[reducible, inline]

abbrev Cvc.Term.mkNEqual {α : Type} (lft rgt : Term α) : Build Formula

Builds a pairwise-distinct term.

Equations

• @Cvc.Term.mkNEqual = @Cvc.Term.distinct

@[reducible, inline]

abbrev Cvc.Term.nequal {α : Type} (lft rgt : Term α) : Build Formula

Builds a pairwise-distinct term.

Equations

• @Cvc.Term.nequal = @Cvc.Term.distinct

def Cvc.Term.mkLt {α : Type} (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a less-than term.

Equations

• Cvc.Term.mkLt terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.LT (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.lt {α : Type} (lft rgt : Term α) : Build Formula

Builds a less-than term.

Equations

• lft.lt rgt = Cvc.Term.mkLt #[lft, rgt] ⋯

def Cvc.Term.mkLe {α : Type} (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a less-than-or-equal-to term.

Equations

• Cvc.Term.mkLe terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.LEQ (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.le {α : Type} (lft rgt : Term α) : Build Formula

Builds a less-than-or-equal-to term.

Equations

• lft.le rgt = Cvc.Term.mkLe #[lft, rgt] ⋯

def Cvc.Term.mkGe {α : Type} (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a greater-than-or-equal-to term.

Equations

• Cvc.Term.mkGe terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.GEQ (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.ge {α : Type} (lft rgt : Term α) : Build Formula

Builds a greater-than-or-equal-to term.

Equations

• lft.ge rgt = Cvc.Term.mkGe #[lft, rgt] ⋯

def Cvc.Term.mkGt {α : Type} (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") : Build Formula

Builds a greater-than term.

Equations

• Cvc.Term.mkGt terms h_size = Cvc.Term.mk✝ (terms.any Cvc.Term.hasSymbols) cvc5.Kind.GT (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.gt {α : Type} (lft rgt : Term α) : Build Formula

Builds a greater-than term.

Equations

• lft.gt rgt = Cvc.Term.mkGt #[lft, rgt] ⋯

Arithmetic

def Cvc.Term.mkAdd {α : Type} [IsSrt α] (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Builds an addition term.

• Forbids difference logics.

Equations

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

def Cvc.Term.add {α : Type} [IsSrt α] (lft rgt : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Builds an addition term.

• Forbids difference logics.

Equations

• lft.add rgt Arith = Cvc.Term.mkAdd #[lft, rgt] ⋯ inferInstance

def Cvc.Term.mkSub {α : Type} [IsSrt α] (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Builds a subtraction term.

Equations

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

def Cvc.Term.sub {α : Type} [IsSrt α] (lft rgt : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Builds a subtraction term.

Equations

• lft.sub rgt Arith = Cvc.Term.mkSub #[lft, rgt] ⋯ inferInstance

def Cvc.Term.neg {α : Type} [IsSrt α] (term : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Equations

• term.neg Arith = Cvc.Term.mk✝ term.hasSymbols cvc5.Kind.NEG #[term.toUnsafe]

def Cvc.Term.mkMul {α : Type} [IsSrt α] (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Builds a multiplication term.

• Forbids difference logic.
• Forces non-linear logic if non-linear.

Equations

• Cvc.Term.mkMul terms h_size Arith = do Cvc.Term.nonDiff✝ let hasSymbols ← Cvc.Term.checkNonLinearOfArgs✝ terms Cvc.Term.mk✝ hasSymbols cvc5.Kind.MULT (Array.map Cvc.Term.toUnsafe terms)

def Cvc.Term.mul {α : Type} [IsSrt α] (lft rgt : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Builds a multiplication term.

• Forbids difference logic.
• Forces non-linear logic if non-linear.

Equations

• lft.mul rgt Arith = Cvc.Term.mkMul #[lft, rgt] ⋯ inferInstance

def Cvc.Term.mkDiv! {α : Type} [IsSrt α] (terms : Array (Term α)) (h_size : 2 ≤ terms.size := by (try (try simp <;> try omega); done) <;> fail "expected an array of **at least** two terms") (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Arithmetic division with division by 0 undefined, left associative.

• Forbids difference logic.
• Forces non-linear logic if non-linear.

Equations

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

def Cvc.Term.div! {α : Type} [IsSrt α] (lft rgt : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Arithmetic division with division by 0 undefined, left associative.

• Forbids difference logic.
• Forces non-linear logic if non-linear.

Equations

• lft.div! rgt Arith = Cvc.Term.mkDiv! #[lft, rgt] ⋯ inferInstance

def Cvc.Term.mkDivTotal {α : Type} [IsSrt α] (lft rgt : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Arithmetic division with division by 0 defined to be 0, left associative.

Equations

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

def Cvc.Term.divTotal {α : Type} [IsSrt α] (lft rgt : Term α) (Arith : IsSrt.Arith α := by (try (exact inferInstance); done) <;> fail "expected arithmetic type `Int` or `Rat`, see `Cvc.is_arith` and `Cvc.IsSrt.Arith`") : Build (Term α)

Arithmetic division with division by 0 defined to be 0, left associative.

Equations

• lft.divTotal rgt Arith = lft.mkDivTotal rgt inferInstance

Function application

def Cvc.Term.apply {β α : Type} [IsSrt β] (function : Term (α → β)) (arg : Term α) : Build (Term β)

Applies a function term to an argument.

Partial applications and higher-order

This function supports partial applications: they are encoded as cvc5.Kind.HO_APPLY terms, which would trigger errors if used in a solver without support for higher-order. Since support for higher-order makes cvc5-level reasoning much more expensive, we want to avoid having HO_APPLY terms as much as possible.

For this reason, this function detects when it is building an application that yields a non-function term; in this case, it will destruct the underlying higher-order terms (recursively, and if any) and rewrite them as a regular (first-order) function application.

Equations

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

structure Cvc.Value (α : Type) : Type

A term-value, as produced by getValue-like (SMT) function.

• ofTerm :: (
• toTerm : Term α

  Underlying term.

• )

def Cvc.Value.toString {α : Type} (value : Value α) : String

Equations

• value.toString = toString value.toTerm

instance Cvc.Value.instToString {α : Type} : ToString (Value α)

Equations

• Cvc.Value.instToString = { toString := Cvc.Value.toString }

@[reducible, inline]

abbrev Cvc.Value.Bool : Type

Boolean values.

Equations

• Cvc.Value.Bool = Cvc.Value Bool

@[reducible, inline]

abbrev Cvc.Value.Int : Type

Integer values.

Equations

• Cvc.Value.Int = Cvc.Value Int

@[reducible, inline]

abbrev Cvc.Value.Real : Type

Real/Rat values.

Equations

• Cvc.Value.Real = Cvc.Value Rat

@[reducible, inline]

abbrev Cvc.Value.String : Type

String values.

Equations

• Cvc.Value.String = Cvc.Value String

@[reducible, inline]

abbrev Cvc.Value.Array (α β : Type) : Type

Array values.

Equations

• Cvc.Value.Array α β = Cvc.Value (Cvc.TMap α β)

@[reducible, inline]

abbrev Cvc.Value.Seq (α : Type) : Type

Sequence values.

Equations

• Cvc.Value.Seq α = Cvc.Value (Array α)

@[reducible, inline]

abbrev Cvc.Value.Fun (α β : Type) : Type

Function values.

Equations

• Cvc.Value.Fun α β = Cvc.Value (α → β)

@[reducible, inline]

abbrev Cvc.Value.Prod (α β : Type) : Type

Product values.

Equations

• Cvc.Value.Prod α β = Cvc.Value (α × β)

@[reducible, inline]

abbrev Cvc.Value.srt {α : Type} [A : IsSrt α] (value : Value α) : Srt

Equations

• Cvc.Value.srt = Cvc.𝕂 (Cvc.IsSrt.srt α)

theorem Cvc.Value.srt_bij {α : Type} [A : IsSrt α] (value : Value α) : α = value.srt.toType

def Cvc.Value.retype {α : Type} [A : IsSrt α] (value : Value α) : Value value.srt.toType

Equations

• value.retype = ⋯ ▸ value

def Cvc.Value.inspectSrt {α : Type} [A : IsSrt α] (value : Value α) {β : Sort u_1} (f : (srt : Srt) → Value srt.toType → β) : β

Equations

• value.inspectSrt f = f value.srt value.retype

def Cvc.Value.boolVal (value : Value.Bool) : Res Bool

Equations

• Cvc.Value.boolVal value = value.toTerm.boolVal

def Cvc.Value.intVal (value : Value.Int) : Res Int

Equations

• Cvc.Value.intVal value = value.toTerm.intVal

def Cvc.Value.ratVal (value : Value.Real) : Res Rat

Equations

• Cvc.Value.ratVal value = value.toTerm.ratVal

class Cvc.Conv.ValueToVal (m : Type → Type) (α : Type) extends Cvc.IsSrt α : Type 1

• mk' :: (
• srt : Srt
• h_bij : α = (srt α).toType
• Val : Type
• ofValue : Value α → m (Val m α)
• )

@[reducible, inline]

abbrev Cvc.Conv.ValueToVal.Id (α : Type) [IsSrt α] : ValueToVal Id α

Equations

• Cvc.Conv.ValueToVal.Id α = { toIsSrt := inst✝, Val := Cvc.Value α, ofValue := id }

def Cvc.Conv.ValueToVal.mk {α : Type} {m : Type → Type} [IsSrt α] (Val : Type) (ofValue : Value α → m Val) : ValueToVal m α

Equations

• Cvc.Conv.ValueToVal.mk Val ofValue = { toIsSrt := inst✝, Val := Val, ofValue := ofValue }

def Cvc.Conv.ValueToVal.mkId {α : Type} [IsSrt α] : ValueToVal Id α

Equations

• Cvc.Conv.ValueToVal.mkId = { toIsSrt := inst✝, Val := Cvc.Value α, ofValue := id }

instance Cvc.Conv.ValueToVal.instCoeSortType {m : Type → Type} {α : Type} : CoeSort (ValueToVal m α) Type

Equations

• Cvc.Conv.ValueToVal.instCoeSortType = { coe := fun (conv : Cvc.Conv.ValueToVal m α) => Cvc.Conv.ValueToVal.Val m α }

@[reducible, inline]

abbrev Cvc.Conv.ValueToVal.adaptM {m : Type → Type} {α : Type} {m' : Type → Type} [A : ValueToVal m α] (lift : {β : Type} → m β → m' β) : ValueToVal m' α

Equations

• Cvc.Conv.ValueToVal.adaptM lift = { toIsSrt := A.toIsSrt m, Val := Cvc.Conv.ValueToVal.Val m α, ofValue := lift ∘ Cvc.Conv.ValueToVal.ofValue }

@[reducible, inline]

abbrev Cvc.Conv.ValueToVal.liftM {m m' : Type → Type} {α : Type} [MonadLiftT m m'] [A : ValueToVal m α] : ValueToVal m' α

Equations

• Cvc.Conv.ValueToVal.liftM = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => liftM

instance Cvc.Conv.ValueToVal.defaultInstUnit : ValueToVal Id Unit

Equations

• Cvc.Conv.ValueToVal.defaultInstUnit = Cvc.Conv.ValueToVal.mk Unit fun (x : Cvc.Value Unit) => pure ()

instance Cvc.Conv.ValueToVal.defaultInstBool : ValueToVal Res Bool

Equations

• Cvc.Conv.ValueToVal.defaultInstBool = Cvc.Conv.ValueToVal.mk Bool fun (v : Cvc.Value Bool) => v.boolVal

instance Cvc.Conv.ValueToVal.instToStringValResBool : ToString (Val Res Bool)

Equations

• Cvc.Conv.ValueToVal.instToStringValResBool = inferInstanceAs (ToString Bool)

instance Cvc.Conv.ValueToVal.defaultInstInt : ValueToVal Res Int

Equations

• Cvc.Conv.ValueToVal.defaultInstInt = Cvc.Conv.ValueToVal.mk Int fun (v : Cvc.Value Int) => v.intVal

instance Cvc.Conv.ValueToVal.instToStringValResInt : ToString (Val Res Int)

Equations

• Cvc.Conv.ValueToVal.instToStringValResInt = inferInstanceAs (ToString Int)

instance Cvc.Conv.ValueToVal.defaultInstRat : ValueToVal Res Rat

Equations

• Cvc.Conv.ValueToVal.defaultInstRat = Cvc.Conv.ValueToVal.mk Rat fun (t : Cvc.Value Rat) => t.ratVal

instance Cvc.Conv.ValueToVal.instToStringValResRat : ToString (Val Res Rat)

Equations

• Cvc.Conv.ValueToVal.instToStringValResRat = inferInstanceAs (ToString Rat)

instance Cvc.Conv.ValueToVal.defaultInstString : ValueToVal Id String

Equations

• Cvc.Conv.ValueToVal.defaultInstString = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstRoundingMode : ValueToVal Id RoundingMode

Equations

• Cvc.Conv.ValueToVal.defaultInstRoundingMode = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstRegex : ValueToVal Id Cvc.Regex

Equations

• Cvc.Conv.ValueToVal.defaultInstRegex = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstFloat {exp sig : UInt32} : ValueToVal Id (Cvc.AnyFloat exp sig)

Equations

• Cvc.Conv.ValueToVal.defaultInstFloat = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstAbstract {k : Srt.Kind} : ValueToVal Id (Cvc.Abstract k)

Equations

• Cvc.Conv.ValueToVal.defaultInstAbstract = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstFiniteField {n : Nat} : ValueToVal Id (FiniteField n)

Equations

• Cvc.Conv.ValueToVal.defaultInstFiniteField = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstBitVec {size : Nat} : ValueToVal Id (BitVec size)

Equations

• Cvc.Conv.ValueToVal.defaultInstBitVec = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstUninterpreted {name : String} : ValueToVal Id (Uninterpreted name)

Equations

• Cvc.Conv.ValueToVal.defaultInstUninterpreted = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstArray {α : Type} [IsSrt α] : ValueToVal Id (Array α)

Equations

• Cvc.Conv.ValueToVal.defaultInstArray = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstProd {α β : Type} [IsSrt α] [IsSrt β] : ValueToVal Id (α × β)

Equations

• Cvc.Conv.ValueToVal.defaultInstProd = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstFun {α β : Type} [IsSrt α] [IsSrt β] : ValueToVal Id (α → β)

Equations

• Cvc.Conv.ValueToVal.defaultInstFun = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstTMap {α β : Type} [IsSrt α] [IsSrt β] : ValueToVal Id (Cvc.TMap α β)

Equations

• Cvc.Conv.ValueToVal.defaultInstTMap = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstBag {α : Type} [IsSrt α] : ValueToVal Id (Cvc.Bag α)

Equations

• Cvc.Conv.ValueToVal.defaultInstBag = Cvc.Conv.ValueToVal.mkId

instance Cvc.Conv.ValueToVal.defaultInstSet {α : Type} [IsSrt α] : ValueToVal Id (Cvc.Set α)

Equations

• Cvc.Conv.ValueToVal.defaultInstSet = Cvc.Conv.ValueToVal.mkId

@[reducible, inline]

abbrev Cvc.Conv.ValueToVal.defaultFor (srt : Srt) : ValueToVal Res srt.toType

Equations

• Cvc.Conv.ValueToVal.defaultFor (Cvc.Srt.abstract _kind) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor (_idx.array _elm) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor _elm.bag = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.bool = Cvc.Conv.ValueToVal.defaultInstBool
• Cvc.Conv.ValueToVal.defaultFor (Cvc.Srt.bitVec _n) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor (Cvc.Srt.finiteField _n) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor (Cvc.Srt.float _exp _sig) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor (_dom.function _cod) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.int = Cvc.Conv.ValueToVal.defaultInstInt
• Cvc.Conv.ValueToVal.defaultFor (_lft.prod _rgt) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.real = Cvc.Conv.ValueToVal.defaultInstRat
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.regex = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.roundingMode = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor _elm.seq = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor _elm.set = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.string = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor Cvc.Srt.unit = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok
• Cvc.Conv.ValueToVal.defaultFor (Cvc.Srt.uninterpreted name) = Cvc.Conv.ValueToVal.adaptM fun {β : Type} => Cvc.Res.ok

def Cvc.Conv.ValueToVal.Default.instResToType (srt : Srt) : ValueToVal Res srt.toType

Equations

• Cvc.Conv.ValueToVal.Default.instResToType srt = Cvc.Conv.ValueToVal.defaultFor srt

class Cvc.Conv.ValuesToVal (m : Type → Type) : Type 1

• instValueToVal (srt : Srt) : ValueToVal m srt.toType

@[reducible, inline]

abbrev Cvc.Conv.ValuesToVal.Values : ValuesToVal Id

Equations

• Cvc.Conv.ValuesToVal.Values = { instValueToVal := fun (x : Cvc.Srt) => Cvc.Conv.ValueToVal.Id x.toType }

@[reducible, inline]

abbrev Cvc.Conv.ValuesToVal.Default : ValuesToVal Res

Equations

• Cvc.Conv.ValuesToVal.Default = { instValueToVal := Cvc.Conv.ValueToVal.defaultFor }

Conversion of term-values

class Cvc.Srt.ToValType : Type 1

• Val : Srt → Type

def Cvc.Srt.ToValType.Terms : ToValType

Equations

• Cvc.Srt.ToValType.Terms = { Val := fun (srt : Cvc.Srt) => Cvc.Term srt.toType }

class Cvc.Term.ToValsextends Cvc.Srt.ToValType : Type 1

• Val : Srt → Type
• build (srt : Srt) : Term srt.toType → Srt.ToValType.Val srt

def Cvc.Term.ToVals.Terms : ToVals

Equations

• Cvc.Term.ToVals.Terms = { toValConv := Cvc.Srt.ToValType.Terms, build := fun (x : Cvc.Srt) => id }

Smt environment and functions

structure Cvc.Smt.State : Type

• solver : cvc5.Solver
• builder : Term.Build.State
• nextActlitIdx' : Nat

@[reducible, inline]

abbrev Cvc.SmtT (m : Type → Type) (α : Type) : Type

Equations

• Cvc.SmtT m = Cvc.ResT (StateT Cvc.Smt.State m)

@[reducible, inline]

abbrev Cvc.SmtIO (α : Type) : Type

Equations

• Cvc.SmtIO = Cvc.SmtT IO

@[reducible, inline]

abbrev Cvc.Smt (α : Type) : Type

Equations

• Cvc.Smt = Cvc.SmtT Id

instance Cvc.Smt.instMonadLiftResIOSmtIO : MonadLift ResIO SmtIO

Equations

• Cvc.Smt.instMonadLiftResIOSmtIO = { monadLift := fun {α : Type} (code : Cvc.ResIO α) (state : Cvc.Smt.State) => do let __do_lift ← code pure (__do_lift, state) }

instance Cvc.Smt.instMonadLiftSmtT {m : Type → Type} [Monad m] : MonadLift m (SmtT m)

Equations

• Cvc.Smt.instMonadLiftSmtT = { monadLift := fun {α : Type} (code : m α) (state : Cvc.Smt.State) => do let __do_lift ← code pure (Except.ok __do_lift, state) }

instance Cvc.Smt.instMonadLiftSmtTOfMonad {m m' : Type → Type} [Monad m] [Monad m'] [MonadLift m m'] : MonadLift (SmtT m) (SmtT m')

Equations

• Cvc.Smt.instMonadLiftSmtTOfMonad = { monadLift := fun {α : Type} (code : Cvc.SmtT m α) (state : Cvc.Smt.State) => do let __do_lift ← liftM (code state) pure __do_lift }

instance Cvc.Smt.instMonadLiftSmtTOfMonad_1 {m : Type → Type} [Monad m] : MonadLift Smt (SmtT m)

Equations

• Cvc.Smt.instMonadLiftSmtTOfMonad_1 = { monadLift := fun {α : Type} (code : Cvc.Smt α) (state : Cvc.Smt.State) => pure (code state) }

instance Cvc.Smt.instMonadLiftSmtIOSmtTOfMonadOfMonadLiftTIO {m : Type → Type} [Monad m] [MonadLiftT IO m] : MonadLift SmtIO (SmtT m)

Equations

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

instance Cvc.Smt.instMonadLiftBuildSmtTOfMonad {m : Type → Type} [Monad m] : MonadLift Term.Build (SmtT m)

Equations

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

def Cvc.Smt.nextActlitIdx : Smt Nat

Equations

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

def Cvc.Smt.setOption (opt : Cvc.Option) : Smt Unit

Sets an option in the solver.

Equations

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

def Cvc.Smt.declare (symbol : String) (α : Type) [IsSrt α] : Smt (Term α)

Declares a function symbol.

Equations

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

def Cvc.Smt.declare' {α : Type} [IsSrt α] (symbol : String) : Smt (Term α)

Declares a function symbol.

Equations

• Cvc.Smt.declare' symbol = Cvc.Smt.declare symbol α

def Cvc.Smt.assert (formula : Formula) : Smt Unit

Asserts a formula.

Equations

• Cvc.Smt.assert formula = Cvc.Smt.lift5✝ (cvc5.Solver.assertFormula formula.toUnsafe)

def Cvc.Smt.checkSat (assuming : Option (Array Formula) := none) : Smt CheckSat

Checks the satisfiability of the formulas asserted with Smt.assert.

Equations

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

def Cvc.Smt.checkSat? (assuming : Option (Array Formula) := none) : Smt (Option Bool)

Simplified Smt.checkSat, returns true/false for sat/unsat, none for unknown/unexpected.

Equations

• Cvc.Smt.checkSat? assuming = Cvc.CheckSat.isSat? <$> Cvc.Smt.checkSat assuming

structure Cvc.Smt.Sat.Stateextends Cvc.Smt.State : Type

Sat-mode state.

• solver : cvc5.Solver
• builder : Term.Build.State
• nextActlitIdx' : Nat

structure Cvc.Smt.Unsat.Stateextends Cvc.Smt.State : Type

Unsat-mode state.

• solver : cvc5.Solver
• builder : Term.Build.State
• nextActlitIdx' : Nat

structure Cvc.Smt.Unknown.Stateextends Cvc.Smt.State : Type

Unknown-mode state.

• solver : cvc5.Solver
• builder : Term.Build.State
• nextActlitIdx' : Nat

@[reducible, inline]

abbrev Cvc.Smt.SatT (m : Type → Type u) (α : Type) : Type u

Sat-mode monad, allows running commands such as get-value.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

Equations

• Cvc.Smt.SatT m = Cvc.ResT (StateT Cvc.Smt.Sat.State m)

@[reducible, inline]

abbrev Cvc.Smt.Sat (α : Type) : Type

Sat-mode monad, allows running commands such as get-value.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

Equations

• Cvc.Smt.Sat = Cvc.Smt.SatT Id

def Cvc.Smt.Sat.unexpected {m : Type → Type u_1} [Monad m] {α : Type} : SatT m α

Equations

• Cvc.Smt.Sat.unexpected = Cvc.throwUser "unexpected sat result"

@[reducible, inline]

abbrev Cvc.Smt.UnsatT (m : Type → Type u) (α : Type) : Type u

Unsat-mode monad, allows running commands such as get-proof.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

Equations

• Cvc.Smt.UnsatT m = Cvc.ResT (StateT Cvc.Smt.Unsat.State m)

@[reducible, inline]

abbrev Cvc.Smt.Unsat (α : Type) : Type

Unsat-mode monad, allows running commands such as get-proof.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

Equations

• Cvc.Smt.Unsat = Cvc.Smt.UnsatT Id

def Cvc.Smt.Unsat.unexpected {m : Type → Type u_1} [Monad m] {α : Type} : UnsatT m α

Equations

• Cvc.Smt.Unsat.unexpected = Cvc.throwUser "unexpected unsat result"

@[reducible, inline]

abbrev Cvc.Smt.UnknownT (m : Type → Type u) (α : Type) : Type u

Unknown-mode monad, allows running unknown-mode-specific commands.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

Equations

• Cvc.Smt.UnknownT m = Cvc.ResT (StateT Cvc.Smt.Unknown.State m)

@[reducible, inline]

abbrev Cvc.Smt.Unknown (α : Type) : Type

Unknown-mode monad, allows running unknown-mode-specific commands.

Smt does not lift to this monad as this would allow issuing a check-sat that could switch to a different solver mode.

Equations

• Cvc.Smt.Unknown = Cvc.Smt.UnknownT Id

def Cvc.Smt.Unknown.unexpected {m : Type → Type u_1} [Monad m] {α : Type} : UnknownT m α

Equations

• Cvc.Smt.Unknown.unexpected = Cvc.throwUser "unexpected unknown result"

def Cvc.Smt.checkSatAnd {m : Type → Type} [Monad m] {α : Type} (assuming : Option (Array Formula) := none) (ifSat : SatT m α := Sat.unexpected) (ifUnsat : UnsatT m α := Unsat.unexpected) (ifUnknown : UnknownT m α := Unknown.unexpected) : SmtT m α

Performs a check-sat and runs sat/unsat/unknown-specific code.

Equations

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

instance Cvc.Smt.Sat.instMonadLiftSatTOfMonad {m : Type → Type u_1} [Monad m] : MonadLift Sat (SatT m)

Equations

• Cvc.Smt.Sat.instMonadLiftSatTOfMonad = { monadLift := fun {α : Type} (code : Cvc.Smt.Sat α) (state : Cvc.Smt.Sat.State) => pure (code state) }

instance Cvc.Smt.Sat.instMonadLiftBuildSatTOfMonad {m : Type → Type u_1} [Monad m] [Monad m] : MonadLift Term.Build (SatT m)

Equations

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

def Cvc.Smt.Sat.getValue {α : Type} (term : Term α) : Sat (Value α)

Retrieves the value of a term in Sat mode.

This function is available the following namespaces: Cvc.Term, Cvc.Smt, and Cvc.Smt.Sat.

Equations

• Cvc.Smt.getValue term = do let term! ← Cvc.Smt.Sat.lift5✝ (cvc5.Solver.getValue term.toUnsafe) pure { toTerm := { hasSymbols := false, toUnsafe := term! } }

def Cvc.Smt.Sat.getValues {α : Type} (terms : Array (Term α)) : Sat (Array (Term α × Value α))

Retrieves the values of some terms of the same sort in Sat mode.

This function is available the following namespaces: Cvc.Term, Cvc.Smt, and Cvc.Smt.Sat.

Equations

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

def Cvc.Smt.Sat.getValUsing {m : Type → Type} {α : Type} [Monad m] [MonadLiftT m Sat] (Val : Conv.ValueToVal m α) (term : Term α) : Sat (Conv.ValueToVal.Val m α)

Retrieves the concrete Value of a term in Sat mode.

Equations

• Cvc.Smt.getValUsing Val term = Cvc.Smt.getValue term >>= liftM ∘ Cvc.Conv.ValueToVal.ofValue

def Cvc.Smt.Sat.getVal {m : Type → Type} {α : Type} [Monad m] [MonadLiftT m Sat] [Val : Conv.ValueToVal m α] (term : Term α) : Sat (Conv.ValueToVal.Val m α)

Retrieves the concrete Value of a term in Sat mode.

Equations

• Cvc.Smt.getVal term = Cvc.Smt.getValUsing Val term

def Cvc.Smt.Sat.getValsUsing {α : Type} (Val : Conv.ValueToVal Sat α) (terms : Array (Term α)) : Sat (Array (Term α × Conv.ValueToVal.Val Sat α))

Retrieves the concrete values of some terms of the same sort in Sat mode.

Equations

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

def Cvc.Smt.Sat.getVals {α : Type} [Val : Conv.ValueToVal Sat α] (terms : Array (Term α)) : Sat (Array (Term α × Conv.ValueToVal.Val Sat α))

Retrieves the concrete values of some terms of the same sort in Sat mode.

Equations

• Cvc.Smt.getVals terms = Cvc.Smt.getValsUsing Val terms

instance Cvc.Smt.Unsat.instMonadLiftUnsatTOfMonad {m : Type → Type u_1} [Monad m] : MonadLift Unsat (UnsatT m)

Equations

• Cvc.Smt.Unsat.instMonadLiftUnsatTOfMonad = { monadLift := fun {α : Type} (code : Cvc.Smt.Unsat α) (state : Cvc.Smt.Unsat.State) => pure (code state) }

instance Cvc.Smt.Unsat.instMonadLiftBuildUnsatTOfMonad {m : Type → Type u_1} [Monad m] [Monad m] : MonadLift Term.Build (UnsatT m)

Equations

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

def Cvc.Smt.Unsat.getProof : Unsat (Array cvc5.Proof)

Retrieves the unsat-proofs in Unsat mode.

Equations

• Cvc.Smt.getProof = Cvc.Smt.Unsat.lift5✝ cvc5.Solver.getProof

instance Cvc.Smt.Unknown.instMonadLiftUnknownTOfMonad {m : Type → Type u_1} [Monad m] : MonadLift Unknown (UnknownT m)

Equations

• Cvc.Smt.Unknown.instMonadLiftUnknownTOfMonad = { monadLift := fun {α : Type} (code : Cvc.Smt.Unknown α) (state : Cvc.Smt.Unknown.State) => pure (code state) }

instance Cvc.Smt.Unknown.instMonadLiftBuildUnknownTOfMonad {m : Type → Type u_1} [Monad m] [Monad m] : MonadLift Term.Build (UnknownT m)

Equations

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

def Cvc.Term.getSymbol? {α : Type} (term : Term α) : Option String

Returns the symbol of a symbol-term.

Equations

• term.getSymbol? = term.toUnsafe.getSymbol?

def Cvc.SmtT.runWith' {m : Type → Type} {α : Type} (smt : SmtT m α) (state : Smt.State) : m (Except Error α × Smt.State)

Equations

• smt.runWith' state = smt state

def Cvc.SmtT.runWith {m : Type → Type} [M : Monad m] {α : Type} (smt : SmtT m α) (state : Smt.State) : m (Except Error α)

Equations

• smt.runWith state = Prod.fst <$> smt.runWith' state

def Cvc.SmtT.run' {m : Type → Type} [M : Monad m] {α : Type} [MonadLiftT BaseIO m] (smt : SmtT m α) (state? : Option Smt.State := none) : m (Except Error (α × Smt.State))

Equations

• One or more equations did not get rendered due to their size.
• smt.run' (some state) = do let __discr ← smt.runWith' state match __discr with | (res, state) => pure (Except.map (fun (x : α) => (x, state)) res)

@[reducible, inline]

abbrev Cvc.SmtT.run {m : Type → Type} [M : Monad m] {α : Type} [MonadLiftT BaseIO m] (smt : SmtT m α) (state? : Option Smt.State := none) : m (Except Error α)

Equations

• smt.run state? = Except.map Prod.fst <$> smt.run' state?

def Cvc.SmtT.runIO' {α : Type} (smt : SmtIO α) (state? : Option Smt.State := none) : IO (α × Smt.State)

Equations

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

def Cvc.SmtT.runIO {α : Type} (smt : SmtIO α) (state? : Option Smt.State := none) : IO α

Equations

• Cvc.SmtT.runIO smt state? = Prod.fst <$> Cvc.SmtT.runIO' smt state?

def Cvc.SmtT.runWithBuilder' {m : Type → Type} [M : Monad m] {α : Type} (smt : SmtT m α) (builder : Term.Build.State) : m (Except Error (α × Smt.State))

Equations

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

def Cvc.SmtT.runWithBuilder {m : Type → Type} [M : Monad m] {α : Type} (smt : SmtT m α) (builder : Term.Build.State) : m (Except Error α)

Equations

• smt.runWithBuilder builder = Except.map Prod.fst <$> smt.runWithBuilder' builder