From 3aadb055b68c480eeea21d45f019965595823d26 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 19 Mar 2021 17:26:30 -0400
Subject: [PATCH] refactor: make proof production lazy

---
 src/core/Sidekick_core.ml               |  2 +-
 src/msat-solver/Sidekick_msat_solver.ml |  6 +++---
 src/smtlib/Process.ml                   | 16 +++++++++-------
 3 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 4f5a62a2..d0b572b0 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -698,7 +698,7 @@ module type SOLVER = sig
   type res =
     | Sat of Model.t
     | Unsat of {
-        proof: proof option;
+        proof: proof option lazy_t;
         unsat_core: Atom.t list lazy_t;
       }
     | Unknown of Unknown.t
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 0aa1173a..49f5a0fa 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -593,7 +593,7 @@ module Make(A : ARG)
   type res =
     | Sat of Model.t
     | Unsat of {
-        proof: proof option;
+        proof: proof option lazy_t;
         unsat_core: Atom.t list lazy_t;
       }
     | Unknown of Unknown.t
@@ -653,13 +653,13 @@ module Make(A : ARG)
       do_on_exit ();
       Sat m
     | Sat_solver.Unsat us ->
-      let proof =
+      let proof = lazy (
         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
+      ) in
       let unsat_core = lazy (us.Msat.unsat_assumptions ()) in
       do_on_exit ();
       Unsat {proof; unsat_core}
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 5ccbfc4e..dbd6f529 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -178,15 +178,16 @@ let solve
          *)
       let t3 = Sys.time () -. t2 in
       Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
-    | Solver.Unsat {proof=None;_} ->
-      Format.printf "Unsat (%.3f/%.3f/-)@." t1 (t2-.t1);
-    | Solver.Unsat {proof=Some p;_} ->
+    | Solver.Unsat {proof;_} ->
       if check then (
-        Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
+        match proof with
+        | lazy (Some p) ->
+          Profile.with_ "unsat.check" (fun () -> Solver.Proof.check p);
+        | _ -> ()
       );
-      begin match dot_proof with
-        | None ->  ()
-        | Some file ->
+      begin match dot_proof, proof with
+        | None, _ ->  ()
+        | Some file, lazy (Some p) ->
           Profile.with_ "dot.proof" @@ fun () ->
           CCIO.with_out file
             (fun oc ->
@@ -194,6 +195,7 @@ let solve
                let fmt = Format.formatter_of_out_channel oc in
                Solver.Proof.pp_dot 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;