From 63e7d6659e34a417f8a32128bb92be01f1a2fc8f Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 20 Oct 2021 20:41:51 -0400
Subject: [PATCH] wip: dump more steps to the trace file

---
 src/base/Proof.ml       | 13 ++++++++++++-
 src/base/Proof_quip.ml  |  2 +-
 src/base/proof_ser.bare |  2 +-
 src/base/proof_ser.ml   |  8 ++++----
 src/main/main.ml        |  4 ++++
 src/util/Chunk_stack.ml | 17 +++++++++++------
 6 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/base/Proof.ml b/src/base/Proof.ml
index 30dc7efc..9cefc241 100644
--- a/src/base/Proof.ml
+++ b/src/base/Proof.ml
@@ -197,7 +197,18 @@ let emit_lit_ (self:t) (lit:Lit.t) : term_id =
   let t = emit_term_ self (Lit.term lit) in
   if sign then t else Int32.neg t
 
-let emit_redundant_clause _ ~hyps:_ _ = dummy_step
+let emit_redundant_clause lits ~hyps (self:t) =
+  if enabled self then (
+    let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
+    let clause = Proof_ser.{Clause.lits} in
+    let hyps = Iter.to_array hyps in
+    let id = alloc_id self in
+    emit_step_ self (
+      Proof_ser.({Step.id; view=Step_view.Step_rup {res=clause; hyps}})
+    );
+    id
+  ) else dummy_step
+
 let emit_input_clause (lits:Lit.t Iter.t) (self:t) =
   if enabled self then (
     let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml
index dced6942..a688eaa1 100644
--- a/src/base/Proof_quip.ml
+++ b/src/base/Proof_quip.ml
@@ -533,6 +533,6 @@ let pp_debug ~sharing out p =
   M.pp_debug ~sharing p out
 
 
-let of_proof _ _ : t = assert false
+let of_proof _ _ : t = Sorry
 
 let output = Quip.output
diff --git a/src/base/proof_ser.bare b/src/base/proof_ser.bare
index b4a05cd4..4dea2005 100644
--- a/src/base/proof_ser.bare
+++ b/src/base/proof_ser.bare
@@ -13,7 +13,7 @@ type Step_input {
 # clause, RUP with previous steps
 type Step_rup {
   res: Clause
-  steps: []ID
+  hyps: []ID
 }
 
 # TODO: remove?
diff --git a/src/base/proof_ser.ml b/src/base/proof_ser.ml
index 421660a1..4033042c 100644
--- a/src/base/proof_ser.ml
+++ b/src/base/proof_ser.ml
@@ -302,22 +302,22 @@ end
 module Step_rup = struct
   type t = {
     res: Clause.t;
-    steps: ID.t array;
+    hyps: ID.t array;
   }
   
   (** @raise Bare.Decode.Error in case of error. *)
   let decode (dec: Bare.Decode.t) : t =
     let res = Clause.decode dec in
-    let steps =
+    let hyps =
       (let len = Bare.Decode.uint dec in
        if len>Int64.of_int Sys.max_array_length then raise (Bare.Decode.Error"array too big");
        Array.init (Int64.to_int len) (fun _ -> ID.decode dec)) in
-    {res; steps; }
+    {res; hyps; }
   
   let encode (enc: Bare.Encode.t) (self: t) : unit =
     begin
       Clause.encode enc self.res;
-      (let arr = self.steps in
+      (let arr = self.hyps in
        Bare.Encode.uint enc (Int64.of_int (Array.length arr));
        Array.iter (fun xi -> ID.encode enc xi) arr);
     end
diff --git a/src/main/main.ml b/src/main/main.ml
index 0f37c096..210c68dc 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -105,8 +105,12 @@ let main_smt () : _ result =
   (* call [k] with the name of a temporary proof file, and cleanup if necessary *)
   let run_with_tmp_file k =
     if enable_proof_ then (
+      let file = ".sidekick-trace.dat" in
+      k file
+      (*  TODO
       CCIO.File.with_temp
         ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat" k
+          *)
     ) else (
       k "/dev/null"
     )
diff --git a/src/util/Chunk_stack.ml b/src/util/Chunk_stack.ml
index 5547cb75..1c73fc94 100644
--- a/src/util/Chunk_stack.ml
+++ b/src/util/Chunk_stack.ml
@@ -71,16 +71,21 @@ module Writer = struct
 
   let into_channel (oc:out_channel) : t =
     let blen = Bytes.create 4 in
+
+    (* add len after chunk *)
+    let[@inline] emit_len_ len =
+      Bytes.set_int32_le blen 0 (Int32.of_int len);
+      output oc blen 0 4;
+      flush oc
+    in
+
     let write b i len =
       output oc b i len;
-      (* add len *)
-      Bytes.set_int32_le blen 0 (Int32.of_int len);
-      output oc blen 0 4
+      emit_len_ len
+
     and write_buf buf =
       Buffer.output_buffer oc buf;
-      (* add len *)
-      Bytes.set_int32_le blen 0 (Int32.of_int (Buffer.length buf));
-      output oc blen 0 4
+      emit_len_ (Buffer.length buf);
     in
     { write; write_buf; }