Lean.Elab.Tactic.BVDecide.External

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

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.

source

@[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

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

source

partial def Lean.Elab.Tactic.BVDecide.External.ModelParser.parseLines.go (acc : Array (Bool × Nat)) :

Std.Internal.Parsec.ByteArray.Parser (Array (Bool × Nat))

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

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

source

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 α

source

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.

source

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

Lean.CoreM (Lean.Elab.Tactic.BVDecide.External.TimedOut IO.Process.Output)

source

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

source

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.

source

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.

source

def Lean.Elab.Tactic.BVDecide.External.satQuery (solverPath : Lake.FilePath) (problemPath : Lake.FilePath) (proofOutput : Lake.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.