From 3aadc640c4a342d39ed8d7fb21379f389708772c Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 30 Sep 2022 22:11:41 -0400
Subject: [PATCH] improve tracing, add `show_trace`

---
 src/base/Solver.ml               |  4 ++--
 src/bencode/Sidekick_bencode.ml  |  8 ++++++--
 src/bencode/Sidekick_bencode.mli |  8 ++++----
 src/core/t_tracer.ml             | 14 ++++++++++++--
 src/core/t_tracer.mli            | 19 ++++++++++++++-----
 src/main/dune                    |  8 ++++++++
 src/main/main.ml                 | 15 ++++++++++++++-
 src/main/pure_sat_solver.ml      |  1 +
 src/main/show_trace.ml           | 21 +++++++++++++++++++++
 src/smt/solver.ml                | 12 ++++++++----
 src/smt/solver.mli               | 10 ++++++----
 src/smt/solver_internal.ml       |  4 +++-
 src/smt/solver_internal.mli      |  8 +++++++-
 src/smt/tracer.ml                | 21 +++++++++++++++++++--
 src/smt/tracer.mli               | 26 +++++++++++++++++---------
 src/trace/entry_id.ml            |  3 +++
 src/trace/sink.ml                |  6 ++++++
 src/trace/sink.mli               |  3 +++
 src/trace/source.ml              | 28 +++++++++++++++++++---------
 19 files changed, 173 insertions(+), 46 deletions(-)
 create mode 100644 src/main/show_trace.ml

diff --git a/src/base/Solver.ml b/src/base/Solver.ml
index c6adfb2f..d2937f60 100644
--- a/src/base/Solver.ml
+++ b/src/base/Solver.ml
@@ -5,5 +5,5 @@ let default_arg =
     let view_as_cc = Term.view_as_cc
   end : Sidekick_smt_solver.Sigs.ARG)
 
-let create_default ?stat ?size ~proof ~theories tst : t =
-  create default_arg ?stat ?size ~proof ~theories tst ()
+let create_default ?stat ?size ?tracer ~proof ~theories tst : t =
+  create default_arg ?stat ?size ?tracer ~proof ~theories tst ()
diff --git a/src/bencode/Sidekick_bencode.ml b/src/bencode/Sidekick_bencode.ml
index cb32c3e3..87af3293 100644
--- a/src/bencode/Sidekick_bencode.ml
+++ b/src/bencode/Sidekick_bencode.ml
@@ -45,7 +45,7 @@ end
 module Decode = struct
   exception Fail
 
-  let of_string ?(idx = 0) s =
+  let of_string ?(idx = 0) s : (int * _) option =
     let i = ref idx in
 
     let[@inline] check_not_eof () =
@@ -111,7 +111,11 @@ module Decode = struct
         read_map (Util.Str_map.add k v acc)
     in
 
-    try Some (top ()) with Fail -> None
+    try
+      let v = top () in
+      let len = !i - idx in
+      Some (len, v)
+    with Fail -> None
 
   let of_string_exn ?idx s =
     match of_string ?idx s with
diff --git a/src/bencode/Sidekick_bencode.mli b/src/bencode/Sidekick_bencode.mli
index 4b521156..8ab4e6c0 100644
--- a/src/bencode/Sidekick_bencode.mli
+++ b/src/bencode/Sidekick_bencode.mli
@@ -6,11 +6,11 @@ module Encode : sig
 end
 
 module Decode : sig
-  val of_string : ?idx:int -> string -> t option
-  (** Decode string.
-    @param idx initial index (default 0) *)
+  val of_string : ?idx:int -> string -> (int * t) option
+  (** Decode string, and also return how  many bytes were consumed.
+      @param idx initial index (default 0) *)
 
-  val of_string_exn : ?idx:int -> string -> t
+  val of_string_exn : ?idx:int -> string -> int * t
   (** Parse string.
       @raise Error.Error if the string is not valid bencode. *)
 end
diff --git a/src/core/t_tracer.ml b/src/core/t_tracer.ml
index 4b935ef4..cb9738e8 100644
--- a/src/core/t_tracer.ml
+++ b/src/core/t_tracer.ml
@@ -55,13 +55,23 @@ let emit_term_ (self : state) (t : Term.t) =
   in
   loop t
 
+class type t =
+  object
+    method emit_term : Term.t -> term_ref
+  end
+
+class dummy : t =
+  object
+    method emit_term _ = Tr.Entry_id.dummy
+  end
+
 (* tracer *)
-class t ~sink =
+class concrete ~sink : t =
   object
     val state = { sink; emitted = T.Weak_map.create 16 }
     method emit_term (t : Term.t) : term_ref = emit_term_ state t
   end
 
-let create ~sink () : t = new t ~sink
+let create ~sink () : t = new concrete ~sink
 let emit (self : #t) (t : T.t) : term_ref = self#emit_term t
 let emit' self t : unit = ignore (emit self t : term_ref)
diff --git a/src/core/t_tracer.mli b/src/core/t_tracer.mli
index 300cb7c2..7e64c75f 100644
--- a/src/core/t_tracer.mli
+++ b/src/core/t_tracer.mli
@@ -22,11 +22,20 @@ type Tr.entry_view +=
   (* FIXME: remove *)
   [@@ocaml.warning "-38"]
 
-class t :
-  sink:Tr.Sink.t
-  -> object
-       method emit_term : Term.t -> term_ref
-     end
+class type t =
+  object
+    method emit_term : Term.t -> term_ref
+  end
+
+(** Dummy implementation, returns {!Tr.Entry_id.dummy} *)
+class dummy :
+  object
+    inherit t
+    method emit_term : Term.t -> term_ref
+  end
+
+class concrete : sink:Tr.Sink.t -> t
+(** Concrete implementation of [t] *)
 
 val create : sink:Tr.Sink.t -> unit -> t
 (** [create ~sink ()] makes a tracer that will write terms
diff --git a/src/main/dune b/src/main/dune
index 8a7a3d55..7b2db52b 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -4,8 +4,16 @@
  (name main)
  (public_name sidekick)
  (package sidekick-bin)
+ (modules main pure_sat_solver)
  (modes native)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
    sidekick.smt-solver sidekick-bin.smtlib sidekick.tef sidekick.drup
    sidekick.memtrace sidekick-bin.lib)
  (flags :standard -safe-string -color always -open Sidekick_util))
+
+(executable
+ (name show_trace)
+ (modules show_trace)
+ (modes native)
+ (libraries containers sidekick.util sidekick.core sidekick.trace)
+ (flags :standard -safe-string -color always -open Sidekick_util))
diff --git a/src/main/main.ml b/src/main/main.ml
index 87ce53d0..9a897a43 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -22,6 +22,7 @@ let file = ref ""
 let p_cnf = ref false
 let p_proof = ref false
 let p_model = ref false
+let file_trace = ref ""
 let check = ref false
 let time_limit = ref 300.
 let mem_limit = ref 1_000_000_000.
@@ -90,6 +91,7 @@ let argspec =
         " store temporary proof in given file (no cleanup)" );
       "-o", Arg.Set_string proof_file, " file into which to output a proof";
       "--model", Arg.Set p_model, " print model";
+      "--trace", Arg.Set_string file_trace, " emit trace into <file>";
       "--no-model", Arg.Clear p_model, " do not print model";
       ( "--bool",
         Arg.Symbol
@@ -133,6 +135,15 @@ let check_limits () =
   else if s > !mem_limit then
     raise Out_of_space
 
+let mk_tracer () =
+  if !file_trace = "" then
+    Sidekick_smt_solver.Tracer.dummy
+  else (
+    let oc = open_out_bin !file_trace in
+    Sidekick_smt_solver.Tracer.concrete
+      ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc)
+  )
+
 let main_smt ~config () : _ result =
   let tst = Term.Store.create ~size:4_096 () in
 
@@ -169,6 +180,7 @@ let main_smt ~config () : _ result =
      let proof = Proof.create ~config () in
   *)
   let proof = Proof.dummy in
+  let tracer = mk_tracer () in
 
   let solver =
     (* TODO: probes, to load only required theories *)
@@ -179,7 +191,7 @@ let main_smt ~config () : _ result =
             (Sidekick_smt_solver.Theory.name th_bool));
       [ th_bool; Process.th_ty_unin; Process.th_data; Process.th_lra ]
     in
-    Process.Solver.create_default ~proof ~theories tst
+    Process.Solver.create_default ~tracer ~proof ~theories tst
   in
 
   let finally () =
@@ -238,6 +250,7 @@ let main_cnf () : _ result =
   in
   CCFun.protect ~finally @@ fun () ->
   let tst = Term.Store.create () in
+  (* FIXME :tracer? *)
   let solver = S.SAT.create_pure_sat ~size:`Big ~proof ~stat () in
 
   S.Dimacs.parse_file solver tst !file >>= fun () ->
diff --git a/src/main/pure_sat_solver.ml b/src/main/pure_sat_solver.ml
index c7e72dc5..3bee156c 100644
--- a/src/main/pure_sat_solver.ml
+++ b/src/main/pure_sat_solver.ml
@@ -1,6 +1,7 @@
 (* pure SAT solver *)
 
 open Sidekick_core
+module Tracer = Sidekick_smt_solver.Tracer
 module E = CCResult
 module SS = Sidekick_sat
 
diff --git a/src/main/show_trace.ml b/src/main/show_trace.ml
new file mode 100644
index 00000000..0d941371
--- /dev/null
+++ b/src/main/show_trace.ml
@@ -0,0 +1,21 @@
+open Sidekick_trace
+
+let show_file file : unit =
+  Log.debugf 1 (fun k -> k "(@[show-file %S@])" file);
+  let src = Source.of_string_using_bencode @@ CCIO.File.read_exn file in
+  Source.iter_all src (fun i ~tag v ->
+      Format.printf "[%d]: %S %a@." i tag Sidekick_util.Ser_value.pp v)
+
+let () =
+  let files = ref [] in
+  let opts =
+    [
+      ( "--bt",
+        Arg.Unit (fun () -> Printexc.record_backtrace true),
+        " enable backtraces" );
+    ]
+    |> Arg.align
+  in
+  Arg.parse opts (fun f -> files := f :: !files) "show_trace [file]+";
+  let files = List.rev !files in
+  List.iter show_file files
diff --git a/src/smt/solver.ml b/src/smt/solver.ml
index 673a3dc4..bc38b854 100644
--- a/src/smt/solver.ml
+++ b/src/smt/solver.ml
@@ -40,6 +40,7 @@ type t = {
   mutable last_res: res option;
   stat: Stat.t;
   proof: P.t;
+  tracer: Tracer.t; [@ocaml.warn "-69"]
   theory_id_gen: Theory_id.state;
   n_clause_input: int Stat.counter;
   n_clause_internal: int Stat.counter;
@@ -71,13 +72,15 @@ let add_theory (self : t) (th : theory) : unit =
 let add_theory_l self = List.iter (add_theory self)
 
 (* create a new solver *)
-let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
+let create arg ?(stat = Stat.global) ?size ?(tracer = Tracer.dummy) ~proof
+    ~theories tst () : t =
   Log.debug 5 "smt-solver.create";
-  let si = Solver_internal.create arg ~stat ~proof tst () in
+  let si = Solver_internal.create arg ~tracer ~stat ~proof tst () in
   let self =
     {
       si;
       proof;
+      tracer;
       last_res = None;
       solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si);
       stat;
@@ -101,8 +104,8 @@ let default_arg =
     let view_as_cc = Default_cc_view.view_as_cc
   end : ARG)
 
-let create_default ?stat ?size ~proof ~theories tst () : t =
-  create default_arg ?stat ?size ~proof ~theories tst ()
+let create_default ?stat ?size ?tracer ~proof ~theories tst () : t =
+  create default_arg ?stat ?size ?tracer ~proof ~theories tst ()
 
 let[@inline] solver self = self.solver
 let[@inline] stats self = self.stat
@@ -155,6 +158,7 @@ end)
 
 let add_clause (self : t) (c : lit array) (proof : step_id) : unit =
   let c, proof = preprocess_clause_ self c proof in
+  Tracer.assert_clause_arr' self.tracer c;
   add_clause_nopreproc_ ~internal:false self c proof;
   Perform_delayed_.top self.si self;
   (* finish preproc *)
diff --git a/src/smt/solver.mli b/src/smt/solver.mli
index 41024d78..7a26b32e 100644
--- a/src/smt/solver.mli
+++ b/src/smt/solver.mli
@@ -49,6 +49,7 @@ val create :
   ?stat:Stat.t ->
   ?size:[ `Big | `Tiny | `Small ] ->
   (* TODO? ?config:Config.t -> *)
+  ?tracer:Tracer.t ->
   proof:proof_trace ->
   theories:Theory.t list ->
   Term.store ->
@@ -71,6 +72,7 @@ val create_default :
   ?stat:Stat.t ->
   ?size:[ `Big | `Tiny | `Small ] ->
   (* TODO? ?config:Config.t -> *)
+  ?tracer:Tracer.t ->
   proof:proof_trace ->
   theories:Theory.t list ->
   Term.store ->
@@ -98,18 +100,18 @@ val mk_lit_t : t -> ?sign:bool -> term -> lit
 
 val add_clause : t -> lit array -> step_id -> unit
 (** [add_clause solver cs] adds a boolean clause to the solver.
-      Subsequent calls to {!solve} will need to satisfy this clause. *)
+    Subsequent calls to {!solve} will need to satisfy this clause. *)
 
 val add_clause_l : t -> lit list -> step_id -> unit
 (** Add a clause to the solver, given as a list. *)
 
 val assert_terms : t -> term list -> unit
-(** Helper that turns each term into an atom, before adding the result
-      to the solver as an assertion *)
+(** Helper that turns each term into an atom, before adding disjunction of
+    the resulting atoms to the solver as a clause assertion *)
 
 val assert_term : t -> term -> unit
 (** Helper that turns the term into an atom, before adding the result
-      to the solver as a unit clause assertion *)
+    to the solver as a unit clause assertion *)
 
 val add_ty : t -> ty -> unit
 
diff --git a/src/smt/solver_internal.ml b/src/smt/solver_internal.ml
index 6e051265..998ca25e 100644
--- a/src/smt/solver_internal.ml
+++ b/src/smt/solver_internal.ml
@@ -58,6 +58,7 @@ type t = {
   mutable level: int;
   mutable complete: bool;
   stat: Stat.t;
+  tracer: Tracer.t; [@ocaml.warning "-69"]
   count_axiom: int Stat.counter;
   count_conflict: int Stat.counter;
   count_propagate: int Stat.counter;
@@ -520,7 +521,7 @@ let add_theory_state ~st ~push_level ~pop_levels (self : t) =
   self.th_states <-
     Ths_cons { st; push_level; pop_levels; next = self.th_states }
 
-let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
+let create (module A : ARG) ~stat ~tracer ~proof (tst : Term.store) () : t =
   let simp = Simplify.create tst ~proof in
   let cc = CC.create (module A : CC.ARG) ~size:`Big tst proof in
   let preprocess = Preprocess.create ~stat ~proof ~cc ~simplify:simp tst in
@@ -530,6 +531,7 @@ let create (module A : ARG) ~stat ~proof (tst : Term.store) () : t =
       tst;
       cc;
       proof;
+      tracer;
       th_states = Ths_nil;
       stat;
       simp;
diff --git a/src/smt/solver_internal.mli b/src/smt/solver_internal.mli
index 552f577c..a6226aa7 100644
--- a/src/smt/solver_internal.mli
+++ b/src/smt/solver_internal.mli
@@ -284,4 +284,10 @@ val add_theory_state :
   unit
 
 val create :
-  (module ARG) -> stat:Stat.t -> proof:Proof_trace.t -> Term.store -> unit -> t
+  (module ARG) ->
+  stat:Stat.t ->
+  tracer:Tracer.t ->
+  proof:Proof_trace.t ->
+  Term.store ->
+  unit ->
+  t
diff --git a/src/smt/tracer.ml b/src/smt/tracer.ml
index 3507cfd0..540b03a4 100644
--- a/src/smt/tracer.ml
+++ b/src/smt/tracer.ml
@@ -4,9 +4,16 @@ module V = Ser_value
 
 type Tr.entry_view += Assert of Term.t | Assert_clause of Lit.t list
 
-class t (sink : Tr.Sink.t) =
+class type t =
   object
-    inherit Term.Tracer.t ~sink as emit_t
+    inherit Term.Tracer.t
+    method emit_assert_term : Term.t -> Tr.Entry_id.t
+    method emit_assert_clause : Lit.t list -> Tr.Entry_id.t
+  end
+
+class concrete (sink : Tr.Sink.t) : t =
+  object
+    inherit Term.Tracer.concrete ~sink as emit_t
 
     method emit_assert_term t =
       let id_t = emit_t#emit_term t in
@@ -29,7 +36,17 @@ class t (sink : Tr.Sink.t) =
       id
   end
 
+class dummy : t =
+  object
+    inherit Term.Tracer.dummy
+    method emit_assert_term _ = Tr.Entry_id.dummy
+    method emit_assert_clause _ = Tr.Entry_id.dummy
+  end
+
 let assert_term (self : #t) t = self#emit_assert_term t
 let assert_term' (self : #t) t = ignore (assert_term self t : Tr.Entry_id.t)
 let assert_clause (self : #t) c = self#emit_assert_clause c
 let assert_clause' (self : #t) c = ignore (assert_clause self c : Tr.Entry_id.t)
+let assert_clause_arr' (self : #t) c = assert_clause' self (Array.to_list c)
+let dummy : #t = new dummy
+let concrete ~sink = new concrete sink
diff --git a/src/smt/tracer.mli b/src/smt/tracer.mli
index 5a065dea..bad089f2 100644
--- a/src/smt/tracer.mli
+++ b/src/smt/tracer.mli
@@ -3,19 +3,27 @@ module Tr = Sidekick_trace
 
 type Tr.entry_view += Assert of Term.t | Assert_clause of Lit.t list
 
-class t :
-  Tr.Sink.t
-  -> object
-       inherit Term.Tracer.t
+class type t =
+  object
+    inherit Term.Tracer.t
 
-       method emit_assert_term : Term.t -> Tr.Entry_id.t
-       (** Emit an assertion *)
+    method emit_assert_term : Term.t -> Tr.Entry_id.t
+    (** Emit an assertion *)
 
-       method emit_assert_clause : Lit.t list -> Tr.Entry_id.t
-       (** Emit an assertion *)
-     end
+    method emit_assert_clause : Lit.t list -> Tr.Entry_id.t
+    (** Emit an assertion *)
+  end
 
+class dummy : t
+(** Dummy tracer *)
+
+class concrete : Tr.Sink.t -> t
+(** Tracer emitting to a sink *)
+
+val dummy : t
+val concrete : sink:Tr.Sink.t -> t
 val assert_term : #t -> Term.t -> Tr.Entry_id.t
 val assert_term' : #t -> Term.t -> unit
 val assert_clause : #t -> Lit.t list -> Tr.Entry_id.t
 val assert_clause' : #t -> Lit.t list -> unit
+val assert_clause_arr' : #t -> Lit.t array -> unit
diff --git a/src/trace/entry_id.ml b/src/trace/entry_id.ml
index 0aaa9dec..baf77673 100644
--- a/src/trace/entry_id.ml
+++ b/src/trace/entry_id.ml
@@ -6,3 +6,6 @@
    increasing with time. *)
 
 include Int_id.Make ()
+
+(** Dummy id *)
+let dummy : t = of_int_unsafe (-1)
diff --git a/src/trace/sink.ml b/src/trace/sink.ml
index 948f65d7..f35544c8 100644
--- a/src/trace/sink.ml
+++ b/src/trace/sink.ml
@@ -18,6 +18,11 @@ let[@inline] emit (module Sink : S) ~tag (v : Ser_value.t) : Entry_id.t =
 let[@inline] emit' (self : t) ~tag v : unit =
   ignore (emit self ~tag v : Entry_id.t)
 
+let null : t =
+  (module struct
+    let emit ~tag:_ _ = Entry_id.dummy
+  end)
+
 let of_out_channel_using_bencode (oc : out_channel) : t =
   let id_ = ref 0 in
   let buf = Buffer.create 128 in
@@ -29,6 +34,7 @@ let of_out_channel_using_bencode (oc : out_channel) : t =
       let v' = Ser_value.(list [ int id; string tag; v ]) in
       incr id_;
       Sidekick_bencode.Encode.to_buffer buf v';
+      Buffer.add_char buf '\n';
       Buffer.output_buffer oc buf;
       Buffer.clear buf;
       id
diff --git a/src/trace/sink.mli b/src/trace/sink.mli
index 15e6091e..2cb2b7f7 100644
--- a/src/trace/sink.mli
+++ b/src/trace/sink.mli
@@ -16,6 +16,9 @@ type t = (module S)
 val emit : t -> tag:tag -> Ser_value.t -> Entry_id.t
 val emit' : t -> tag:tag -> Ser_value.t -> unit
 
+val null : t
+(** Sink that writes nowhere, just eats bytes. *)
+
 val of_out_channel_using_bencode : out_channel -> t
 (** A sink that emits entries using Bencode into the given channel *)
 
diff --git a/src/trace/source.ml b/src/trace/source.ml
index aef90071..e86815a6 100644
--- a/src/trace/source.ml
+++ b/src/trace/source.ml
@@ -19,25 +19,35 @@ let decode_bencode_entry_ =
     let+ id, tag, view = tup3 int string any in
     id, tag, view)
 
+let is_whitespace_ = function
+  | ' ' | '\t' | '\n' -> true
+  | _ -> false
+
 let of_string_using_bencode (str : string) : t =
   (module struct
     let iter_all f =
       let i = ref 0 in
       while !i < String.length str do
-        match Sidekick_bencode.Decode.of_string ~idx:!i str with
-        | None -> i := String.length str
-        | Some b ->
-          (match Ser_decode.run decode_bencode_entry_ b with
-          | Error err ->
-            Error.errorf "cannot decode string entry: %a" Ser_decode.Error.pp
-              err
-          | Ok (id, tag, v) -> f id ~tag v)
+        while !i < String.length str && is_whitespace_ str.[!i] do
+          incr i
+        done;
+        if !i < String.length str then (
+          match Sidekick_bencode.Decode.of_string ~idx:!i str with
+          | None -> i := String.length str
+          | Some (len, b) ->
+            i := !i + len;
+            (match Ser_decode.run decode_bencode_entry_ b with
+            | Error err ->
+              Error.errorf "cannot decode string entry: %a" Ser_decode.Error.pp
+                err
+            | Ok (id, tag, v) -> f id ~tag v)
+        )
       done
 
     let get_entry id : tag * Ser_value.t =
       match Sidekick_bencode.Decode.of_string str ~idx:id with
       | None -> Error.errorf "invalid offset %d" id
-      | Some b ->
+      | Some (_len, b) ->
         (match Ser_decode.run decode_bencode_entry_ b with
         | Error err ->
           Error.errorf "cannot decode string entry: %a" Ser_decode.Error.pp err