From a205c429e73e70cc338836a87589ae6323e48e71 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 2 Aug 2021 23:13:18 -0400
Subject: [PATCH] feat(sat): check proofs if asked to

---
 src/main/main.ml            | 3 ++-
 src/main/pure_sat_solver.ml | 9 +++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index c2d6e68b..921567e8 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -149,8 +149,9 @@ let main_cnf () : _ result =
       ~on_new_atom:(fun _ -> incr n_atoms)
       ~size:`Big ()
   in
+
   S.Dimacs.parse_file solver !file >>= fun () ->
-  let r = S.solve solver in
+  let r = S.solve  ~check:!check solver in
   if !p_stat then (
     Fmt.printf "; n-conflicts: %d n-decisions: %d n-propagations: %d@.\
                 ; n-restarts: %d n-atoms: %d@."
diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index da8e094d..261e0322 100644
--- a/src/main/pure_sat_solver.ml
+++ b/src/main/pure_sat_solver.ml
@@ -40,7 +40,7 @@ module Dimacs = struct
       E.of_exn_trace e
 end
 
-let solve (solver:SAT.t) : (unit, string) result =
+let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
   let res =
     Profile.with_ "solve" (fun () -> SAT.solve solver)
   in
@@ -50,7 +50,12 @@ let solve (solver:SAT.t) : (unit, string) result =
     | SAT.Sat _ ->
       let t3 = Sys.time () -. t2 in
       Format.printf "Sat (%.3f/%.3f)@." t2 t3;
-    | SAT.Unsat _ ->
+    | SAT.Unsat (module US) ->
+
+      if check then (
+        let pr = US.get_proof() in
+        SAT.Proof.check (SAT.store solver) pr;
+      );
 
       let t3 = Sys.time () -. t2 in
       Format.printf "Unsat (%.3f/%.3f)@." t2 t3;