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.

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

Instances For

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

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

Instances For

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

- Lean.Elab.Tactic.BVDecide.External.ModelParser.parseLines = Lean.Elab.Tactic.BVDecide.External.ModelParser.parseLines.go✝ #[]

Instances For

source
@[inline]
def Lean.Elab.Tactic.BVDecide.External.ModelParser.parseHeader :
Std.Internal.Parsec.ByteArray.Parser Unit
Equations

- Lean.Elab.Tactic.BVDecide.External.ModelParser.parseHeader = do Std.Internal.Parsec.ByteArray.skipString "s SATISFIABLE" Std.Tactic.BVDecide.LRAT.Parser.Text.skipNewline

Instances For

source
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

Equations

- Lean.Elab.Tactic.BVDecide.External.ModelParser.parse = do Lean.Elab.Tactic.BVDecide.External.ModelParser.parseHeader Lean.Elab.Tactic.BVDecide.External.ModelParser.parseLines

Instances For

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

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For