opaque auto.smt : Lean.Option Bool

opaque auto.smt.trust : Lean.Option Bool

axiom autoSMTSorry (α : Sort u) : α

opaque auto.smt.timeout : Lean.Option Nat

def auto.smt.save.doc : String

Equations

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

opaque auto.smt.save : Lean.Option Bool

opaque auto.smt.savepath : Lean.Option String

opaque auto.smt.rconsProof : Lean.Option Bool

opaque auto.smt.dumpHints : Lean.Option Bool

opaque auto.smt.sygus_inst : Lean.Option Bool

opaque auto.smt.dumpHints.limitedRws : Lean.Option Bool

inductive Auto.Solver.SMT.SolverName : Type

• none : SolverName
• z3 : SolverName
• cvc4 : SolverName
• cvc5 : SolverName

instance Auto.Solver.SMT.instBEqSolverName : BEq SolverName

Equations

• Auto.Solver.SMT.instBEqSolverName = { beq := Auto.Solver.SMT.instBEqSolverName.beq }

def Auto.Solver.SMT.instBEqSolverName.beq : SolverName → SolverName → Bool

Equations

• Auto.Solver.SMT.instBEqSolverName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Auto.Solver.SMT.instHashableSolverName : Hashable SolverName

Equations

• Auto.Solver.SMT.instHashableSolverName = { hash := Auto.Solver.SMT.instHashableSolverName.hash }

def Auto.Solver.SMT.instHashableSolverName.hash : SolverName → UInt64

Equations

• Auto.Solver.SMT.instHashableSolverName.hash Auto.Solver.SMT.SolverName.none = 0
• Auto.Solver.SMT.instHashableSolverName.hash Auto.Solver.SMT.SolverName.z3 = 1
• Auto.Solver.SMT.instHashableSolverName.hash Auto.Solver.SMT.SolverName.cvc4 = 2
• Auto.Solver.SMT.instHashableSolverName.hash Auto.Solver.SMT.SolverName.cvc5 = 3

def Auto.Solver.SMT.instInhabitedSolverName.default : SolverName

Equations

• Auto.Solver.SMT.instInhabitedSolverName.default = Auto.Solver.SMT.SolverName.none

instance Auto.Solver.SMT.instInhabitedSolverName : Inhabited SolverName

Equations

• Auto.Solver.SMT.instInhabitedSolverName = { default := Auto.Solver.SMT.instInhabitedSolverName.default }

instance Auto.Solver.SMT.instReprSolverName : Repr SolverName

Equations

• Auto.Solver.SMT.instReprSolverName = { reprPrec := Auto.Solver.SMT.instReprSolverName.repr }

def Auto.Solver.SMT.instReprSolverName.repr : SolverName → Nat → Std.Format

Equations

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

instance Auto.Solver.SMT.instToStringSolverName : ToString SolverName

Equations

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

instance Auto.Solver.SMT.instValueSolverName : Lean.KVMap.Value SolverName

Equations

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

opaque auto.smt.solver.name : Lean.Option Auto.Solver.SMT.SolverName

@[reducible, inline]

abbrev Auto.Solver.SMT.SolverProc : Type

Equations

• Auto.Solver.SMT.SolverProc = IO.Process.Child { stdin := IO.Process.Stdio.piped, stdout := IO.Process.Stdio.piped, stderr := IO.Process.Stdio.piped }

def Auto.Solver.SMT.createSolver (name : SolverName) : Lean.MetaM SolverProc

Equations

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

def Auto.Solver.SMT.createSolver.createAux (path : String) (args : Array String) : Lean.MetaM SolverProc

Equations

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

axiom Auto.Solver.SMT.autoSMTSorry (α : Sort u) : α

def Auto.Solver.SMT.getTerm (s : String) : Lean.MetaM (Parser.SMTTerm.Term × String)

Equations

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

def Auto.Solver.SMT.validFactOfUnsatCore (unsatCore : Parser.SMTTerm.Term) : Lean.MetaM (Array Nat)

Recover id of valid facts from unsat core. Refer to lamFOL2SMT

Equations

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

def Auto.Solver.SMT.querySolver (query : Array IR.SMT.Command) : Lean.MetaM (Option (Parser.SMTTerm.Term × String))

Only put declarations in the query

Equations

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

@[reducible, inline]

abbrev Auto.Solver.SMT.solverHints : Type

solverHints includes:

• preprocessFacts : List (Parser.SMTTerm.Term)
• theoryLemmas : List (Parser.SMTTerm.Term)
• instantiations : List (Parser.SMTTerm.Term)
• computationLemmas : List (Parser.SMTTerm.Term)
• polynomialLemmas : List (Parser.SMTTerm.Term)
• rewriteFacts : List (List (Parser.SMTTerm.Term))

Equations

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

def Auto.Solver.SMT.querySolverWithHints (query : Array IR.SMT.Command) : Lean.MetaM (Option (Parser.SMTTerm.Term × solverHints × String))

Behaves like querySolver but assumes that the output came from cvc5 with --dump-hints enabled. The additional output is used to return not just the unsatCore and proof, but also a list of theory lemmas.

Equations

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

def Auto.Solver.SMT.saveQuery (query : Array IR.SMT.Command) : Lean.MetaM Unit

Equations

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