Skip to content
This repository has been archived by the owner on Aug 29, 2024. It is now read-only.

Commit

Permalink
style: format and cleanup External
Browse files Browse the repository at this point in the history
  • Loading branch information
@hargoniX
hargoniX committed Jul 16, 2024
1 parent 30fcb07 commit 30448db
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 71 deletions.
79 changes: 19 additions & 60 deletions LeanSAT/External/DimacsLRAT.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,19 +10,23 @@ open LRAT Lean Parser Elab Command DefaultClause

namespace Dimacs

def intToLiteral [Monad M] [MonadError M] {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : M (Literal (PosFin n)) :=
def intToLiteral [Monad m] [MonadError m] {n : Nat} (x : Int) (x_ne_zero : x ≠ 0)
: m (Literal (PosFin n)) :=
if h : x.natAbs < n then
if x > 0 then return (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
else return (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
else throwError "Given literal {x} is outside of the bounds specified by the number of variables"

/-- `loadProblem` takes in the path of a CNF file and attempts to output a number `n` (indicating the total number
of variables + 1) along with an Array of `DefaultClause n` Option expressions. This Array should match the
`ofArray` specification given in `Formula.Implementation.lean`.
if x > 0 then
return (⟨x.natAbs, ⟨by omega, h⟩⟩, true)
else
return (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
else
throwError "Given literal {x} is outside of the bounds specified by the number of variables"

`loadProblem` is written as a `CommandElabM` monad so that it can be used in commands such as `loadDimacs` at
the end of this file. -/
def loadProblem (path : System.FilePath) : CommandElabM (Σ n : Nat, Array (Option (DefaultClause n))) := do
/--
`loadProblem` takes in the path of a CNF file and attempts to output a number `n` (indicating the total number
of variables + 1) along with an Array of `DefaultClause n` Option expressions. This Array should match the
`ofArray` specification given in `Formula.Implementation.lean`.
-/
def loadProblem (path : System.FilePath) [Monad m] [MonadError m] [MonadLiftT IO m]
: m (Σ n : Nat, Array (Option (DefaultClause n))) := do
let lines ← IO.FS.lines path
let #[problemLine] := lines.filter fun l => l.startsWith "p"
| throwError "There must be exactly one problem line in the dimacs file"
Expand All @@ -48,14 +52,16 @@ def loadProblem (path : System.FilePath) : CommandElabM (Σ n : Nat, Array (Opti
if h : lit ≠ 0 then
match curClause.insert (← intToLiteral lit h) with
| some updatedClause => curClause := updatedClause
| none => throwError "Dimacs requires that no clause contain a complementary set of literals"
| none =>
throwError "Dimacs requires that no clause contain a complementary set of literals"
else
res := res.push curClause
curClause := empty -- Reset curClause because the 0 just terminated the previous clause
if curClause.clause ≠ [] then -- Dimacs format allows the last clause to not terminate in a 0
res := res.push curClause
if res.size != numClauses + 1 then
throwError "The problem line stated there were {numClauses} clauses but there are actually {res.size} (res: {res})"
throwError
"The problem line stated there were {numClauses} clauses but there are actually {res.size}"
return ⟨numVarsSucc, res⟩

def intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Literal (PosFin n)) := do
Expand All @@ -64,50 +70,3 @@ def intToLiteralPure {n : Nat} (x : Int) (x_ne_zero : x ≠ 0) : Option (Literal
else some (⟨x.natAbs, ⟨by omega, h⟩⟩, false)
else
none

/-- `parseProblem` takes in the path of a CNF file and attempts to output a number `n` (indicating the total number
of variables + 1) along with an Array of `DefaultClause n` Option expressions. This Array should match the
`ofArray` specification given in Implementation.lean.
`parseProblem` is written as an `IO` monad so that it can be used in programs such as `main`. Since the `IO` monad
does not support `throwError` in the way that `CommandElabM` does, `parseProblem` returns `none` where `loadProblem`
would throw an error. Other than this difference though, `loadProblem` and `parseProblem` are intended to be equivalent. -/
def parseProblem (path : System.FilePath) : IO (Option (Σ n : Nat, Array (Option (DefaultClause n)))) := do
let lines ← IO.FS.lines path
let #[problemLine] := lines.filter fun l => l.startsWith "p"
| IO.println "There must be exactly one problem line in the dimacs file"; return none
let [_, _, numVars, numClauses] := String.splitOn problemLine " "
| IO.println "Improperly formatted problem line"; return none
let some numVars := String.toNat? numVars
| IO.println "Improperly formatted problem line"; return none
let some numClauses := String.toNat? numClauses
| IO.println "Improperly formatted problem line"; return none

let numVarsSucc := numVars + 1

let lines := lines.filter fun l => not (l.startsWith "c" || l.startsWith "p")
let mut res : Array (Option (DefaultClause numVarsSucc)) := #[none]
let mut curClause : DefaultClause numVarsSucc := empty
for line in lines do
let line := line.replace "\t" " "
let c := (line.splitOn " ").toArray
for lit in c do
if lit = "" then continue
let some lit := String.toInt? lit
| IO.println s!"Clause {c} contains non-int {lit}"; return none
if h : lit ≠ 0 then
let some lit := intToLiteralPure lit h
| return none
match curClause.insert lit with
| some updatedClause => curClause := updatedClause
| none => IO.println s!"Dimacs requires that no clause contain a complementary set of literals"; return none
else
res := res.push curClause
curClause := empty -- Reset curClause because the 0 just terminated the previous clause
if curClause.clause ≠ [] then -- Dimacs format allows the last clause to not terminate in a 0
res := res.push curClause
if res.size != numClauses + 1 then
IO.println s!"The problem line stated there were {numClauses} clauses but there are actually {res.size - 1} (res: {res})"
return none
return some ⟨numVarsSucc, res⟩

28 changes: 17 additions & 11 deletions LeanSAT/External/Solver.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josh Clune
-/
import LeanSAT.External.LRAT
import Lean.Data.Parsec
import Lean.CoreM

inductive SolverResult where
Expand Down Expand Up @@ -74,10 +73,7 @@ partial def runInterruptible (args : IO.Process.SpawnArgs) : CoreM IO.Process.Ou
where
go {cfg} (child : IO.Process.Child cfg) (stdout stderr : Task (Except IO.Error String))
(tk : IO.CancelToken) : CoreM IO.Process.Output := do
if ← tk.isSet then
child.kill
throw <| .internal Core.interruptExceptionId
else
withInterruptCheck tk child.kill do
match ← child.tryWait with
| some exitCode =>
let stdout ← IO.ofExcept stdout.get
Expand All @@ -87,12 +83,22 @@ where
IO.sleep 50
go child stdout stderr tk

/-- By default, satQuery assumes that the user has cadical (≥ version 1.7.0) installed and their path set up so that it
can be run via the command `cadical` in terminal. If the path to the user's `cadical` is different, it can be provided
in the `solverPath` argument. `satQuery` will call cadical on the CNF file at `problemPath` and output an LRAT result
to `proofOutput` -/
def satQuery (solverPath := "cadical") (problemPath : System.FilePath) (proofOutput : System.FilePath)
(timeout : Nat) : CoreM SolverResult := do
withInterruptCheck {α : Type} (tk : IO.CancelToken) (interrupted : CoreM Unit) (x : CoreM α)
: CoreM α := do
if ← tk.isSet then
interrupted
throw <| .internal Core.interruptExceptionId
else
x

/--
By default, satQuery assumes that the user has cadical (≥ version 1.7.0) installed and their
path set up so that it can be run via the command `cadical` in terminal. If the path to the user's
`cadical` is different, it can be provided in the `solverPath` argument. `satQuery` will call
cadical on the CNF file at `problemPath` and output an LRAT result to `proofOutput`.
-/
def satQuery (solverPath := "cadical") (problemPath : System.FilePath)
(proofOutput : System.FilePath) (timeout : Nat) : CoreM SolverResult := do
let cmd := solverPath
let args := #[
problemPath.toString,
Expand Down

0 comments on commit 30448db

Please sign in to comment.