smt tracer is now a clause tracer

src/core/clause_tracer.ml

@@ -8,7 +8,7 @@ class type t =
     method encode_lit : Lit.t -> Ser_value.t
   end
 
-let dummy : t =
+class dummy : t =
   object
     method assert_clause ~id:_ _ = Tr.Entry_id.dummy
     method delete_clause ~id:_ _ = ()
@@ -16,6 +16,7 @@ let dummy : t =
     method encode_lit _ = Ser_value.null
   end
 
+let dummy : t = new dummy
 let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c
 
 let assert_clause' (self : #t) ~id c : unit =

src/core/clause_tracer.mli

@@ -11,6 +11,8 @@ class type t =
     method encode_lit : Lit.t -> Ser_value.t
   end
 
+class dummy : t
+
 val dummy : t
 (** Dummy tracer, recording nothing. *)
 

src/main/main.ml

@@ -141,8 +141,9 @@ let mk_smt_tracer () =
     Sidekick_smt_solver.Tracer.dummy
   else (
     let oc = open_out_bin !file_trace in
-    Sidekick_smt_solver.Tracer.concrete
+    Sidekick_smt_solver.Tracer.make
       ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc)
+      ()
   )
 
 let mk_sat_tracer () : Clause_tracer.t =

src/smt/solver.ml

@@ -82,7 +82,8 @@ let create arg ?(stat = Stat.global) ?size ?(tracer = Tracer.dummy) ~proof
       proof;
       tracer;
       last_res = None;
-      solver = Sat_solver.create ~proof ?size ~stat (SI.to_sat_plugin si);
+      solver =
+        Sat_solver.create ~proof ?size ~tracer ~stat (SI.to_sat_plugin si);
       stat;
       theory_id_gen = Theory_id.create ();
       n_clause_input = Stat.mk_int stat "smt.solver.add-clause.input";
@@ -158,7 +159,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;
+  Tracer.assert_clause' self.tracer ~id:0 (Iter.of_array c);
   add_clause_nopreproc_ ~internal:false self c proof;
   Perform_delayed_.top self.si self;
   (* finish preproc *)

src/smt/trace_reader.ml

@@ -1,12 +1,12 @@
 open Sidekick_core
 module Tr = Sidekick_trace
 
-type entry = Assert of Term.t | Assert_clause of Lit.t list
+type entry = Assert of Term.t | Assert_clause of { id: int; c: Lit.t list }
 
 let pp_entry out = function
   | Assert t -> Fmt.fprintf out "(@[assert@ %a@])" Term.pp t
-  | Assert_clause c ->
-    Fmt.fprintf out "(@[assert-c@ %a@])" (Fmt.Dump.list Lit.pp) c
+  | Assert_clause { id; c } ->
+    Fmt.fprintf out "(@[assert-c[%d]@ %a@])" id (Fmt.Dump.list Lit.pp) c
 
 type t = { tst: Term.store; src: Tr.Source.t; t_dec: Term.Trace_reader.t }
 
@@ -14,7 +14,8 @@ let create ?const_decoders tst src : t =
   let t_dec = Term.Trace_reader.create ?const_decoders tst ~source:src in
   { tst; src; t_dec }
 
-let add_const_decoders self c = Term.Trace_reader.add_const_decoders self.t_dec c
+let add_const_decoders self c =
+  Term.Trace_reader.add_const_decoders self.t_dec c
 
 let dec_t (self : t) =
   Ser_decode.(
@@ -27,7 +28,8 @@ let dec_c (self : t) =
       let+ b, t = tup2 bool @@ dec_t self in
       Lit.atom self.tst ~sign:b t
     in
-    list dec_lit)
+    let+ id = dict_field "id" int and+ c = dict_field "c" (list dec_lit) in
+    id, c)
 
 let decode (self : t) ~tag v =
   Log.debugf 30 (fun k ->
@@ -43,7 +45,7 @@ let decode (self : t) ~tag v =
   | "AssC" ->
     Ser_decode.(
       (match run (dec_c self) v with
-      | Ok c -> Some (Assert_clause c)
+      | Ok (id, c) -> Some (Assert_clause { id; c })
       | Error err ->
         Fmt.eprintf "cannot decode entry with tag %S:@ %a@." tag
           Ser_decode.Error.pp err;

src/smt/trace_reader.mli

@@ -3,7 +3,7 @@
 open Sidekick_core
 module Tr = Sidekick_trace
 
-type entry = Assert of Term.t | Assert_clause of Lit.t list
+type entry = Assert of Term.t | Assert_clause of { id: int; c: Lit.t list }
 
 val pp_entry : entry Fmt.printer
 

src/smt/tracer.ml

@@ -6,11 +6,12 @@ class type t =
   object
     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
+    inherit Clause_tracer.t
+    method emit_assert_term : Term.t -> Tr.Entry_id.t
   end
 
 class concrete (sink : Tr.Sink.t) : t =
-  object
+  object (self)
     inherit Term.Tracer.concrete ~sink as emit_t
 
     method emit_assert_term t =
@@ -19,32 +20,47 @@ class concrete (sink : Tr.Sink.t) : t =
       let id = Tr.Sink.emit sink ~tag:"AssT" v in
       id
 
-    method emit_assert_clause (c : Lit.t list) =
+    method encode_lit (lit : Lit.t) : V.t =
+      let sign = Lit.sign lit in
+      let id_t = emit_t#emit_term @@ Lit.term lit in
+      V.(list [ bool sign; int id_t ])
+
+    method assert_clause ~id (c : Lit.t Iter.t) =
       (* get a list of pairs *)
-      let l =
-        List.map
-          (fun lit ->
-            let sign = Lit.sign lit in
-            let id_t = emit_t#emit_term @@ Lit.term lit in
-            V.(list [ bool sign; int id_t ]))
-          c
-        |> V.list
-      in
-      let id = Tr.Sink.emit sink ~tag:"AssC" l in
+      let l = Iter.map self#encode_lit c |> Iter.to_rev_list |> V.list in
+      let v = V.(dict_of_list [ "id", int id; "c", l ]) in
+      let id = Tr.Sink.emit sink ~tag:"AssC" v in
       id
+
+    method unsat_clause ~id =
+      let v = Ser_value.(dict_of_list [ "id", int id ]) in
+      Tr.Sink.emit sink ~tag:"UnsatC" v
+
+    method delete_clause ~id _lits : unit =
+      let v = Ser_value.(dict_of_list [ "id", int id ]) in
+      ignore (Tr.Sink.emit sink ~tag:"DelCSat" v : Tr.Entry_id.t)
   end
 
 class dummy : t =
   object
     inherit Term.Tracer.dummy
+    inherit Clause_tracer.dummy
     method emit_assert_term _ = Tr.Entry_id.dummy
-    method emit_assert_clause _ = Tr.Entry_id.dummy
   end
 
+let dummy : #t = new dummy
+let make ~sink () = new concrete sink
+let assert_clause (self : #t) ~id c : Tr.Entry_id.t = self#assert_clause ~id c
+
+let assert_clause' (self : #t) ~id c : unit =
+  ignore (self#assert_clause ~id c : Tr.Entry_id.t)
+
+let unsat_clause (self : #t) ~id : Tr.Entry_id.t = self#unsat_clause ~id
+
+let unsat_clause' (self : #t) ~id : unit =
+  ignore (self#unsat_clause ~id : Tr.Entry_id.t)
+
+let delete_clause (self : #t) ~id c = self#delete_clause ~id c
+let encode_lit (self : #t) lit = self#encode_lit lit
 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

src/smt/tracer.mli

@@ -4,12 +4,10 @@ module Tr = Sidekick_trace
 class type t =
   object
     inherit Term.Tracer.t
+    inherit Clause_tracer.t
 
     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
 
 class dummy : t
@@ -19,9 +17,12 @@ class concrete : Tr.Sink.t -> t
 (** Tracer emitting to a sink *)
 
 val dummy : t
-val concrete : sink:Tr.Sink.t -> t
+val make : sink:Tr.Sink.t -> unit -> 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
+val assert_clause : #t -> id:int -> Lit.t Iter.t -> Tr.Entry_id.t
+val assert_clause' : #t -> id:int -> Lit.t Iter.t -> unit
+val delete_clause : #t -> id:int -> Lit.t Iter.t -> unit
+val unsat_clause : #t -> id:int -> Tr.Entry_id.t
+val unsat_clause' : #t -> id:int -> unit
+val encode_lit : #t -> Lit.t -> Ser_value.t