From ed114f8abee5c9c86e3131e9c133f7fea152acaa 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            | 4 +++-
 src/main/pure_sat_solver.ml | 9 +++++++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index 0c10a6fd..d26200f2 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -152,8 +152,10 @@ let main_cnf () : _ result =
       ~on_new_atom:(fun _ -> incr n_atoms)
       ~size:`Big ()
   in
+
   Pure_sat_solver.Dimacs.parse_file solver !file >>= fun () ->
-  let r = Pure_sat_solver.solve solver in
+  let r = Pure_sat_solver.solve ~check:!check solver in
+
   if !p_stat then (
     Fmt.printf "; n-atoms: %d n-conflicts: %d n-decisions: %d@."
       !n_atoms !n_confl !n_decision;
diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index da8e094d..52101ca3 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 pr;
+      );
 
       let t3 = Sys.time () -. t2 in
       Format.printf "Unsat (%.3f/%.3f)@." t2 t3;