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.Elab.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.

def Lean.Elab.Tactic.BVDecide.External.ModelParser.parsePartialAssignment : Std.Internal.Parsec.ByteArray.Parser (Bool × Array (Bool × Nat))

def Lean.Elab.Tactic.BVDecide.External.ModelParser.parseLines : Std.Internal.Parsec.ByteArray.Parser (Array (Bool × Nat))

@[inline]

def Lean.Elab.Tactic.BVDecide.External.ModelParser.parseHeader : Std.Internal.Parsec.ByteArray.Parser Unit

def Lean.Elab.Tactic.BVDecide.External.ModelParser.parse : Std.Internal.Parsec.ByteArray.Parser (Array (Bool × Nat))

Parse the witness format of a SAT solver. The rough grammar for this is: line = "v" (" " lit)\n terminal_line = "v" (" " lit) (" " 0)\n witness = "s SATISFIABLE\n" line+ terminal_line

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

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

def Lean.Elab.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.

def Lean.Elab.Tactic.BVDecide.External.satQuery (solverPath problemPath proofOutput : System.FilePath) (timeout : Nat) (binaryProofs : Bool) (mode : Frontend.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.