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.beqSolverName✝ }

instance Auto.Solver.SMT.instHashableSolverName : Hashable SolverName

Equations

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

instance Auto.Solver.SMT.instInhabitedSolverName : Inhabited SolverName

Equations

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

instance Auto.Solver.SMT.instReprSolverName : Repr SolverName

Equations

• Auto.Solver.SMT.instReprSolverName = { reprPrec := Auto.Solver.SMT.reprSolverName✝ }

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.