From 784c1dceeeb0430a6aa7216a289a47966af65fa8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 27 Apr 2021 23:04:08 -0400
Subject: [PATCH] feat(main): `-o` to dump proof into a file

---
 src/main/main.ml       |  7 +++++--
 src/smtlib/Process.ml  | 17 +++++++++++++++--
 src/smtlib/Process.mli |  1 +
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/src/main/main.ml b/src/main/main.ml
index cc2bc7f7..e37c228f 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -31,6 +31,7 @@ let gc = ref true
 let p_stat = ref false
 let p_gc_stat = ref false
 let p_progress = ref false
+let proof_file = ref ""
 
 let hyps : Term.t list ref = ref []
 
@@ -73,6 +74,7 @@ let argspec = Arg.align [
     "--stat", Arg.Set p_stat, " print statistics";
     "--proof", Arg.Set p_proof, " print proof";
     "--no-proof", Arg.Clear p_proof, " do not print proof";
+    "-o", Arg.Set_string proof_file, " file into which to output a proof";
     "--model", Arg.Set p_model, " print model";
     "--no-model", Arg.Clear p_model, " do not print model";
     "--gc-stat", Arg.Set p_gc_stat, " outputs statistics about the GC";
@@ -153,9 +155,10 @@ let main () =
         Process.th_lra;
       ]
     in
-    let store_proof = !check || !p_proof in
+    let store_proof = !check || !p_proof || !proof_file <> "" in
     Process.Solver.create ~store_proof ~theories tst () ()
   in
+  let proof_file = if !proof_file ="" then None else Some !proof_file in
   if !check then (
     (* might have to check conflicts *)
     Solver.add_theory solver Process.Check_cc.theory;
@@ -172,7 +175,7 @@ let main () =
       E.fold_l
         (fun () ->
            Process.process_stmt
-             ~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
+             ~hyps ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf ?proof_file
              ~time:!time_limit ~memory:!size_limit
              ?dot_proof ~pp_proof:!p_proof ~pp_model:!p_model
              ~check:!check ~progress:!p_progress
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index 9bb054da..bd83fbbb 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -145,6 +145,7 @@ let solve
     ?dot_proof
     ?(pp_proof=false)
     ?(pp_model=false)
+    ?proof_file
     ?(check=false)
     ?time:_ ?memory:_ ?(progress=false)
     ?hyps:_
@@ -201,6 +202,17 @@ let solve
         | _ -> ()
       end;
 
+      begin match proof_file, proof with
+        | Some file, lazy (Some p) ->
+          Profile.with_ "proof.write-file" @@ fun () ->
+          let p = Profile.with1 "proof.mk-proof" Solver.Pre_proof.to_proof p in
+          CCIO.with_out file
+            (fun oc ->
+               let fmt = Format.formatter_of_out_channel oc in
+               Fmt.fprintf fmt "%a@." Proof.Quip.pp p);
+        | _ -> ()
+      end;
+
       let t3 = Sys.time () -. t2 in
       Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
 
@@ -220,7 +232,8 @@ let solve
 (* process a single statement *)
 let process_stmt
     ?hyps
-    ?gc ?restarts ?(pp_cnf=false) ?dot_proof ?pp_proof ?pp_model ?(check=false)
+    ?gc ?restarts ?(pp_cnf=false)
+    ?dot_proof ?pp_proof ?proof_file ?pp_model ?(check=false)
     ?time ?memory ?progress
     (solver:Solver.t)
     (stmt:Statement.t) : unit or_error =
@@ -259,7 +272,7 @@ let process_stmt
           l
       in
       solve
-        ?gc ?restarts ?dot_proof ~check ?pp_proof ?pp_model
+        ?gc ?restarts ?dot_proof ~check ?pp_proof ?proof_file ?pp_model
         ?time ?memory ?progress
         ~assumptions ?hyps
         solver;
diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli
index 8779e99f..7277edaa 100644
--- a/src/smtlib/Process.mli
+++ b/src/smtlib/Process.mli
@@ -26,6 +26,7 @@ val process_stmt :
   ?pp_cnf:bool ->
   ?dot_proof:string ->
   ?pp_proof:bool ->
+  ?proof_file:string ->
   ?pp_model:bool ->
   ?check:bool ->
   ?time:float ->