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))

@[inline]

def Lean.Elab.Tactic.BVDecide.External.ModelParser.parsePartialAssignment.wsLit : Std.Internal.Parsec.ByteArray.Parser Int

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

partial def Lean.Elab.Tactic.BVDecide.External.ModelParser.parseLines.go (acc : Array (Bool × Nat)) : 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.

partial def Lean.Elab.Tactic.BVDecide.External.runInterruptible.go {cfg : IO.Process.StdioConfig} (budgetMs : Nat) (child : IO.Process.Child cfg) (stdout stderr : Task (Except IO.Error String)) : CoreM (TimedOut IO.Process.Output)

def Lean.Elab.Tactic.BVDecide.External.runInterruptible.killAndWait {cfg : IO.Process.StdioConfig} (child : IO.Process.Child cfg) : IO Unit

def Lean.Elab.Tactic.BVDecide.External.runInterruptible.withTimeoutCheck {α : Type} (budgetMs : Nat) (cleanup : CoreM Unit) (x : CoreM (TimedOut α)) : CoreM (TimedOut α)

def Lean.Elab.Tactic.BVDecide.External.runInterruptible.withInterruptCheck {α : Type} (cleanup : CoreM Unit) (x : CoreM α) : CoreM α

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