test: move External and LRAT tests out of the core repo

LeanSAT/External/LRAT.lean

@@ -236,17 +236,3 @@ def parseLRATProof (path : System.FilePath) : IO (Option (Array IntAction)) := d
     | none => encounteredError := true
   if encounteredError then return none
   else return some proof
-
-syntax (name := loadLRATCommand) "loadLRAT " strLit : command
-
-@[command_elab loadLRATCommand] def elabLoadLRAT : CommandElab := fun stx => do
-  match stx with
-  | `(loadLRAT $file) =>
-    match Syntax.isStrLit? file with
-    | some file =>
-        let proof ← loadLRATProof file
-        IO.println s!"{proof}"
-    | _ => throwError "Expected strLit: {file}"
-  | _ => throwError "Failed to parse loadLRAT command"
-
-loadLRAT "./pigeon-hole/hole6.lrat"

LeanSAT/LRAT/LRATChecker.lean

@@ -62,25 +62,3 @@ def lratChecker [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (prf
     if checkSuccess then lratChecker f restPrf
     else rup_failure
   | del ids :: restPrf => lratChecker (delete f ids) restPrf
-
-open Lean Parser Elab Command Dimacs
-
-syntax (name := lratCheckCommand) "lratCheck" strLit strLit : command
-
-@[command_elab lratCheckCommand] def runLRATCheck : CommandElab := fun stx => do
-  match stx with
-  | `(lratCheck $problemFile $prfFile) =>
-    match Syntax.isStrLit? problemFile, Syntax.isStrLit? prfFile with
-    | some problemFile, some prfFile =>
-      let ⟨n, formula⟩ ← loadProblem problemFile
-      let formula : DefaultFormula n := DefaultFormula.ofArray formula
-      let proof ← loadLRATProof prfFile
-      IO.println s!"formula: {formula.dimacs}\n"
-      -- O.println s!"proof: {proof}\n"
-      let proof ← proof.mapM $ intActionToDefaultClauseAction n
-      IO.println s!"lratChecker output: {lratChecker formula proof.toList}"
-    | _, _ => throwError "Either {problemFile} or {prfFile} did not register as a string literal"
-  | _ => throwError "Failed to parse loadLRAT command"
-
-lratCheck "./pigeon-hole/hole6.cnf" "./pigeon-hole/hole6.lrat"
-lratCheck "./pigeon-hole/hole7.cnf" "./pigeon-hole/hole7.lrat"

Test.lean

@@ -1,3 +1,5 @@
 import Test.Sat
 import Test.ExternalDimacs
+import Test.LRAT
+import Test.LRATChecker
 import Test.PHPDemo

Test/LRAT.lean

@@ -0,0 +1,17 @@
+import LeanSAT.External.LRAT
+
+open LRAT Lean Parser Elab Command
+
+syntax (name := loadLRATCommand) "loadLRAT " strLit : command
+
+@[command_elab loadLRATCommand] def elabLoadLRAT : CommandElab := fun stx => do
+  match stx with
+  | `(loadLRAT $file) =>
+    match Syntax.isStrLit? file with
+    | some file =>
+        let proof ← loadLRATProof file
+        IO.println s!"{proof}"
+    | _ => throwError "Expected strLit: {file}"
+  | _ => throwError "Failed to parse loadLRAT command"
+
+loadLRAT "./pigeon-hole/hole6.lrat"

Test/LRATChecker.lean

@@ -0,0 +1,23 @@
+import LeanSAT.LRAT.LRATChecker
+
+open LRAT Lean Parser Elab Command Dimacs
+
+syntax (name := lratCheckCommand) "lratCheck" strLit strLit : command
+
+@[command_elab lratCheckCommand] def runLRATCheck : CommandElab := fun stx => do
+  match stx with
+  | `(lratCheck $problemFile $prfFile) =>
+    match Syntax.isStrLit? problemFile, Syntax.isStrLit? prfFile with
+    | some problemFile, some prfFile =>
+      let ⟨n, formula⟩ ← loadProblem problemFile
+      let formula : DefaultFormula n := DefaultFormula.ofArray formula
+      let proof ← loadLRATProof prfFile
+      IO.println s!"formula: {formula.dimacs}\n"
+      -- O.println s!"proof: {proof}\n"
+      let proof ← proof.mapM $ intActionToDefaultClauseAction n
+      IO.println s!"lratChecker output: {lratChecker formula proof.toList}"
+    | _, _ => throwError "Either {problemFile} or {prfFile} did not register as a string literal"
+  | _ => throwError "Failed to parse loadLRAT command"
+
+lratCheck "./pigeon-hole/hole6.cnf" "./pigeon-hole/hole6.lrat"
+lratCheck "./pigeon-hole/hole7.cnf" "./pigeon-hole/hole7.lrat"