feat: add Clause_tracer, works both for SMT and SAT

src/core/Sidekick_core.ml

@@ -46,5 +46,6 @@ module Proof_term = Proof_term
 module Subst = Sidekick_core_logic.Subst
 module Var = Sidekick_core_logic.Var
 module Box = Box
+module Clause_tracer = Clause_tracer
 
 exception Resource_exhausted

src/core/clause_tracer.ml

@@ -0,0 +1,30 @@
+module Tr = Sidekick_trace
+
+class type t =
+  object
+    method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
+    method delete_clause : id:int -> Lit.t Iter.t -> unit
+    method unsat_clause : id:int -> Tr.Entry_id.t
+    method encode_lit : Lit.t -> Ser_value.t
+  end
+
+let dummy : t =
+  object
+    method assert_clause ~id:_ _ = Tr.Entry_id.dummy
+    method delete_clause ~id:_ _ = ()
+    method unsat_clause ~id:_ = Tr.Entry_id.dummy
+    method encode_lit _ = Ser_value.null
+  end
+
+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

src/core/clause_tracer.mli

@@ -0,0 +1,22 @@
+(** Tracer for clauses and literals *)
+
+module Tr = Sidekick_trace
+
+(** Tracer for clauses. *)
+class type t =
+  object
+    method assert_clause : id:int -> Lit.t Iter.t -> Tr.Entry_id.t
+    method delete_clause : id:int -> Lit.t Iter.t -> unit
+    method unsat_clause : id:int -> Tr.Entry_id.t
+    method encode_lit : Lit.t -> Ser_value.t
+  end
+
+val dummy : t
+(** Dummy tracer, recording nothing. *)
+
+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

src/main/main.ml

@@ -4,6 +4,7 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+open Sidekick_core
 module E = CCResult
 module Fmt = CCFormat
 module Term = Sidekick_base.Term
@@ -135,7 +136,7 @@ let check_limits () =
   else if s > !mem_limit then
     raise Out_of_space
 
-let mk_tracer () =
+let mk_smt_tracer () =
   if !file_trace = "" then
     Sidekick_smt_solver.Tracer.dummy
   else (
@@ -144,6 +145,15 @@ let mk_tracer () =
       ~sink:(Sidekick_trace.Sink.of_out_channel_using_bencode oc)
   )
 
+let mk_sat_tracer () : Clause_tracer.t =
+  if !file_trace = "" then
+    Clause_tracer.dummy
+  else (
+    let oc = open_out_bin !file_trace in
+    let sink = Sidekick_trace.Sink.of_out_channel_using_bencode oc in
+    Pure_sat_solver.tracer ~sink ()
+  )
+
 let main_smt ~config () : _ result =
   let tst = Term.Store.create ~size:4_096 () in
 
@@ -180,7 +190,7 @@ let main_smt ~config () : _ result =
      let proof = Proof.create ~config () in
   *)
   let proof = Proof.dummy in
-  let tracer = mk_tracer () in
+  let tracer = mk_smt_tracer () in
 
   let solver =
     (* TODO: probes, to load only required theories *)
@@ -250,8 +260,8 @@ 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
+  let tracer = mk_sat_tracer () in
+  let solver = S.SAT.create_pure_sat ~size:`Big ~tracer ~proof ~stat () in
 
   S.Dimacs.parse_file solver tst !file >>= fun () ->
   let r = S.solve ~check:!check ?in_memory_proof solver in

src/main/pure_sat_solver.ml

@@ -1,11 +1,13 @@
 (* pure SAT solver *)
 
 open Sidekick_core
-module Tracer = Sidekick_smt_solver.Tracer
 module E = CCResult
 module SS = Sidekick_sat
+module Tr = Sidekick_trace
 
 module I_const : sig
+  type Const.view += I of int
+
   val make : Term.store -> int -> Lit.t
   val const_decoders : Const.decoders
 end = struct
@@ -77,6 +79,42 @@ module Dimacs = struct
     with e -> E.of_exn_trace e
 end
 
+(** Tracer that emit list of integers. *)
+let tracer ~(sink : Tr.Sink.t) () : Clause_tracer.t =
+  object (self)
+    method encode_lit (lit : Lit.t) =
+      let sign = Lit.sign lit in
+      let i =
+        match Term.view (Lit.term lit) with
+        | Term.E_const { Const.c_view = I_const.I i; _ } -> abs i
+        | _ -> assert false
+      in
+      Ser_value.int
+        (if sign then
+          i
+        else
+          -i)
+
+    method assert_clause ~id (lits : Lit.t Iter.t) =
+      let v =
+        Ser_value.(
+          dict_of_list
+            [
+              "id", int id;
+              "c", list (lits |> Iter.map self#encode_lit |> Iter.to_rev_list);
+            ])
+      in
+      Tr.Sink.emit sink ~tag:"AssCSat" v
+
+    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
+
 (* FIXME
    let check_proof (proof : Proof.in_memory) : bool =
      Profile.with_ "pure-sat.check-proof" @@ fun () ->

src/main/show_trace.ml

@@ -2,6 +2,57 @@ open Sidekick_core
 open Sidekick_trace
 module Smt = Sidekick_smt_solver
 
+type state = { dump: bool; src: Source.t; t_reader: Smt.Trace_reader.t }
+
+let show_sat (_self : state) ~tag v : unit =
+  match tag with
+  | "AssCSat" ->
+    (match
+       Ser_decode.(
+         let d =
+           let+ id = dict_field "id" int and+ c = dict_field "c" (list int) in
+           id, c
+         in
+         run d v)
+     with
+    | Ok (id, c) -> Fmt.printf "[%d]: %a@." id Fmt.Dump.(list int) c
+    | Error _ -> ())
+  | "DelCSat" ->
+    (match
+       Ser_decode.(
+         let d =
+           let+ id = dict_field "id" int in
+           id
+         in
+         run d v)
+     with
+    | Ok id -> Fmt.printf "del [%d]@." id
+    | Error _ -> ())
+  | "UnsatC" ->
+    (match
+       Ser_decode.(
+         let d =
+           let+ id = dict_field "id" int in
+           id
+         in
+         run d v)
+     with
+    | Ok id -> Fmt.printf "unsat [%d]@." id
+    | Error _ -> ())
+  | _ -> ()
+
+let show_event (self : state) i ~tag v : unit =
+  Log.debugf 10 (fun k ->
+      k "(@[show-trace[%d]@ :tag %S@ :val %a@])" i tag Ser_value.pp v);
+  if self.dump then Format.printf "[%d]: %S %a@." i tag Ser_value.pp v;
+
+  (match Smt.Trace_reader.decode self.t_reader ~tag v with
+  | Some e -> Fmt.printf "[%d]: %a@." i Smt.Trace_reader.pp_entry e
+  | None -> ());
+
+  show_sat self ~tag v;
+  ()
+
 let show_file ~dump 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
@@ -16,14 +67,8 @@ let show_file ~dump file : unit =
         ]
   in
 
-  Source.iter_all src (fun i ~tag v ->
-      Log.debugf 10 (fun k ->
-          k "(@[show-trace[%d]@ :tag %S@ :val %a@])" i tag Ser_value.pp v);
-      if dump then Format.printf "[%d]: %S %a@." i tag Ser_value.pp v;
-
-      match Smt.Trace_reader.decode t_reader ~tag v with
-      | Some e -> Fmt.printf "[%d]: %a@." i Smt.Trace_reader.pp_entry e
-      | None -> ())
+  let st = { t_reader; src; dump } in
+  Source.iter_all src (fun i ~tag v -> show_event st i ~tag v)
 
 let () =
   let files = ref [] in

src/sat/solver.ml

@@ -244,6 +244,7 @@ type t = {
   store: store; (* atom/var/clause store *)
   plugin: plugin; (* user defined theory *)
   proof: Proof_trace.t; (* the proof object *)
+  tracer: Clause_tracer.t;
   (* Clauses are simplified for efficiency purposes. In the following
      vectors, the comments actually refer to the original non-simplified
      clause. *)
@@ -306,10 +307,12 @@ let restart_first = 100
 let _nop_on_conflict (_ : atom array) = ()
 
 (* Starting environment. *)
-let create_ ~store ~proof ~stat ~max_clauses_learnt (plugin : plugin) : t =
+let create_ ~store ~proof ~tracer ~stat ~max_clauses_learnt (plugin : plugin) :
+    t =
   {
     store;
     plugin;
+    tracer;
     unsat_at_0 = None;
     next_decisions = [];
     max_clauses_learnt;
@@ -677,6 +680,8 @@ let report_unsat self (us : unsat_cause) : _ =
       Event.emit self.on_learnt c;
       let p = Clause.proof_step self.store c in
       Proof_trace.add_unsat self.proof p;
+      Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int c) Iter.empty;
+      Clause_tracer.unsat_clause' self.tracer ~id:(Clause.to_int c);
       US_false c
     | US_local _ -> us
   in
@@ -1018,6 +1023,8 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit =
       Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps)
     in
     let uclause = Clause.make_a store ~removable:true cr.cr_learnt p in
+    Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int uclause)
+      (Clause.lits_iter store uclause);
     Event.emit self.on_learnt uclause;
 
     if Atom.is_false store fuip then
@@ -1034,6 +1041,8 @@ let record_learnt_clause (self : t) ~pool (cr : conflict_res) : unit =
       Proof_sat.sat_redundant_clause lits ~hyps:(Step_vec.to_iter cr.cr_steps)
     in
     let lclause = Clause.make_a store ~removable:true cr.cr_learnt p in
+    Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int lclause)
+      (Clause.lits_iter store lclause);
 
     add_clause_to_vec_ ~pool self lclause;
     attach_clause self lclause;
@@ -1071,6 +1080,8 @@ let add_clause_ (self : t) ~pool (init : clause) : unit =
   let store = self.store in
   Log.debugf 30 (fun k ->
       k "(@[sat.add-clause@ @[<hov>%a@]@])" (Clause.debug store) init);
+  Clause_tracer.assert_clause' self.tracer ~id:(Clause.to_int init)
+    (Clause.lits_iter store init);
   (* Insertion of new lits is done before simplification. Indeed, else a lit in a
      trivial clause could end up being not decided on, which is a bug. *)
   Clause.iter store init ~f:(fun x -> insert_var_order self (Atom.var x));
@@ -1530,6 +1541,8 @@ let reduce_clause_db (self : t) : unit =
     (* need to remove from watchlists *)
     mark_dirty_atom (Atom.neg atoms.(1));
     Event.emit self.on_gc (Clause.lits_a store c);
+    Clause_tracer.delete_clause self.tracer ~id:(Clause.to_int c)
+      (Clause.lits_iter store c);
     Proof_trace.delete self.proof (Clause.proof_step store c)
   in
 
@@ -1647,7 +1660,7 @@ let search (self : t) ~on_progress ~(max_conflicts : int) : unit =
     | Some confl ->
       (* Conflict *)
       incr n_conflicts;
-      (* When the theory has raised Unsat, add_boolean_conflict
+      (* When the theory has raised Unsat, [add_boolean_conflict]
          might 'forget' the initial conflict clause, and only add the
          analyzed backtrack clause. So in those case, we use add_clause
          to make sure the initial conflict clause is also added. *)
@@ -2034,10 +2047,15 @@ let[@inline] eval_lit self (lit : Lit.t) : lbool =
   | Some a -> eval_atom_ self a
   | None -> L_undefined
 
-let create ?(stat = Stat.global) ?(size = `Big) ~proof (p : plugin) : t =
+let create ?(stat = Stat.global) ?(size = `Big) ?tracer ~proof (p : plugin) : t
+    =
+  let tracer =
+    (tracer : #Clause_tracer.t option :> Clause_tracer.t option)
+    |> Option.value ~default:Clause_tracer.dummy
+  in
   let store = Store.create ~size ~stat () in
   let max_clauses_learnt = ref 0 in
-  let self = create_ ~max_clauses_learnt ~store ~proof ~stat p in
+  let self = create_ ~max_clauses_learnt ~store ~tracer ~proof ~stat p in
   self
 
 let plugin_cdcl_t (module P : THEORY_CDCL_T) : (module PLUGIN) =
@@ -2066,5 +2084,5 @@ let plugin_pure_sat : plugin =
     let has_theory = false
   end)
 
-let create_pure_sat ?stat ?size ~proof () : t =
-  create ?stat ?size ~proof plugin_pure_sat
+let create_pure_sat ?stat ?size ?tracer ~proof () : t =
+  create ?stat ?size ?tracer ~proof plugin_pure_sat

src/sat/solver.mli

@@ -176,6 +176,7 @@ val mk_plugin_cdcl_t :
 val create :
   ?stat:Stat.t ->
   ?size:[ `Tiny | `Small | `Big ] ->
+  ?tracer:#Clause_tracer.t ->
   proof:Proof_trace.t ->
   plugin ->
   t
@@ -190,6 +191,7 @@ val plugin_pure_sat : plugin
 val create_pure_sat :
   ?stat:Stat.t ->
   ?size:[ `Tiny | `Small | `Big ] ->
+  ?tracer:#Clause_tracer.t ->
   proof:Proof_trace.t ->
   unit ->
   t