From 5865151247e7a6d2ef5abcd78789c58932721548 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 10 Feb 2019 16:59:27 -0600
Subject: [PATCH] refactor: return optional proof, do not store if if
 `-no-check` was given

---
 src/main/main.ml      |  2 +-
 src/smt/Solver.ml     | 16 +++++++++++-----
 src/smt/Solver.mli    |  3 ++-
 src/smtlib/Process.ml | 24 +++++++++++++-----------
 4 files changed, 27 insertions(+), 18 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index 5f21f13c..f6a371f2 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -107,7 +107,7 @@ let main () =
       | Smtlib ->
         [Sidekick_th_bool.th] (* TODO: more theories *)
     in
-    Sidekick_smt.Solver.create ~theories ()
+    Sidekick_smt.Solver.create ~store_proof:!check ~theories ()
   in
   let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
   begin match syn with
diff --git a/src/smt/Solver.ml b/src/smt/Solver.ml
index d3cc98d6..e38aaf80 100644
--- a/src/smt/Solver.ml
+++ b/src/smt/Solver.ml
@@ -63,10 +63,10 @@ let[@inline] mk_atom_t self ?sign t : Atom.t =
   let lit = Lit.atom ?sign t in
   mk_atom_lit self lit
 
-let create ?size ?(config=Config.empty) ~theories () : t =
+let create ?size ?(config=Config.empty) ?store_proof ~theories () : t =
   let th_combine = Theory_combine.create() in
   let self = {
-    solver=Sat_solver.create ?size th_combine;
+    solver=Sat_solver.create ?store_proof ?size th_combine;
     stat=Stat.create ();
     config;
   } in
@@ -168,7 +168,7 @@ let pp_model = Model.pp
 
 type res =
   | Sat of model
-  | Unsat of Proof.t
+  | Unsat of Proof.t option
   | Unknown of unknown
 
 (** {2 Main} *)
@@ -221,7 +221,7 @@ let check_model (_s:t) : unit =
 
 (* TODO: main loop with iterative deepening of the unrolling  limit
    (not the value depth limit) *)
-let solve ?(on_exit=[]) ?check:(_=true) ~assumptions (self:t) : res =
+let solve ?(on_exit=[]) ?(check=true) ~assumptions (self:t) : res =
   let r = Sat_solver.solve ~assumptions (solver self) in
   match r with
   | Sat_solver.Sat st ->
@@ -237,7 +237,13 @@ let solve ?(on_exit=[]) ?check:(_=true) ~assumptions (self:t) : res =
     Unknown U_incomplete (* TODO *)
     *)
   | Sat_solver.Unsat us ->
-    let pr = us.get_proof () in
+    let pr =
+      try
+        let pr = us.get_proof () in
+        if check then Sat_solver.Proof.check pr;
+        Some pr
+      with Msat.Solver_intf.No_proof -> None
+    in
     do_on_exit ~on_exit;
     Unsat pr
 
diff --git a/src/smt/Solver.mli b/src/smt/Solver.mli
index c66cdccd..a2ea550e 100644
--- a/src/smt/Solver.mli
+++ b/src/smt/Solver.mli
@@ -30,7 +30,7 @@ type unknown =
 
 type res =
   | Sat of Model.t
-  | Unsat of Proof.t
+  | Unsat of Proof.t option
   | Unknown of unknown
 
 (** {2 Main} *)
@@ -41,6 +41,7 @@ type t
 val create :
   ?size:[`Big | `Tiny | `Small] ->
   ?config:Config.t ->
+  ?store_proof:bool ->
   theories:Theory.t list ->
   unit -> t
 
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index c01e816b..dbf59206 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -287,20 +287,22 @@ let solve
       );
       let t3 = Sys.time () -. t2 in
       Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
-    | Solver.Unsat p ->
+    | Solver.Unsat None ->
+      Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
+    | Solver.Unsat (Some p) ->
       if check then (
         Solver.Proof.check p;
-        begin match dot_proof with
-          | None ->  ()
-          | Some file ->
-            CCIO.with_out file
-              (fun oc ->
-                 Log.debugf 1 (fun k->k "write proof into `%s`" file);
-                 let fmt = Format.formatter_of_out_channel oc in
-                 Dot.pp fmt p;
-                 Format.pp_print_flush fmt (); flush oc)
-        end
       );
+      begin match dot_proof with
+        | None ->  ()
+        | Some file ->
+          CCIO.with_out file
+            (fun oc ->
+               Log.debugf 1 (fun k->k "write proof into `%s`" file);
+               let fmt = Format.formatter_of_out_channel oc in
+               Dot.pp fmt p;
+               Format.pp_print_flush fmt (); flush oc)
+      end;
       let t3 = Sys.time () -. t2 in
       Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
     | Solver.Unknown reas ->