refactor: remove proof-trace infra from base to use sidekick.trace instead

src/base/proof-trace/.ocamlformat-ignore

@@ -1 +0,0 @@
-proof_ser.bare

src/base/proof-trace/Storage.ml

@@ -1,32 +0,0 @@
-module CS = Chunk_stack
-
-type t = No_store | In_memory of CS.Buf.t | On_disk of string * out_channel
-
-let pp out = function
-  | No_store -> Fmt.string out "no-store"
-  | In_memory _ -> Fmt.string out "in-memory"
-  | On_disk (file, _) -> Fmt.fprintf out "(on-file %S)" file
-
-let nop_ _ = ()
-
-let iter_chunks_ (r : CS.Reader.t) k =
-  let rec loop () =
-    CS.Reader.next r ~finish:nop_ ~yield:(fun b i _len ->
-        let step = Proof_ser.Bare.of_bytes_exn Proof_ser.Step.decode b ~off:i in
-        k step;
-        loop ())
-  in
-  loop ()
-
-let iter_steps_backward (self : t) : Proof_ser.Step.t Iter.t =
-  let module CS = Chunk_stack in
-  fun yield ->
-    match self with
-    | No_store -> ()
-    | In_memory buf ->
-      let r = CS.Reader.from_buf buf in
-      iter_chunks_ r yield
-    | On_disk (file, _oc) ->
-      let ic = open_in file in
-      let iter = CS.Reader.from_channel_backward ~close_at_end:true ic in
-      iter_chunks_ iter yield

src/base/proof-trace/Storage.mli

@@ -1,7 +0,0 @@
-type t =
-  | No_store
-  | In_memory of Chunk_stack.Buf.t
-  | On_disk of string * out_channel
-
-val pp : Format.formatter -> t -> unit
-val iter_steps_backward : t -> Proof_ser.Step.t Iter.t

src/base/proof-trace/dune

@@ -1,14 +0,0 @@
-(library
- (name sidekick_base_proof_trace)
- (public_name sidekick-base.proof-trace)
- (libraries sidekick.util)
- (flags :standard -w -32 -warn-error -a+8 -open Sidekick_util))
-
-; generate (de)ser + types from .bare file
-
-(rule
- (targets proof_ser.ml)
- (deps proof_ser.bare)
- (mode promote) ; not required in releases
- (action
-  (run bare-codegen --pp --standalone %{deps} -o %{targets})))

src/base/proof-trace/proof_ser.bare

@@ -1,149 +0,0 @@
-
-type ID i32
-type Lit ID
-
-type Clause {
-  lits: []Lit
-}
-
-type Step_input {
-  c: Clause
-}
-
-# clause, RUP with previous steps
-type Step_rup {
-  res: Clause
-  hyps: []ID
-}
-
-# TODO: remove?
-# lit <-> expr
-type Step_bridge_lit_expr {
-  lit: Lit
-  expr: ID
-}
-
-# prove congruence closure lemma `\/_{e\in eqns} e`
-type Step_cc {
-  eqns: []ID
-}
-
-# prove t=u using some previous steps and unit equations,
-# and add clause (t=u) with given ID
-type Step_preprocess {
-  t: ID
-  u: ID
-  using: []ID
-}
-
-type Step_clause_rw {
-  c: ID
-  res: Clause
-  using: []ID
-}
-
-type Step_unsat {
-  c: ID
-}
-
-# rewrite `c` with the unit clause `rw_with` of the form `t=u`  *)
-type Step_proof_p1 {
-  rw_with: ID
-  c: ID
-}
-
-# resolve `c` with the unit clause `unit` of the form `|- t`  *)
-type Step_proof_r1 {
-  unit: ID
-  c: ID
-}
-
-# resolve `c1` with `c2` on pivot `pivot` *)
-type Step_proof_res {
-  pivot: ID
-  c1: ID
-  c2: ID
-}
-
-type Step_bool_tauto {
-  lits: []Lit
-}
-
-type Step_bool_c {
-  rule: string
-  exprs: []ID
-}
-
-type Step_true {
-  true_: ID
-}
-
-type Fun_decl {
-  f: string
-}
-
-# define c := rhs
-type Expr_def {
-  c: ID
-  rhs: ID
-}
-
-type Expr_bool {
-  b: bool
-}
-
-type Expr_if {
-  cond: ID
-  then_: ID
-  else_: ID
-}
-
-type Expr_not {
-  f: ID
-}
-
-type Expr_eq {
-  lhs: ID
-  rhs: ID
-}
-
-type Expr_app {
-  f: ID
-  args: []ID
-}
-
-type Expr_isa {
-  c: ID
-  arg: ID
-}
-
-type Step_view
-  ( Step_input
-  | Step_unsat
-  | Step_rup
-  | Step_bridge_lit_expr
-  | Step_cc
-  | Step_preprocess
-  | Step_clause_rw
-  | Step_bool_tauto
-  | Step_bool_c
-  | Step_proof_p1
-  | Step_proof_r1
-  | Step_proof_res
-  | Step_true
-  | Fun_decl
-  | Expr_def
-  | Expr_bool
-  | Expr_if
-  | Expr_not
-  | Expr_isa
-  | Expr_eq
-  | Expr_app
-  )
-
-type Step {
-  id: ID
-  view: Step_view
-}
-
-

src/base/proof-trace/sidekick_base_proof_trace.ml

@@ -1,10 +0,0 @@
-(** Proof trace with serialization
-
-    This library is useful to serialize a series of reasoning steps
-    in memory or into a file, to be able to reconstruct a proper
-    proof later. *)
-
-module Proof_ser = Proof_ser
-module Storage = Storage
-
-let iter_steps_backward = Storage.iter_steps_backward

src/proof-trace-bare-dump/dune

@@ -1,5 +0,0 @@
-(executable
- (name proof_trace_dump)
- (modes native)
- (libraries containers sidekick.util sidekick-base.proof-trace)
- (flags :standard -w -32 -warn-error -a+8 -open Sidekick_util))

src/proof-trace-bare-dump/proof_trace_dump.ml

@@ -1,44 +0,0 @@
-module CS = Chunk_stack
-module Pr_trace = Sidekick_base_proof_trace
-module Proof_ser = Pr_trace.Proof_ser
-
-let file = ref ""
-let quiet = ref false
-
-let parse_file () : unit =
-  Log.debugf 2 (fun k -> k "parsing file %S" !file);
-
-  CS.Reader.with_file_backward !file @@ fun reader ->
-  (* TODO: use the storage module function
-     Pr_trace.iter_steps_backward (Pr_trace.Storage.
-  *)
-  let n = ref 0 in
-  let rec display_steps () =
-    CS.Reader.next reader
-      ~finish:(fun () -> ())
-      ~yield:(fun b i _len ->
-        let decode = Proof_ser.Bare.Decode.of_bytes b ~off:i in
-        let step = Proof_ser.Step.decode decode in
-        incr n;
-        if not !quiet then Format.printf "@[<2>%a@]@." Proof_ser.Step.pp step;
-        display_steps ())
-  in
-  display_steps ();
-  Format.printf "read %d steps@." !n;
-  ()
-
-let () =
-  let opts =
-    [
-      ( "--bt",
-        Arg.Unit (fun () -> Printexc.record_backtrace true),
-        " enable stack traces" );
-      "-d", Arg.Int Log.set_debug, "<lvl> sets the debug verbose level";
-      "-q", Arg.Set quiet, " quiet: do not print steps";
-    ]
-    |> Arg.align
-  in
-  Arg.parse opts (fun f -> file := f) "proof-trace-dump <file>";
-  if !file = "" then failwith "please provide a file";
-
-  parse_file ()

src/proof-trace/.ocamlformat-ignore

@@ -1 +0,0 @@
-proof_ser.ml

src/sat/tracer.ml

@@ -0,0 +1,31 @@
+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
+
+class 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 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 =
+  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/sat/tracer.mli

@@ -0,0 +1,24 @@
+(** 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
+
+class dummy : t
+
+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/trace/entry_view.ml

@@ -1,6 +0,0 @@
-
-
-type t = ..
-(** Extensible type, each entry uses its own.
-
-   See {!Entry.t}. *)