This module implements the logic to call CaDiCal (or CLI interface compatible SAT solvers) and extract an LRAT UNSAT proof or a model from its output.

inductive Lean.Meta.Tactic.BVDecide.External.SolverResult : Type

The result of calling a SAT solver.

• sat (assignment : Array (Bool × Nat)) : SolverResult

  The solver returned SAT with some literal assignment.

• unsat : SolverResult

  The solver returned UNSAT.

inductive Lean.Meta.Tactic.BVDecide.External.TimedOut (α : Type u) : Type u

• success {α : Type u} (x : α) : TimedOut α
• timeout {α : Type u} : TimedOut α

def Lean.Meta.Tactic.BVDecide.External.runInterruptible (timeout : Nat) (args : IO.Process.SpawnArgs) : CoreM (TimedOut IO.Process.Output)

Run a process with args until it terminates or the cancellation token in CoreM tells us to abort or timeout seconds have passed.

Equations

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

def Lean.Meta.Tactic.BVDecide.External.satQuery (solverPath problemPath proofOutput : System.FilePath) (timeout : Nat) (binaryProofs : Bool) (mode : Elab.Tactic.BVDecide.SolverMode) : CoreM SolverResult

Call the SAT solver in solverPath with problemPath as CNF input and ask it to output an LRAT UNSAT proof (binary or non-binary depending on binaryProofs) into proofOutput. To avoid runaway solvers the solver is run with timeout in seconds as a maximum time limit to solve the problem.

Note: This function currently assume that the solver has the same CLI as CaDiCal.

Equations

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