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: Array (Bool × Nat) → Lean.Elab.Tactic.BVDecide.External.SolverResult

  The solver returned SAT with some literal assignment.

• unsat: Lean.Elab.Tactic.BVDecide.External.SolverResult

  The solver returned UNSAT.

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.

@[inline]

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

Equations

• Lean.Elab.Tactic.BVDecide.External.ModelParser.parsePartialAssignment.wsLit = do Std.Internal.Parsec.ByteArray.skipByteChar ' ' Std.Tactic.BVDecide.LRAT.Parser.Text.parseLit

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 #[]

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

Equations

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

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

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

• success: {α : Type u} → α → Lean.Elab.Tactic.BVDecide.External.TimedOut α
• timeout: {α : Type u} → Lean.Elab.Tactic.BVDecide.External.TimedOut α

def Lean.Elab.Tactic.BVDecide.External.runInterruptible (timeout : Nat) (args : IO.Process.SpawnArgs) : Lean.CoreM (Lean.Elab.Tactic.BVDecide.External.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.

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)) : Lean.CoreM (Lean.Elab.Tactic.BVDecide.External.TimedOut IO.Process.Output)

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

Equations

• Lean.Elab.Tactic.BVDecide.External.runInterruptible.killAndWait child = do child.kill discard child.wait

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

Equations

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

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

Equations

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

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