feat(main): for pure SAT, emit proofs into file or locally

src/main/main.ml

@@ -143,49 +143,28 @@ let main_smt () : _ result =
 let main_cnf () : _ result =
   let module Proof = Pure_sat_solver.Proof in
   let module S = Pure_sat_solver in
-  (* TODO: switch proof depending on whether we need proofs or not *)
-  let proof = Proof.dummy in
 
-  (* FIXME: this should go in the proof module, or is already redundant? *)
-  let close_proof_, on_learnt, on_gc =
-    if !proof_file ="" then (
-      (fun() -> ()), None, None
+  let proof, in_memory_proof =
+    if !check then (
+      let pr, inmp = Proof.create_in_memory () in
+      pr, Some inmp
+    ) else if !proof_file <> "" then (
+      Proof.create_to_file !proof_file, None
     ) else (
-      let oc = open_out !proof_file in
-      let pp_lits lits =
-        Array.iteri (fun i v ->
-            if i>0 then output_char oc ' ';
-            output_string oc (string_of_int v))
-          lits
-      in
-      let pp_c solver c =
-        let store = S.SAT.store solver in
-        let lits = S.SAT.Clause.lits_a store c in
-        pp_lits lits
-      in
-      let on_learnt solver c =
-        pp_c solver c; output_string oc " 0\n";
-      and on_gc solver c =
-        output_string oc "d "; pp_lits c; output_string oc " 0\n";
-        ()
-      and close () =
-        flush oc;
-        close_out_noerr oc;
-      in
-      close, Some on_learnt, Some on_gc
+      Proof.dummy, None
     )
   in
 
   let stat = Stat.create () in
-  let solver =
-    S.SAT.create
-      ~size:`Big ?on_learnt ?on_gc ~proof ~stat ()
-  in
+  let solver = S.SAT.create ~size:`Big ~proof ~stat () in
 
   S.Dimacs.parse_file solver !file >>= fun () ->
-  let r = S.solve  ~check:!check solver in
+  let r = S.solve ~check:!check ?in_memory_proof solver in
 
-  close_proof_();
+  (* FIXME: if in memory proof and !proof_file<>"",
+     then dump proof into file now *)
+
+  Proof.close proof;
   if !p_stat then (
     Fmt.printf "%a@." Stat.pp_all (Stat.all stat);
   );

src/main/pure_sat_solver.ml

@@ -19,62 +19,98 @@ end
 module Proof : sig
   include Sidekick_sat.PROOF with type lit = Lit.t
 
+  type in_memory
+
   val dummy : t
-  val create : unit -> t
-  val to_string : t -> string
-  val to_chan : out_channel -> t -> unit
+
+  val create_in_memory : unit -> t * in_memory
+  val to_string : in_memory -> string
+  val to_chan : out_channel -> in_memory -> unit
+
+  val create_to_file : string -> t
+  val close : t -> unit
+
   type event = Sidekick_bin_lib.Drup_parser.event =
     | Input of int list
     | Add of int list
     | Delete of int list
-  val iter_events : t -> event Iter.t
+  val iter_events : in_memory -> event Iter.t
 end = struct
   let bpf = Printf.bprintf
+  let fpf = Printf.fprintf
+
   type lit = Lit.t
+  type in_memory = Buffer.t
   type t =
     | Dummy
-    | Inner of {
-        buf: Buffer.t;
+    | Inner of in_memory
+    | Out of {
+        oc: out_channel;
+        close: (unit -> unit);
       }
+
   type dproof = t -> unit
 
   let[@inline] with_proof pr f = match pr with
     | Dummy -> ()
-    | Inner _ -> f pr
+    | Inner _ | Out _ -> f pr
 
-  let emit_lits_ buf lits =
+  let[@inline] emit_lits_buf_ buf lits =
     lits (fun i -> bpf buf "%d " i)
+  let[@inline] emit_lits_out_ oc lits =
+    lits (fun i -> fpf oc "%d " i)
 
   let emit_input_clause lits self =
     match self with
     | Dummy -> ()
-    | Inner {buf} ->
-      bpf buf "i "; emit_lits_ buf lits; bpf buf "0\n"
+    | Inner buf ->
+      bpf buf "i "; emit_lits_buf_ buf lits; bpf buf "0\n"
+    | Out {oc;_} ->
+      fpf oc "i "; emit_lits_out_ oc lits; fpf oc "0\n"
 
   let emit_redundant_clause lits self =
     match self with
     | Dummy -> ()
-    | Inner {buf} ->
-      bpf buf "r "; emit_lits_ buf lits; bpf buf "0\n"
+    | Inner buf ->
+      bpf buf "r "; emit_lits_buf_ buf lits; bpf buf "0\n"
+    | Out {oc;_} -> fpf oc "r "; emit_lits_out_ oc lits; fpf oc "0\n"
 
   let del_clause lits self =
     match self with
     | Dummy -> ()
-    | Inner {buf} ->
-      bpf buf "d "; emit_lits_ buf lits; bpf buf "0\n"
+    | Inner buf ->
+      bpf buf "d "; emit_lits_buf_ buf lits; bpf buf "0\n"
+    | Out {oc; _}->
+      fpf oc "d "; emit_lits_out_ oc lits; fpf oc "0\n"
 
   (* lifetime *)
 
   let dummy : t = Dummy
-  let create () : t = Inner {buf=Buffer.create 1_024}
+  let create_in_memory () : t * in_memory =
+    let buf = Buffer.create 1_024 in
+    Inner buf, buf
 
-  let to_string = function
-    | Dummy -> ""
-    | Inner {buf} -> Buffer.contents buf
+  let create_to_file file =
+    let oc, close =
+      match Filename.extension file with
+      | ".gz" ->
+        let cmd = Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file) in
+        Log.debugf 1 (fun k->k"proof file: command is %s" cmd);
+        let oc = Unix.open_process_out cmd in
+        oc, (fun () -> ignore (Unix.close_process_out oc: Unix.process_status))
+      | ".drup" ->
+        let oc = open_out_bin file in
+        oc, (fun () -> close_out_noerr oc)
+      | s -> Error.errorf "unknown file extension '%s'" s
+    in
+    Out {oc; close}
 
-  let to_chan oc = function
-    | Dummy -> ()
-    | Inner {buf} -> Buffer.output_buffer oc buf; flush oc
+  let close = function
+    | Dummy | Inner _ -> ()
+    | Out {close; oc} -> flush oc; close()
+
+  let to_string = Buffer.contents
+  let to_chan = Buffer.output_buffer
 
   module DP = Sidekick_bin_lib.Drup_parser
 
@@ -84,12 +120,9 @@ end = struct
     | Delete of int list
 
   (* parse the proof back *)
-  let iter_events (self:t) : DP.event Iter.t =
-    match self with
-    | Dummy -> Iter.empty
-    | Inner {buf} ->
-      let dp = DP.create_string (to_string self) in
-      DP.iter dp
+  let iter_events (self:in_memory) : DP.event Iter.t =
+    let dp = DP.create_string (to_string self) in
+    DP.iter dp
 end
 
 module Arg = struct
@@ -118,7 +151,7 @@ module Dimacs = struct
       E.of_exn_trace e
 end
 
-let check_proof proof : bool =
+let check_proof (proof:Proof.in_memory) : bool =
   Profile.with_ "pure-sat.check-proof" @@ fun () ->
   let module SDRUP = Sidekick_drup.Make() in
   let store = SDRUP.Clause.create() in
@@ -149,7 +182,7 @@ let check_proof proof : bool =
     );
   !ok
 
-let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
+let solve ?(check=false) ?in_memory_proof (solver:SAT.t) : (unit, string) result =
   let res =
     Profile.with_ "solve" (fun () -> SAT.solve solver)
   in
@@ -162,11 +195,14 @@ let solve ?(check=false) (solver:SAT.t) : (unit, string) result =
     | SAT.Unsat (module US) ->
 
       if check then (
-        let proof = SAT.proof solver in
-        let ok = check_proof proof in
-        if not ok then (
-          Error.errorf "Proof validation failed"
-        );
+        match in_memory_proof with
+        | None ->
+          Error.errorf "Cannot validate proof, no in-memory proof provided"
+        | Some proof ->
+          let ok = check_proof proof in
+          if not ok then (
+            Error.errorf "Proof validation failed"
+          );
       );
 
       let t3 = Sys.time () -. t2 in