wip: Tracer for SMT

src/smt/Sidekick_smt_solver.ml

@@ -16,6 +16,7 @@ module Theory = Theory
 module Theory_id = Theory_id
 module Preprocess = Preprocess
 module Find_foreign = Find_foreign
+module Tracer = Tracer
 
 type theory = Theory.t
 type solver = Solver.t

src/smt/dune

@@ -3,5 +3,5 @@
  (public_name sidekick.smt-solver)
  (synopsis "main SMT solver")
  (libraries containers iter sidekick.core sidekick.util sidekick.cc
-   sidekick.sat sidekick.simplify sidekick.model)
+   sidekick.sat sidekick.simplify sidekick.model sidekick.trace)
  (flags :standard -w +32 -open Sidekick_util))

src/smt/tracer.ml

@@ -0,0 +1,35 @@
+open Sidekick_core
+module Tr = Sidekick_trace
+module V = Ser_value
+
+type Tr.entry_view += Assert of Term.t | Assert_clause of Lit.t list
+
+class t (sink : Tr.Sink.t) =
+  object
+    inherit Term.Tracer.t ~sink as emit_t
+
+    method emit_assert_term t =
+      let id_t = emit_t#emit_term t in
+      let v = V.int id_t in
+      let id = Tr.Sink.emit sink ~tag:"AssT" v in
+      id
+
+    method emit_assert_clause (c : Lit.t list) =
+      (* 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
+      id
+  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)

src/smt/tracer.mli

@@ -0,0 +1,21 @@
+open Sidekick_core
+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
+
+       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
+
+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

src/trace/sidekick_trace.ml

@@ -19,7 +19,6 @@
 (** {2 Exports} *)
 
 module Entry_view = Entry_view
-module Entry_read = Entry_read
 module Sink = Sink
 module Source = Source
 module Entry_id = Entry_id