Merge pull request #16 from c-cube/wip-proof-smt

wip: proofs for SMT

.github/workflows/main.yml

@@ -14,8 +14,7 @@ jobs:
           - windows-latest
             #- macos-latest  # clogs CI
         ocaml-compiler:
-          - 4.04.x
-          - 4.10.x
+          - 4.08.x
           - 4.12.x
     runs-on: ${{ matrix.os }}
     steps:
@@ -26,6 +25,6 @@ jobs:
     - run: opam pin -n .
     - run: opam depext -yt sidekick sidekick-base sidekick-bin
     - run: opam install -t . --deps-only
-    - run: opam exec -- dune build
-    - run: opam exec -- dune runtest
+    - run: opam exec -- dune build --ignore-promoted-rules
+    - run: opam exec -- dune runtest --ignore-promoted-rules
       if: ${{ matrix.os == 'ubuntu-latest'}}

doc/guide.md

@@ -196,7 +196,7 @@ A list of theories can be added initially, or later using
 `Solver.add_theory`.
 
 ```ocaml
-# let solver = Solver.create ~theories:[th_bool] ~proof:(Proof_stub.create()) tstore () ();;
+# let solver = Solver.create ~theories:[th_bool] ~proof:(Proof.empty) tstore () ();;
 val solver : Solver.t = <abstr>
 
 # Solver.add_theory;;
@@ -238,7 +238,7 @@ whether the assertions and hypotheses are satisfiable together.
                   Solver.mk_lit_t solver q ~sign:false];;
 - : Solver.res =
 Sidekick_base_solver.Solver.Unsat
- {Sidekick_base_solver.Solver.unsat_core = <fun>}
+ {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>}
 ```
 
 Here it's unsat, because we asserted "p = q", and then assumed "p"
@@ -295,7 +295,7 @@ val q_imp_not_r : Term.t = (=> q (not r))
 # Solver.solve ~assumptions:[] solver;;
 - : Solver.res =
 Sidekick_base_solver.Solver.Unsat
- {Sidekick_base_solver.Solver.unsat_core = <fun>}
+ {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>}
 ```
 
 This time we got _unsat_ and there is no way of undoing it.
@@ -309,7 +309,7 @@ We can solve linear real arithmetic problems as well.
 Let's create a new solver and add the theory of reals to it.
 
 ```ocaml
-# let solver = Solver.create ~theories:[th_bool; th_lra] ~proof:(Proof_stub.create()) tstore () ();;
+# let solver = Solver.create ~theories:[th_bool; th_lra] ~proof:(Proof.empty) tstore () ();;
 val solver : Solver.t = <abstr>
 ```
 
@@ -356,10 +356,10 @@ val b_leq_half : Term.t = (<= b 1/2)
                   Solver.mk_lit_t solver b_leq_half];;
 val res : Solver.res =
   Sidekick_base_solver.Solver.Unsat
-   {Sidekick_base_solver.Solver.unsat_core = <fun>}
+   {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>}
 
 # match res with Solver.Unsat {unsat_core=us; _} -> us() |> Iter.to_list | _ -> assert false;;
-- : Proof_stub.lit list = [(a >= 1); (b <= 1/2)]
+- : Proof.lit list = [(a >= 1); (b <= 1/2)]
 ```
 
 This just showed that `a=1, b=1/2, a>=b` is unsatisfiable.
@@ -401,7 +401,7 @@ val f1_u1 : Term.t = (f1 u1)
 Anyway, Sidekick knows how to reason about functions.
 
 ```ocaml
-# let solver = Solver.create ~theories:[] ~proof:(Proof_stub.create()) tstore () ();;
+# let solver = Solver.create ~theories:[] ~proof:(Proof.empty) tstore () ();;
 val solver : Solver.t = <abstr>
 
 # (* helper *)
@@ -422,13 +422,13 @@ val appf1 : Term.t list -> Term.t = <fun>
     ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u1 (appf1[u1]))];;
 - : Solver.res =
 Sidekick_base_solver.Solver.Unsat
- {Sidekick_base_solver.Solver.unsat_core = <fun>}
+ {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>}
 
 # Solver.solve solver
     ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u2 u3)];;
 - : Solver.res =
 Sidekick_base_solver.Solver.Unsat
- {Sidekick_base_solver.Solver.unsat_core = <fun>}
+ {Sidekick_base_solver.Solver.unsat_core = <fun>; unsat_proof_step = <fun>}
 ```
 
 Assuming: `f1(u1)=u2, f1(u2)=u3, f1^2(u1)=u1, f1^3(u1)=u1`,

proof-trace-dump.sh

@@ -0,0 +1,2 @@
+#!/usr/bin/env sh
+exec dune exec --profile=release src/proof-trace-dump/proof_trace_dump.exe -- $@

sidekick-base.opam

@@ -14,7 +14,7 @@ depends: [
   "dune" { >= "1.1" }
   "containers" { >= "3.0" & < "4.0" }
   "iter" { >= "1.0" & < "2.0" }
-  "ocaml" { >= "4.04" }
+  "ocaml" { >= "4.08" } # for BARE, which uses Bytes functions
   "sidekick" { = version }
   "zarith" { >= "1.8" } # constraint for infix ops
   "alcotest" {with-test}

sidekick-bin.opam

@@ -19,7 +19,7 @@ depends: [
   "sidekick" { = version }
   "sidekick-base" { = version }
   "menhir"
-  "ocaml" { >= "4.04" }
+  "ocaml" { >= "4.08" }
   "odoc" {with-doc}
 ]
 depopts: [

src/base-solver/sidekick_base_solver.ml

@@ -14,8 +14,9 @@ module Solver_arg = struct
 
   let cc_view = Term.cc_view
   let is_valid_literal _ = true
-  module P = Proof_stub
+  module P = Sidekick_base.Proof
   type proof = P.t
+  type proof_step = P.proof_step
 end
 
 (** SMT solver, obtained from {!Sidekick_smt_solver} *)
@@ -26,7 +27,7 @@ module Th_data = Sidekick_th_data.Make(struct
     module S = Solver
     open! Base_types
     open! Sidekick_th_data
-    module Proof = Proof_stub
+    module Proof = Proof
     module Cstor = Cstor
 
     let as_datatype ty = match Ty.view ty with
@@ -59,9 +60,14 @@ module Th_data = Sidekick_th_data.Make(struct
     let ty_is_finite = Ty.finite
     let ty_set_is_finite = Ty.set_finite
 
-    let lemma_isa_disj p lits = Proof.lemma_isa_disj p lits
-    let lemma_isa_split p lits = Proof.lemma_isa_split p lits
-    let lemma_cstor_inj p lits = Proof.lemma_cstor_inj p lits
+    let lemma_isa_cstor = Proof.lemma_isa_cstor
+    let lemma_select_cstor = Proof.lemma_select_cstor
+    let lemma_isa_split = Proof.lemma_isa_split
+    let lemma_isa_sel = Proof.lemma_isa_sel
+    let lemma_isa_disj = Proof.lemma_isa_disj
+    let lemma_cstor_inj = Proof.lemma_cstor_inj
+    let lemma_cstor_distinct = Proof.lemma_cstor_distinct
+    let lemma_acyclicity = Proof.lemma_acyclicity
   end)
 
 (** Reducing boolean formulas to clauses *)
@@ -69,11 +75,11 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   module S = Solver
   type term = S.T.Term.t
   include Form
-  let lemma_bool_tauto = Proof_stub.lemma_bool_tauto
-  let lemma_bool_c = Proof_stub.lemma_bool_c
-  let lemma_bool_equiv = Proof_stub.lemma_bool_equiv
-  let lemma_ite_true = Proof_stub.lemma_ite_true
-  let lemma_ite_false = Proof_stub.lemma_ite_false
+  let lemma_bool_tauto = Proof.lemma_bool_tauto
+  let lemma_bool_c = Proof.lemma_bool_c
+  let lemma_bool_equiv = Proof.lemma_bool_equiv
+  let lemma_ite_true = Proof.lemma_ite_true
+  let lemma_ite_false = Proof.lemma_ite_false
 end)
 
 (** Theory of Linear Rational Arithmetic *)
@@ -96,7 +102,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   let ty_lra _st = Ty.real()
   let has_ty_real t = Ty.equal (T.ty t) (Ty.real())
 
-  let lemma_lra = Proof_stub.lemma_lra
+  let lemma_lra = Proof.lemma_lra
 
   module Gensym = struct
     type t = {

src/base/Base_types.ml

@@ -5,6 +5,8 @@ module Log = Sidekick_util.Log
 module Fmt = CCFormat
 
 module CC_view = Sidekick_core.CC_view
+module Proof_ser = Sidekick_base_proof_trace.Proof_ser
+module Storage = Sidekick_base_proof_trace.Storage
 
 type lra_pred = Sidekick_arith_lra.Predicate.t = Leq | Geq | Lt | Gt | Eq | Neq
 type lra_op = Sidekick_arith_lra.op = Plus | Minus

src/base/Proof.ml

@@ -0,0 +1,274 @@
+
+open Base_types
+
+(* we store steps as binary chunks *)
+module CS = Chunk_stack
+module PS = Proof_ser
+
+module Config = struct
+  type storage =
+    | No_store
+    | In_memory
+    | On_disk_at of string
+
+  let pp_storage out = function
+    | No_store -> Fmt.string out "no-store"
+    | In_memory -> Fmt.string out "in-memory"
+    | On_disk_at file -> Fmt.fprintf out "(on-file :at %S)" file
+
+  type t = {
+    enabled: bool;
+    storage: storage;
+  }
+
+  let default = { enabled=true; storage=In_memory }
+  let empty = { enabled=false; storage=No_store }
+
+  let pp out (self:t) =
+    let { enabled; storage } = self in
+    Fmt.fprintf out
+      "(@[config@ :enabled %B@ :storage %a@])"
+      enabled pp_storage storage
+
+  let enable b self = {self with enabled=b}
+  let store_in_memory self = {self with storage=In_memory}
+  let store_on_disk_at file self = {self with storage=On_disk_at file}
+  let no_store self = {self with storage=No_store}
+end
+
+(* a step is just a unique integer ID.
+   The actual step is stored in the chunk_stack. *)
+type proof_step = Proof_ser.ID.t
+type term_id = Proof_ser.ID.t
+
+type lit = Lit.t
+type term = Term.t
+
+type t = {
+  mutable enabled : bool;
+  config: Config.t;
+  buf: Buffer.t;
+  mutable storage: Storage.t;
+  mutable dispose: unit -> unit;
+  mutable steps_writer: CS.Writer.t;
+  mutable next_id: int;
+  map_term: term_id Term.Tbl.t; (* term -> proof ID *)
+  map_fun: term_id Fun.Tbl.t;
+}
+type proof_rule = t -> proof_step
+
+module Step_vec = struct
+  type elt=proof_step
+  include VecI32
+end
+
+let disable (self:t) : unit =
+  self.enabled <- false;
+  self.storage <- Storage.No_store;
+  self.dispose();
+  self.steps_writer <- CS.Writer.dummy;
+  ()
+
+let nop_ _ = ()
+
+let create ?(config=Config.default) () : t =
+  (* acquire resources for logging *)
+  let storage, steps_writer, dispose =
+    match config.Config.storage with
+    | Config.No_store ->
+      Storage.No_store, CS.Writer.dummy, nop_
+
+    | Config.In_memory ->
+      let buf = CS.Buf.create ~cap:256 () in
+      Storage.In_memory buf, CS.Writer.into_buf buf, nop_
+
+    | Config.On_disk_at file ->
+      let oc =
+        open_out_gen [Open_creat; Open_wronly; Open_trunc; Open_binary] 0o644 file
+      in
+      let w = CS.Writer.into_channel oc in
+      let dispose () = close_out oc in
+      Storage.On_disk (file, oc), w, dispose
+  in
+  { enabled=config.Config.enabled;
+    config;
+    next_id=1;
+    buf=Buffer.create 1_024;
+    map_term=Term.Tbl.create 32;
+    map_fun=Fun.Tbl.create 32;
+    steps_writer; storage; dispose;
+  }
+
+let empty = create ~config:Config.empty ()
+
+let iter_steps_backward (self:t) =
+  Storage.iter_steps_backward self.storage
+
+let dummy_step : proof_step = Int32.min_int
+
+let[@inline] enabled (self:t) = self.enabled
+
+(* allocate a unique ID to refer to an event in the trace *)
+let[@inline] alloc_id (self:t) : Proof_ser.ID.t =
+  let n = self.next_id in
+  self.next_id <- 1 + self.next_id;
+  Int32.of_int n
+
+(* emit a proof step *)
+let emit_step_ (self:t) (step:Proof_ser.Step.t) : unit =
+  if enabled self then (
+    Buffer.clear self.buf;
+    Proof_ser.Step.encode self.buf step;
+    Chunk_stack.Writer.add_buffer self.steps_writer self.buf;
+  )
+
+let emit_fun_ (self:t) (f:Fun.t) : term_id =
+  try Fun.Tbl.find self.map_fun f
+  with Not_found ->
+    let id = alloc_id self in
+    Fun.Tbl.add self.map_fun f id;
+    let f_name = ID.to_string (Fun.id f) in
+    emit_step_ self
+      Proof_ser.({ Step.id; view=Fun_decl {Fun_decl.f=f_name}});
+    id
+
+let rec emit_term_ (self:t) (t:Term.t) : term_id =
+  try Term.Tbl.find self.map_term t
+  with Not_found ->
+    let view = match Term_cell.map (emit_term_ self) @@ Term.view t with
+      | Term_cell.Bool b ->
+        PS.Step_view.Expr_bool {PS.Expr_bool.b}
+
+      | Term_cell.Ite (a,b,c) ->
+        PS.Step_view.Expr_if {PS.Expr_if.cond=a; then_=b; else_=c}
+
+      | Term_cell.Not a ->
+        PS.Step_view.Expr_not {PS.Expr_not.f=a}
+
+      | Term_cell.App_fun (f, arr) ->
+        let f = emit_fun_ self f in
+        PS.Step_view.Expr_app {PS.Expr_app.f; args=(arr:_ IArray.t:> _ array)}
+
+      | Term_cell.Eq (a, b) ->
+        PS.Step_view.Expr_eq {PS.Expr_eq.lhs=a; rhs=b}
+
+      | LRA _ -> assert false (* TODO *)
+    in
+
+    let id = alloc_id self in
+    Term.Tbl.add self.map_term t id;
+    emit_step_ self {id; view};
+    id
+
+let emit_lit_ (self:t) (lit:Lit.t) : term_id =
+  let sign = Lit.sign lit in
+  let t = emit_term_ self (Lit.term lit) in
+  if sign then t else Int32.neg t
+
+let emit_ (self:t) f : proof_step =
+  if enabled self then (
+    let view = f () in
+    let id = alloc_id self in
+    emit_step_ self {PS.Step.id; view};
+    id
+  ) else dummy_step
+
+let emit_no_return_ (self:t) f : unit =
+  if enabled self then (
+    let view = f () in
+    emit_step_ self {PS.Step.id=(-1l); view}
+  )
+
+let[@inline] emit_redundant_clause lits ~hyps (self:t) =
+  emit_ self @@ fun() ->
+  let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
+  let clause = Proof_ser.{Clause.lits} in
+  let hyps = Iter.to_array hyps in
+  PS.Step_view.Step_rup {res=clause; hyps}
+
+let emit_input_clause (lits:Lit.t Iter.t) (self:t) =
+  emit_ self @@ fun () ->
+  let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
+  PS.(Step_view.Step_input {Step_input.c={Clause.lits}})
+
+let define_term t u (self:t) =
+  emit_ self @@ fun () ->
+  let t = emit_term_ self t and u = emit_term_ self u in
+  PS.(Step_view.Expr_def {Expr_def.c=t; rhs=u})
+
+let proof_p1 rw_with c (self:t) =
+  emit_ self @@ fun() ->
+  PS.(Step_view.Step_proof_p1 {Step_proof_p1.c; rw_with})
+
+let lemma_preprocess t u ~using (self:t) =
+  emit_ self @@ fun () ->
+  let t = emit_term_ self t and u = emit_term_ self u in
+  let using = using |> Iter.to_array in
+  PS.(Step_view.Step_preprocess {Step_preprocess.t; u; using})
+
+let lemma_true t (self:t) =
+  emit_ self @@ fun () ->
+  let t = emit_term_ self t in
+  PS.(Step_view.Step_true {Step_true.true_=t})
+
+let lemma_cc lits (self:t) =
+  emit_ self @@ fun () ->
+  let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
+  PS.(Step_view.Step_cc {Step_cc.eqns=lits})
+
+let lemma_rw_clause c ~res ~using (self:t) =
+  if enabled self then (
+    let using = Iter.to_array using in
+    if Array.length using=0 then c (* useless step *)
+    else (
+      emit_ self @@ fun() ->
+      let lits = Iter.map (emit_lit_ self) res |> Iter.to_array in
+      let res = Proof_ser.{Clause.lits} in
+      PS.(Step_view.Step_clause_rw {Step_clause_rw.c; res; using})
+    )
+  ) else dummy_step
+
+(* TODO *)
+let with_defs _ _ (_pr:t) = dummy_step
+
+(* not useful *)
+let del_clause _ _ (_pr:t) = ()
+
+(* TODO *)
+let emit_unsat_core _ (_pr:t) = dummy_step
+
+let emit_unsat c (self:t) : unit =
+  emit_no_return_ self @@ fun() ->
+  PS.(Step_view.Step_unsat {Step_unsat.c})
+
+let lemma_bool_tauto lits (self:t) =
+  emit_ self @@ fun() ->
+  let lits = Iter.map (emit_lit_ self) lits |> Iter.to_array in
+  PS.(Step_view.Step_bool_tauto {Step_bool_tauto.lits})
+
+let lemma_bool_c rule (ts:Term.t list) (self:t) =
+  emit_ self @@ fun() ->
+  let exprs = ts |> Util.array_of_list_map (emit_term_ self) in
+  PS.(Step_view.Step_bool_c {Step_bool_c.exprs; rule})
+
+(* TODO *)
+
+let lemma_lra _ _ = dummy_step
+
+let lemma_bool_equiv _ _ _ = dummy_step
+
+let lemma_ite_true ~ite:_ _ = dummy_step
+let lemma_ite_false ~ite:_ _ = dummy_step
+
+let lemma_isa_cstor ~cstor_t:_ _ (_pr:t) = dummy_step
+let lemma_select_cstor ~cstor_t:_ _ (_pr:t) = dummy_step
+let lemma_isa_split _ _ (_pr:t) = dummy_step
+let lemma_isa_sel _ (_pr:t) = dummy_step
+let lemma_isa_disj _ _ (_pr:t) = dummy_step
+let lemma_cstor_inj _ _ _ (_pr:t) = dummy_step
+let lemma_cstor_distinct _ _ (_pr:t) = dummy_step
+let lemma_acyclicity _ (_pr:t) = dummy_step
+
+module Unsafe_ = struct
+  let[@inline] id_of_proof_step_ (p:proof_step) : proof_step = p
+end

src/base/Proof.mli

@@ -0,0 +1,84 @@
+
+(** Proof representation *)
+
+open Base_types
+
+(** Configuration of proofs *)
+module Config : sig
+  type t
+
+  val pp : t Fmt.printer
+
+  val default : t
+  (** Default proof config, enabled *)
+
+  val empty : t
+  (** Disabled proof, without storage *)
+
+  val enable : bool -> t -> t
+  (** Enable/disable proof storage *)
+
+  val store_in_memory : t -> t
+  (** Store proof in memory *)
+
+  val store_on_disk_at : string -> t -> t
+  (** [store_on_disk_at file] stores temporary proof in file [file] *)
+
+  val no_store : t -> t
+end
+
+(** {2 Main Proof API} *)
+
+type t
+(** A container for the whole proof *)
+
+type proof_step
+(** A proof step in the trace.
+
+    The proof will store all steps, and at the end when we find the empty clause
+    we can filter them to keep only the relevant ones. *)
+
+include Sidekick_core.PROOF
+  with type t := t
+   and type proof_step := proof_step
+   and type lit = Lit.t
+   and type term = Term.t
+
+val lemma_lra : Lit.t Iter.t -> proof_rule
+
+include Sidekick_th_data.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t
+
+include Sidekick_th_bool_static.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t
+
+(** {2 Creation} *)
+
+val create : ?config:Config.t -> unit -> t
+(** Create new proof.
+    @param config modifies the proof behavior *)
+
+val empty : t
+(** Empty proof, stores nothing *)
+
+val disable : t -> unit
+(** Disable proof, even if the config would enable it *)
+
+(** {2 Use the proof} *)
+
+val iter_steps_backward : t -> Proof_ser.Step.t Iter.t
+(** Iterates on all the steps of the proof, from the end.
+
+    This will yield nothing if the proof was disabled or used
+    a dummy backend. *)
+
+
+module Unsafe_ : sig
+  val id_of_proof_step_ : proof_step -> Proof_ser.ID.t
+end

src/base/Proof_dummy.ml

@@ -0,0 +1,45 @@
+
+open Base_types
+
+type lit = Lit.t
+type term = Term.t
+
+type t = unit
+type proof_step = unit
+type proof_rule = t -> proof_step
+
+module Step_vec = Vec_unit
+
+let create () : t = ()
+let with_proof _ _ = ()
+
+let enabled (_pr:t) = false
+let del_clause _ _ (_pr:t) = ()
+let emit_redundant_clause _ ~hyps:_ _ = ()
+let emit_input_clause _ _ = ()
+let define_term _ _ _ = ()
+let emit_unsat _ _ = ()
+let proof_p1 _ _ (_pr:t) = ()
+let emit_unsat_core _ (_pr:t) = ()
+let lemma_preprocess _ _ ~using:_ (_pr:t) = ()
+let lemma_true _ _ = ()
+let lemma_cc _ _ = ()
+let lemma_rw_clause _ ~res:_ ~using:_ (_pr:t) = ()
+let with_defs _ _ (_pr:t) = ()
+
+let lemma_lra _ _ = ()
+
+let lemma_bool_tauto _ _ = ()
+let lemma_bool_c _ _ _ = ()
+let lemma_bool_equiv _ _ _ = ()
+let lemma_ite_true ~ite:_ _ = ()
+let lemma_ite_false ~ite:_ _ = ()
+
+let lemma_isa_cstor ~cstor_t:_ _ (_pr:t) = ()
+let lemma_select_cstor ~cstor_t:_ _ (_pr:t) = ()
+let lemma_isa_split _ _ (_pr:t) = ()
+let lemma_isa_sel _ (_pr:t) = ()
+let lemma_isa_disj _ _ (_pr:t) = ()
+let lemma_cstor_inj _ _ _ (_pr:t) = ()
+let lemma_cstor_distinct _ _ (_pr:t) = ()
+let lemma_acyclicity _ (_pr:t) = ()

src/base/Proof_dummy.mli

@@ -0,0 +1,29 @@
+
+(** Dummy proof module that does nothing. *)
+
+open Base_types
+
+
+include Sidekick_core.PROOF
+  with type t = private unit
+   and type proof_step = private unit
+   and type lit = Lit.t
+   and type term = Term.t
+
+type proof_rule = t -> proof_step
+
+val create : unit -> t
+
+val lemma_lra : Lit.t Iter.t -> proof_rule
+
+include Sidekick_th_data.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t
+
+include Sidekick_th_bool_static.PROOF
+  with type proof := t
+   and type proof_step := proof_step
+   and type lit := Lit.t
+   and type term := Term.t

src/base/Proof_quip.ml

@@ -0,0 +1,295 @@
+
+(* output proof *)
+module P = Sidekick_quip.Proof
+
+(* serialized proof trace *)
+module PS = Sidekick_base_proof_trace.Proof_ser
+
+type t = P.t
+
+module type CONV_ARG = sig
+  val proof : Proof.t
+  val unsat : Proof.proof_step
+end
+
+module Make_lazy_tbl(T:sig type t end)() = struct
+  let lazy_tbl_ : T.t lazy_t Util.Int_tbl.t = Util.Int_tbl.create 32
+
+  (** FInd step by its ID *)
+  let find (id:PS.ID.t) : T.t =
+    match Util.Int_tbl.get lazy_tbl_ (Int32.to_int id) with
+    | Some (lazy p) -> p
+    | None ->
+      Error.errorf "proof-quip: step `%a` was not reconstructed" PS.ID.pp id
+
+  (** Add entry *)
+  let add id (e:T.t lazy_t) =
+    assert (not (Util.Int_tbl.mem lazy_tbl_ (Int32.to_int id)));
+    Util.Int_tbl.add lazy_tbl_ (Int32.to_int id) e
+end
+
+module Conv(X : CONV_ARG) : sig
+  val reconstruct : unit -> t
+end = struct
+  let (!!) = Lazy.force
+
+  (* Steps we need to decode.
+     Invariant: the IDs of these steps must be lower than the current processed
+     ID (we start from the end) *)
+  let needed_steps_ = Util.Int_tbl.create 128
+
+  let add_needed_step (id:PS.ID.t) : unit =
+    Util.Int_tbl.replace needed_steps_ (Int32.to_int id) ()
+
+  let unsat_id = Proof.Unsafe_.id_of_proof_step_ X.unsat
+
+  (* start with the unsat step *)
+  let () = add_needed_step unsat_id
+
+  (* store reconstructed proofs, but lazily because their dependencies
+     (sub-steps, terms, etc.) might not have come up in the reverse stream yet. *)
+  module L_proofs = Make_lazy_tbl(struct type t = P.t end)()
+
+  (* store reconstructed terms *)
+  module L_terms = Make_lazy_tbl(struct type t = P.term end)()
+
+  (* id -> function symbol *)
+  let funs: P.Fun.t Util.Int_tbl.t = Util.Int_tbl.create 32
+
+  (* list of toplevel steps, in the final proof order *)
+  let top_steps_ : P.composite_step lazy_t list ref = ref []
+  let add_top_step s = top_steps_ := s :: !top_steps_
+
+  let conv_lit (lit:PS.Lit.t) : P.Lit.t lazy_t =
+    let v = Int32.abs lit in
+    add_needed_step v;
+    lazy (
+      let t = L_terms.find v in
+      let sign = lit > Int32.zero in
+      (* reconstruct literal *)
+      P.Lit.mk sign t
+    )
+
+  let conv_lits (lits:PS.Lit.t array) : P.Lit.t list lazy_t =
+    let lits =
+      lits
+      |> Util.array_to_list_map conv_lit
+    in
+    lazy (List.map Lazy.force lits)
+
+  let conv_clause (c:PS.Clause.t) : P.clause lazy_t = conv_lits c.lits
+
+  let name_clause (id: PS.ID.t) : string = Printf.sprintf "c%ld" id
+  let name_term (id: PS.ID.t) : string = Printf.sprintf "t%ld" id
+
+  (* TODO: see if we can allow `(stepc c5 (cl …) (… (@ c5) …))`.
+     Namely, the alias `c5 := (cl …)` could be available within its own proof
+     so we don't have to print it twice, which is useful for rules like `ccl`
+     where it's typically `(stepc c5 (cl …) (ccl (cl …)))` for twice the space.
+     *)
+
+  let is_def_ (step:PS.Step.t) =
+    match step.view with
+    | PS.Step_view.Expr_def _ -> true
+    | _ -> false
+
+  (* process a step of the trace *)
+  let process_step_ (step: PS.Step.t) : unit =
+    let lid = step.id in
+    let id = Int32.to_int lid in
+    if Util.Int_tbl.mem needed_steps_ id || is_def_ step then (
+      Log.debugf 20 (fun k->k"(@[proof-quip.process-needed-step@ %a@])" PS.Step.pp step);
+      Util.Int_tbl.remove needed_steps_ id;
+
+      (* now process the step *)
+      begin match step.view with
+        | PS.Step_view.Step_input i ->
+          let c = conv_clause i.PS.Step_input.c in
+          let name = name_clause lid in
+          let step = lazy (
+            P.S_step_c {name; res= !!c; proof=P.assertion_c_l !!c}
+          ) in
+          add_top_step step;
+          (* refer to the step by name now *)
+          L_proofs.add lid (lazy (P.ref_by_name name));
+
+        | PS.Step_view.Step_unsat { c=uclause } ->
+          let c = [] in
+          let name = "unsat" in
+          add_needed_step uclause;
+          let name_c = name_clause uclause in
+          add_top_step (lazy (P.S_step_c{name; res=c; proof=P.ref_by_name name_c}));
+
+        | PS.Step_view.Step_cc { eqns } ->
+          let c = conv_lits eqns in
+          let name = name_clause lid in
+          let step = lazy (
+            P.S_step_c {name; res= !!c; proof=P.cc_lemma !!c}
+          ) in
+          add_top_step  step;
+          L_proofs.add lid (lazy (P.ref_by_name name))
+
+        | PS.Step_view.Fun_decl { f } ->
+          Util.Int_tbl.add funs id f;
+
+        | PS.Step_view.Expr_eq { lhs; rhs } ->
+          add_needed_step lhs;
+          add_needed_step rhs;
+          let name = name_term lid in
+          let step = lazy (
+            let lhs = L_terms.find lhs
+            and rhs = L_terms.find rhs in
+            let t = P.T.eq lhs rhs in
+            P.S_define_t_name (name, t)
+          ) in
+          add_top_step step;
+          L_terms.add lid (lazy (P.T.ref name))
+
+        | PS.Step_view.Expr_bool {b} ->
+          let t = Lazy.from_val (P.T.bool b) in
+          L_terms.add lid t
+
+        | PS.Step_view.Expr_app { f; args } ->
+          add_needed_step f;
+          Array.iter add_needed_step args;
+          let t = lazy (
+            let f =
+              try Util.Int_tbl.find funs (Int32.to_int f)
+              with Not_found -> Error.errorf "unknown function '%ld'" f
+            in
+            let args = Array.map L_terms.find args in
+            P.T.app_fun f args
+          ) in
+
+          if Array.length args > 0 then (
+            (* introduce a name *)
+            let name = name_term lid in
+            let step = lazy (P.S_define_t_name (name, !!t)) in
+            add_top_step step;
+            L_terms.add lid (lazy (P.T.ref name))
+          ) else (
+            L_terms.add lid t
+          )
+
+        | PS.Step_view.Expr_def { c; rhs } ->
+          add_needed_step c;
+          add_needed_step rhs;
+          let name = name_clause lid in
+          (* add [name := (|- c=rhs) by refl c].
+             Make sure we do it first, order in final proof will be reversed. *)
+          let step_refl = lazy (
+            let c = L_terms.find c in
+            let rhs = L_terms.find rhs in
+            P.S_step_c {name; res=[P.Lit.eq c rhs]; proof=P.refl c}
+          ) in
+          add_top_step step_refl;
+          (* define [c:=rhs] *)
+          let step_def = lazy (
+            let c = L_terms.find c in
+            let rhs = L_terms.find rhs in
+            P.S_define_t (c, rhs)
+          ) in
+          add_top_step step_def;
+          L_proofs.add lid (lazy (P.ref_by_name name));
+
+        | PS.Step_view.Expr_not { f } ->
+          add_needed_step f;
+          let t = lazy (
+            let f = L_terms.find f in
+            P.T.not_ f
+          ) in
+          L_terms.add lid t
+
+        | PS.Step_view.Expr_if _ -> () (* TODO *)
+
+        | PS.Step_view.Step_rup { res; hyps } ->
+          let res = conv_clause res in
+          Array.iter add_needed_step hyps;
+          let name = name_clause lid in
+          let step = lazy (
+            let hyps = Util.array_to_list_map L_proofs.find hyps in
+            P.S_step_c {name; res= !!res; proof=P.rup !!res hyps}
+          ) in
+          add_top_step step;
+          L_proofs.add lid (lazy (P.ref_by_name name));
+
+        | PS.Step_view.Step_clause_rw { c; res; using } ->
+          let res = conv_clause res in
+          add_needed_step c;
+          Array.iter add_needed_step using;
+          let name = name_clause lid in
+
+          let step = lazy (
+            let c = L_proofs.find c in
+            let using = Util.array_to_list_map L_proofs.find using in
+            let res = !! res in
+            P.S_step_c {name; res; proof=P.Clause_rw {res; c0=c; using}}
+          ) in
+          add_top_step step;
+          L_proofs.add lid (lazy (P.ref_by_name name))
+
+        | PS.Step_view.Step_proof_p1 { rw_with; c } ->
+          add_needed_step c;
+          add_needed_step rw_with;
+          let p = lazy (
+            let rw_with = L_proofs.find rw_with in
+            let c = L_proofs.find c in
+            P.paramod1 rw_with c
+          ) in
+          L_proofs.add lid p;
+
+        | PS.Step_view.Step_bool_c { rule; exprs } ->
+          Array.iter add_needed_step exprs;
+          let p = lazy (
+            let exprs = Util.array_to_list_map L_terms.find exprs in
+            P.bool_c rule exprs
+          ) in
+          L_proofs.add lid p;
+
+        | PS.Step_view.Step_preprocess { t; u; using } ->
+          let name = name_clause lid in
+          add_needed_step t;
+          add_needed_step u;
+          Array.iter add_needed_step using;
+
+          let step = lazy (
+            let t = L_terms.find t
+            and u = L_terms.find u in
+            let using = Util.array_to_list_map L_proofs.find using in
+            let res = [P.Lit.eq t u] in
+            P.S_step_c {res; name; proof=P.cc_imply_l using t u}
+          ) in
+          add_top_step step;
+          L_proofs.add lid (lazy (P.ref_by_name name));
+
+        | PS.Step_view.Step_bridge_lit_expr _ -> assert false
+        | PS.Step_view.Step_bool_tauto _ -> () (* TODO *)
+        | PS.Step_view.Step_true _ -> () (* TODO *)
+
+      end
+    )
+
+  let reconstruct_once_ = lazy (
+    Profile.with_ "proof-quip.reconstruct" @@ fun () ->
+    Proof.iter_steps_backward X.proof process_step_;
+    ()
+  )
+
+  let reconstruct () : t =
+    Lazy.force reconstruct_once_;
+    let steps = Util.array_of_list_map Lazy.force !top_steps_ in
+    P.composite_a steps
+end
+
+let of_proof (self:Proof.t) ~(unsat:Proof.proof_step) : P.t =
+  let module C = Conv(struct
+      let proof = self
+      let unsat = unsat
+    end) in
+  C.reconstruct()
+
+type out_format = Sidekick_quip.out_format =
+  | Sexp
+  | CSexp
+
+let output = Sidekick_quip.output

src/base/Proof_quip.mli

@@ -0,0 +1,13 @@
+(** Export to Quip from {!module:Proof}.
+
+    We use {!Sidekick_quip} but do not export anything from it. *)
+
+type t
+
+val of_proof : Proof.t -> unsat:Proof.proof_step -> t
+
+type out_format = Sidekick_quip.out_format =
+  | Sexp
+  | CSexp
+
+val output : ?fmt:out_format -> out_channel -> t -> unit

src/base/Proof_stub.ml

@@ -1,30 +0,0 @@
-
-open Base_types
-
-type lit = Lit.t
-type term = Term.t
-
-type t = unit
-type dproof = t -> unit
-
-let create () : t = ()
-let with_proof _ _ = ()
-
-let begin_subproof _ = ()
-let end_subproof _ = ()
-let del_clause _ _ = ()
-let emit_redundant_clause _ _ = ()
-let emit_input_clause _ _ = ()
-let define_term _ _ _ = ()
-let lemma_preprocess _ _ _ = ()
-let lemma_true _ _ = ()
-let lemma_cc _ _ = ()
-let lemma_lra _ _ = ()
-let lemma_cstor_inj _ _ = ()
-let lemma_isa_disj _ _ = ()
-let lemma_isa_split _ _ = ()
-let lemma_bool_tauto _ _ = ()
-let lemma_bool_c _ _ _ = ()
-let lemma_bool_equiv _ _ _ = ()
-let lemma_ite_true ~a:_ ~ite:_ _ = ()
-let lemma_ite_false ~a:_ ~ite:_ _ = ()

src/base/Proof_stub.mli

@@ -1,22 +0,0 @@
-
-(** Dummy proof module that does nothing. *)
-
-open Base_types
-
-include Sidekick_core.PROOF
-  with type lit = Lit.t
-   and type term = Term.t
-
-val create : unit -> t
-
-val lemma_bool_tauto : Lit.t Iter.t -> t -> unit
-val lemma_bool_c : string -> term list -> t -> unit
-val lemma_bool_equiv : term -> term -> t -> unit
-val lemma_ite_true : a:term -> ite:term -> t -> unit
-val lemma_ite_false : a:term -> ite:term -> t -> unit
-
-val lemma_lra : Lit.t Iter.t -> t -> unit
-
-val lemma_isa_split : Lit.t Iter.t -> t -> unit
-val lemma_isa_disj : Lit.t Iter.t -> t -> unit
-val lemma_cstor_inj : Lit.t Iter.t -> t -> unit

src/base/Sidekick_base.ml

@@ -33,7 +33,10 @@ module Form = Form
 
 module Solver_arg = Solver_arg
 module Lit = Lit
-module Proof_stub = Proof_stub
+
+module Proof_dummy = Proof_dummy
+module Proof = Proof
+module Proof_quip = Proof_quip
 
 (* re-export *)
 module IArray = IArray

src/base/dune

@@ -2,7 +2,9 @@
  (name sidekick_base)
  (public_name sidekick-base)
  (synopsis "Base term definitions for the standalone SMT solver and library")
- (libraries containers sidekick.core sidekick.util sidekick.lit
-            sidekick.arith-lra sidekick.th-bool-static
-            sidekick.zarith zarith)
+ (libraries containers iter sidekick.core sidekick.util sidekick.lit
+            sidekick-base.proof-trace sidekick.quip
+            sidekick.arith-lra sidekick.th-bool-static sidekick.th-data
+            sidekick.zarith
+            zarith)
  (flags :standard -w -32 -open Sidekick_util))

src/cc/Sidekick_cc.ml

@@ -16,6 +16,7 @@ module Make (A: CC_ARG)
   : S with module T = A.T
        and module Lit = A.Lit
        and type proof = A.proof
+       and type proof_step = A.proof_step
        and module Actions = A.Actions
 = struct
   module T = A.T
@@ -27,7 +28,7 @@ module Make (A: CC_ARG)
   type lit = Lit.t
   type fun_ = T.Fun.t
   type proof = A.proof
-  type dproof = proof -> unit
+  type proof_step = A.proof_step
   type actions = Actions.t
 
   module Term = T.Term
@@ -95,7 +96,7 @@ module Make (A: CC_ARG)
     | E_merge_t of term * term
     | E_congruence of node * node (* caused by normal congruence *)
     | E_and of explanation * explanation
-    | E_theory of explanation
+    | E_theory of proof_step * explanation list
 
   type repr = node
 
@@ -166,7 +167,7 @@ module Make (A: CC_ARG)
       | E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2
       | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
       | E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
-      | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
+      | E_theory (_p,es) -> Fmt.fprintf out "(@[th@ %a@])" (Util.pp_list pp) es
       | E_and (a,b) ->
         Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
 
@@ -175,7 +176,7 @@ module Make (A: CC_ARG)
     let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b)
     let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b)
     let[@inline] mk_lit l : t = E_lit l
-    let mk_theory e = E_theory e
+    let[@inline] mk_theory p es = E_theory (p,es)
 
     let rec mk_list l =
       match l with
@@ -241,6 +242,7 @@ module Make (A: CC_ARG)
   type t = {
     tst: term_store;
     tbl: node T_tbl.t;
+    proof: proof;
     (* internalization [term -> node] *)
     signatures_tbl : node Sig_tbl.t;
     (* map a signature to the corresponding node in some equivalence class.
@@ -279,7 +281,7 @@ module Make (A: CC_ARG)
   and ev_on_post_merge = t -> actions -> N.t -> N.t -> unit
   and ev_on_new_term = t -> N.t -> term -> unit
   and ev_on_conflict = t -> th:bool -> lit list -> unit
-  and ev_on_propagate = t -> lit -> (unit -> lit list * (proof -> unit)) -> unit
+  and ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit
   and ev_on_is_subterm = N.t -> term -> unit
 
   let[@inline] size_ (r:repr) = r.n_size
@@ -287,6 +289,7 @@ module Make (A: CC_ARG)
   let[@inline] n_false cc = Lazy.force cc.false_
   let n_bool cc b = if b then n_true cc else n_false cc
   let[@inline] term_store cc = cc.tst
+  let[@inline] proof cc = cc.proof
   let allocate_bitfield ~descr cc =
     Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr);
     Bits.mk_field cc.bitgen
@@ -372,7 +375,7 @@ module Make (A: CC_ARG)
         n.n_expl <- FL_none;
     end
 
-  let raise_conflict_ (cc:t) ~th (acts:actions) (e:lit list) p : _ =
+  let raise_conflict_ (cc:t) ~th (acts:actions) (e:lit list) (p:proof_step) : _ =
     Profile.instant "cc.conflict";
     (* clear tasks queue *)
     Vec.clear cc.pending;
@@ -455,8 +458,16 @@ module Make (A: CC_ARG)
           assert false
       end
     | E_lit lit -> lit :: acc
-    | E_theory e' ->
-      th := true; explain_decompose_expl cc ~th acc e'
+    | E_theory (_pr, sub_l) ->
+      (* FIXME: use pr as a subproof. We need to accumulate subproofs too, because
+         there is some amount of resolution done inside the congruence closure
+         itself to resolve Horn clauses produced by theories.
+
+         maybe we need to store [t=u] where [pr] is the proof of [Gamma |- t=u],
+         add [t=u] to the explanation, and use a subproof to resolve
+         it away using [pr] and add [Gamma] to the mix *)
+      th := true;
+      List.fold_left (explain_decompose_expl cc ~th) acc sub_l
     | E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b
     | E_merge_t (a,b) ->
       (* find nodes for [a] and [b] on the fly *)
@@ -656,10 +667,11 @@ module Make (A: CC_ARG)
         let lits = explain_decompose_expl cc ~th [] e_ab in
         let lits = explain_equal_rec_ cc ~th lits a ra in
         let lits = explain_equal_rec_ cc ~th lits b rb in
-        let emit_proof p =
+        let pr =
           let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
-          P.lemma_cc p_lits p in
-        raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) emit_proof
+          P.lemma_cc p_lits @@ Actions.proof acts
+        in
+        raise_conflict_ cc ~th:!th acts (List.rev_map Lit.neg lits) pr
       );
       (* We will merge [r_from] into [r_into].
          we try to ensure that [size ra <= size rb] in general, but always
@@ -774,12 +786,12 @@ module Make (A: CC_ARG)
              let e = lazy (
                let lazy (th, acc) = half_expl in
                let lits = explain_equal_rec_ cc ~th acc u1 t1 in
-               let emit_proof p =
+               let pr =
                  (* make a tautology, not a true guard *)
                  let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
-                 P.lemma_cc p_lits p
+                 P.lemma_cc p_lits @@ Actions.proof acts
                in
-               lits, emit_proof
+               lits, pr
              ) in
              fun () -> Lazy.force e
            in
@@ -846,11 +858,11 @@ module Make (A: CC_ARG)
     let th = ref true in
     let lits = explain_decompose_expl cc ~th [] expl in
     let lits = List.rev_map Lit.neg lits in
-    let emit_proof p =
+    let pr =
       let p_lits = Iter.of_list lits in
-      P.lemma_cc p_lits p
+      P.lemma_cc p_lits @@ Actions.proof acts
     in
-    raise_conflict_ cc ~th:!th acts lits emit_proof
+    raise_conflict_ cc ~th:!th acts lits pr
 
   let merge cc n1 n2 expl =
     Log.debugf 5
@@ -876,12 +888,12 @@ module Make (A: CC_ARG)
       ?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[])
       ?(on_conflict=[]) ?(on_propagate=[]) ?(on_is_subterm=[])
       ?(size=`Big)
-      (tst:term_store) : t =
+      (tst:term_store) (proof:proof) : t =
     let size = match size with `Small -> 128 | `Big -> 2048 in
     let bitgen = Bits.mk_gen () in
     let field_marked_explain = Bits.mk_field bitgen in
     let rec cc = {
-      tst;
+      tst; proof;
       tbl = T_tbl.create size;
       signatures_tbl = Sig_tbl.create size;
       bitgen;

src/cc/Sidekick_cc.mli

@@ -7,4 +7,5 @@ module Make (A: CC_ARG)
   : S with module T = A.T
        and module Lit = A.Lit
        and type proof = A.proof
+       and type proof_step = A.proof_step
        and module Actions = A.Actions

src/checker/drup_check.ml

@@ -71,7 +71,7 @@ end
     Each event is checked by reverse-unit propagation on previous events. *)
 module Fwd_check : sig
   type error =
-    [ `Bad_steps of VecI32.t
+    [ `Bad_steps of VecSmallInt.t
     | `No_empty_clause
     ]
 
@@ -84,11 +84,11 @@ module Fwd_check : sig
 end = struct
   type t = {
     checker: Checker.t;
-    errors: VecI32.t;
+    errors: VecSmallInt.t;
   }
   let create cstore : t = {
     checker=Checker.create cstore;
-    errors=VecI32.create();
+    errors=VecSmallInt.create();
   }
 
   (* check event, return [true] if it's valid *)
@@ -114,17 +114,17 @@ end = struct
     end
 
   type error =
-    [ `Bad_steps of VecI32.t
+    [ `Bad_steps of VecSmallInt.t
     | `No_empty_clause
     ]
 
   let pp_error trace out = function
     | `No_empty_clause -> Fmt.string out "no empty clause found"
     | `Bad_steps bad ->
-      let n0 = VecI32.get bad 0 in
+      let n0 = VecSmallInt.get bad 0 in
       Fmt.fprintf out
         "@[<v>checking failed on %d ops.@ @[<2>First failure is op[%d]:@ %a@]@]"
-        (VecI32.size bad) n0
+        (VecSmallInt.size bad) n0
         Trace.pp_op (Trace.get trace n0)
 
   let check trace : _ result =
@@ -137,7 +137,7 @@ end = struct
           let ok = check_op self i op in
           if ok then (
             Log.debugf 50
-              (fun k->k"(@[check.step.ok@ :idx %d@ :op %a@])" i Trace.pp_op op);
+              (fun k->k"(@[check.proof_rule.ok@ :idx %d@ :op %a@])" i Trace.pp_op op);
 
             (* check if op adds the empty clause *)
             begin match op with
@@ -147,13 +147,13 @@ end = struct
             end;
           ) else (
             Log.debugf 10
-              (fun k->k"(@[check.step.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
-            VecI32.push self.errors i
+              (fun k->k"(@[check.proof_rule.fail@ :idx %d@ :op %a@])" i Trace.pp_op op);
+            VecSmallInt.push self.errors i
           ));
 
-    Log.debugf 10 (fun k->k"found %d errors" (VecI32.size self.errors));
+    Log.debugf 10 (fun k->k"found %d errors" (VecSmallInt.size self.errors));
     if not !has_false then Error `No_empty_clause
-    else if VecI32.size self.errors > 0 then Error (`Bad_steps self.errors)
+    else if VecSmallInt.size self.errors > 0 then Error (`Bad_steps self.errors)
     else Ok ()
 end
 

src/core/Sidekick_core.ml

@@ -147,86 +147,112 @@ end
 
 (** Proofs for the congruence closure *)
 module type CC_PROOF = sig
+  type proof_step
   type t
   type lit
 
-  val lemma_cc : lit Iter.t -> t -> unit
+  val lemma_cc : lit Iter.t -> t -> proof_step
   (** [lemma_cc proof lits] asserts that [lits] form a tautology for the theory
       of uninterpreted functions. *)
 end
 
-(** Signature for SAT-solver proof emission, using DRUP.
-
-    We do not store the resolution steps, just the stream of clauses deduced.
-    See {!Sidekick_drup} for checking these proofs. *)
+(** Signature for SAT-solver proof emission. *)
 module type SAT_PROOF = sig
   type t
   (** The stored proof (possibly nil, possibly on disk, possibly in memory) *)
 
+  type proof_step
+  (** identifier for a proof *)
+
+  module Step_vec : Vec_sig.S with type elt = proof_step
+  (** A vector of steps *)
+
   type lit
   (** A boolean literal for the proof trace *)
 
-  type dproof = t -> unit
-  (** A delayed proof, used to produce proofs on demand from theories. *)
+  type proof_rule = t -> proof_step
+  (** A proof proof_rule constructor, used to obtain proofs from theories *)
 
-  val with_proof : t -> (t -> unit) -> unit
-  (** If proof is enabled, call [f] on it to emit steps.
-      if proof is disabled, the callback won't even be called. *)
+  val enabled : t -> bool
+  (** Returns true if proof production is enabled *)
 
-  val emit_input_clause : lit Iter.t -> t -> unit
+  val emit_input_clause : lit Iter.t -> proof_rule
   (** Emit an input clause. *)
 
-  val emit_redundant_clause : lit Iter.t -> t -> unit
-  (** Emit a clause deduced by the SAT solver, redundant wrt axioms.
-      The clause must be RUP wrt previous clauses. *)
+  val emit_redundant_clause : lit Iter.t -> hyps:proof_step Iter.t -> proof_rule
+  (** Emit a clause deduced by the SAT solver, redundant wrt previous clauses.
+      The clause must be RUP wrt [hyps]. *)
 
-  val del_clause : lit Iter.t -> t -> unit
+  val emit_unsat_core : lit Iter.t -> proof_rule
+  (** Produce a proof of the empty clause given this subset of the assumptions.
+      FIXME: probably needs the list of proof_step that disprove the lits? *)
+
+  val emit_unsat : proof_step -> t -> unit
+  (** Signal "unsat" result at the given proof *)
+
+  val del_clause : proof_step -> lit Iter.t -> t -> unit
   (** Forget a clause. Only useful for performance considerations. *)
-  (* TODO: replace with something index-based? *)
 end
 
-(** Proofs of unsatisfiability.
-
-    We use DRUP(T)-style traces where we simply emit clauses as we go,
-    annotating enough for the checker to reconstruct them.
-    This allows for low overhead proof production. *)
+(** Proofs of unsatisfiability. *)
 module type PROOF = sig
   type t
   (** The abstract representation of a proof. A proof always proves
       a clause to be {b valid} (true in every possible interpretation
       of the problem's assertions, and the theories) *)
 
+  type proof_step
+  (** Identifier for a proof proof_rule (like a unique ID for a clause previously
+      added/proved) *)
+
   type term
   type lit
+  type proof_rule = t -> proof_step
 
   include CC_PROOF
     with type t := t
      and type lit := lit
+     and type proof_step := proof_step
 
   include SAT_PROOF
     with type t := t
      and type lit := lit
+     and type proof_step := proof_step
+     and type proof_rule := proof_rule
 
-  val begin_subproof : t -> unit
-  (** Begins a subproof. The result of this will only be the
-      clause with which {!end_subproof} is called; all other intermediate
-      steps will be discarded. *)
+  val define_term : term -> term -> proof_rule
+  (** [define_term cst u proof] defines the new constant [cst] as being equal
+      to [u].
+      The result is a proof of the clause [cst = u] *)
 
-  val end_subproof : t -> unit
-  (** [end_subproof p] ends the current active subproof, the last result
-      of which is kept. *)
+  val proof_p1 : proof_step -> proof_step -> proof_rule
+  (** [proof_p1 p1 p2], where [p1] proves the unit clause [t=u] (t:bool)
+      and [p2] proves [C \/ t], is the rule that produces [C \/ u],
+      i.e unit paramodulation. *)
 
-  val define_term : term -> term -> t -> unit
-  (** [define_term p cst u] defines the new constant [cst] as being equal
-      to [u]. *)
+  val with_defs : proof_step -> proof_step Iter.t -> proof_rule
+  (** [with_defs pr defs] specifies that [pr] is valid only in
+      a context where the definitions [defs] are present. *)
 
-  val lemma_true : term -> t -> unit
-  (** [lemma_true p (true)] asserts the clause [(true)] *)
+  val lemma_true : term -> proof_rule
+  (** [lemma_true (true) p] asserts the clause [(true)] *)
 
-  val lemma_preprocess : term -> term -> t -> unit
-  (** [lemma_preprocess p t u] asserts that [t = u] is a tautology
+  val lemma_preprocess : term -> term -> using:proof_step Iter.t -> proof_rule
+  (** [lemma_preprocess t u ~using p] asserts that [t = u] is a tautology
       and that [t] has been preprocessed into [u].
-      From now on, [t] and [u] will be used interchangeably. *)
+
+      The theorem [/\_{eqn in using} eqn |- t=u] is proved using congruence
+      closure, and then resolved against the clauses [using] to obtain
+      a unit equality.
+
+      From now on, [t] and [u] will be used interchangeably.
+      @return a proof_rule ID for the clause [(t=u)]. *)
+
+  val lemma_rw_clause : proof_step -> res:lit Iter.t -> using:proof_step Iter.t -> proof_rule
+  (** [lemma_rw_clause prc ~res ~using], where [prc] is the proof of [|- c],
+      uses the equations [|- p_i = q_i] from [using]
+      to rewrite some literals of [c] into [res]. This is used to preprocess
+      literals of a clause (using {!lemma_preprocess} individually). *)
 end
 
 (** Literals
@@ -285,21 +311,25 @@ module type CC_ACTIONS = sig
   module Lit : LIT with module T = T
 
   type proof
-  type dproof = proof -> unit
-  module P : CC_PROOF with type lit = Lit.t and type t = proof
+  type proof_step
+  module P : CC_PROOF with type lit = Lit.t
+                       and type t = proof
+                       and type proof_step = proof_step
 
   type t
   (** An action handle. It is used by the congruence closure
       to perform the actions below. How it performs the actions
       is not specified and is solver-specific. *)
 
-  val raise_conflict : t -> Lit.t list -> dproof -> 'a
+  val proof : t -> proof
+
+  val raise_conflict : t -> Lit.t list -> proof_step -> 'a
   (** [raise_conflict acts c pr] declares that [c] is a tautology of
       the theory of congruence. This does not return (it should raise an
       exception).
       @param pr the proof of [c] being a tautology *)
 
-  val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * dproof) -> unit
+  val propagate : t -> Lit.t -> reason:(unit -> Lit.t list * proof_step) -> unit
   (** [propagate acts lit ~reason pr] declares that [reason() => lit]
       is a tautology.
 
@@ -315,11 +345,16 @@ module type CC_ARG = sig
   module T : TERM
   module Lit : LIT with module T = T
   type proof
-  module P : CC_PROOF with type lit = Lit.t and type t = proof
+  type proof_step
+  module P : CC_PROOF
+    with type lit = Lit.t
+     and type t = proof
+     and type proof_step = proof_step
   module Actions : CC_ACTIONS
     with module T=T
      and module Lit = Lit
      and type proof = proof
+     and type proof_step = proof_step
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
   (** View the term through the lens of the congruence closure *)
@@ -347,12 +382,16 @@ module type CC_S = sig
   module T : TERM
   module Lit : LIT with module T = T
   type proof
-  type dproof = proof -> unit
-  module P : CC_PROOF with type lit = Lit.t and type t = proof
+  type proof_step
+  module P : CC_PROOF
+    with type lit = Lit.t
+     and type t = proof
+     and type proof_step = proof_step
   module Actions : CC_ACTIONS
     with module T = T
     and module Lit = Lit
     and type proof = proof
+    and type proof_step = proof_step
   type term_store = T.Term.store
   type term = T.Term.t
   type fun_ = T.Fun.t
@@ -441,7 +480,14 @@ module type CC_S = sig
     val mk_merge_t : term -> term -> t
     val mk_lit : lit -> t
     val mk_list : t list -> t
-    val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *)
+    val mk_theory : proof_step -> t list -> t
+    (* FIXME: this should probably take [t, u, proof(Gamma |- t=u), expls],
+       where [expls] is a list of explanation of the equations in [Gamma].
+
+       For example for the lemma [a=b] deduced by injectivity from [Some a=Some b]
+       in the theory of datatypes,
+       the arguments would be [a, b, proof(Some a=Some b |- a=b), e0]
+       where [e0] is an explanation of [Some a=Some b] *)
   end
 
   type node = N.t
@@ -456,6 +502,8 @@ module type CC_S = sig
 
   val term_store : t -> term_store
 
+  val proof : t -> proof
+
   val find : t -> node -> repr
   (** Current representative *)
 
@@ -493,7 +541,7 @@ module type CC_S = sig
       participating in the conflict are purely syntactic theories
       like injectivity of constructors. *)
 
-  type ev_on_propagate = t -> lit -> (unit -> lit list * dproof) -> unit
+  type ev_on_propagate = t -> lit -> (unit -> lit list * proof_step) -> unit
   (** [ev_on_propagate cc lit reason] is called whenever [reason() => lit]
       is a propagated lemma. See {!CC_ACTIONS.propagate}. *)
 
@@ -512,6 +560,7 @@ module type CC_S = sig
     ?on_is_subterm:ev_on_is_subterm list ->
     ?size:[`Small | `Big] ->
     term_store ->
+    proof ->
     t
   (** Create a new congruence closure.
 
@@ -647,11 +696,14 @@ module type SOLVER_INTERNAL = sig
   type ty_store = T.Ty.store
   type clause_pool
   type proof
-  type dproof = proof -> unit
-  (** Delayed proof. This is used to build a proof step on demand. *)
+  type proof_step
 
   (** {3 Proofs} *)
-  module P : PROOF with type lit = Lit.t and type term = term and type t = proof
+  module P : PROOF
+    with type lit = Lit.t
+     and type term = term
+     and type t = proof
+     and type proof_step = proof_step
 
   (** {3 Main type for a solver} *)
   type t
@@ -661,7 +713,8 @@ module type SOLVER_INTERNAL = sig
   val ty_st : t -> ty_store
   val stats : t -> Stat.t
 
-  val with_proof : t -> (proof -> unit) -> unit
+  val proof : t -> proof
+  (** Access the proof object *)
 
   (** {3 Actions for the theories} *)
 
@@ -670,13 +723,6 @@ module type SOLVER_INTERNAL = sig
 
   type lit = Lit.t
 
-  (** {3 Proof helpers} *)
-
-  val define_const : t -> const:term -> rhs:term -> unit
-  (** [define_const si ~const ~rhs] adds the definition [const := rhs]
-      to the (future) proof. [const] should be a fresh constant that
-      occurs nowhere else, and [rhs] a term defined without [const]. *)
-
   (** {3 Congruence Closure} *)
 
   (** Congruence closure instance *)
@@ -684,6 +730,7 @@ module type SOLVER_INTERNAL = sig
     with module T = T
      and module Lit = Lit
      and type proof = proof
+     and type proof_step = proof_step
      and type P.t = proof
      and type P.lit = lit
      and type Actions.t = theory_actions
@@ -703,24 +750,25 @@ module type SOLVER_INTERNAL = sig
     val clear : t -> unit
     (** Reset internal cache, etc. *)
 
-    val with_proof : t -> (proof -> unit) -> unit
+    val proof : t -> proof
+    (** Access proof *)
 
-    type hook = t -> term -> term option
+    type hook = t -> term -> (term * proof_step Iter.t) option
     (** Given a term, try to simplify it. Return [None] if it didn't change.
 
         A simple example could be a hook that takes a term [t],
         and if [t] is [app "+" (const x) (const y)] where [x] and [y] are number,
         returns [Some (const (x+y))], and [None] otherwise. *)
 
-    val normalize : t -> term -> term option
+    val normalize : t -> term -> (term * proof_step) option
     (** Normalize a term using all the hooks. This performs
         a fixpoint, i.e. it only stops when no hook applies anywhere inside
         the term. *)
 
-    val normalize_t : t -> term -> term
+    val normalize_t : t -> term -> term * proof_step option
     (** Normalize a term using all the hooks, along with a proof that the
         simplification is correct.
-        returns [t, refl t] if no simplification occurred. *)
+        returns [t, ø] if no simplification occurred. *)
   end
 
   type simplify_hook = Simplify.hook
@@ -728,13 +776,11 @@ module type SOLVER_INTERNAL = sig
   val add_simplifier : t -> Simplify.hook -> unit
   (** Add a simplifier hook for preprocessing. *)
 
-  val simplifier : t -> Simplify.t
-
-  val simplify_t : t -> term -> term option
+  val simplify_t : t -> term -> (term * proof_step) option
   (** Simplify input term, returns [Some u] if some
       simplification occurred. *)
 
-  val simp_t : t -> term -> term
+  val simp_t : t -> term -> term * proof_step option
   (** [simp_t si t] returns [u] even if no simplification occurred
       (in which case [t == u] syntactically).
       It emits [|- t=u].
@@ -746,10 +792,17 @@ module type SOLVER_INTERNAL = sig
       Typically some clauses are also added to the solver. *)
 
   module type PREPROCESS_ACTS = sig
-    val mk_lit : ?sign:bool -> term -> lit
-    (** creates a new literal for a boolean term. *)
+    val proof : proof
 
-    val add_clause : lit list -> dproof -> unit
+    val mk_lit_nopreproc : ?sign:bool -> term -> lit
+    (** [mk_lit t] creates a new literal for a boolean term [t]. *)
+
+    val mk_lit : ?sign:bool -> term -> lit * proof_step option
+    (** [mk_lit t] creates a new literal for a boolean term [t].
+        Also returns an optional proof of preprocessing, which if present
+        is the proof of [|- t = lit] with [lit] the result. *)
+
+    val add_clause : lit list -> proof_step -> unit
     (** pushes a new clause into the SAT solver. *)
 
     val add_lit : ?default_pol:bool -> lit -> unit
@@ -762,7 +815,7 @@ module type SOLVER_INTERNAL = sig
   type preprocess_hook =
     t ->
     preprocess_actions ->
-    term -> term option
+    term -> (term * proof_step Iter.t) option
   (** Given a term, try to preprocess it. Return [None] if it didn't change,
       or [Some (u)] if [t=u].
       Can also add clauses to define new terms.
@@ -782,7 +835,7 @@ module type SOLVER_INTERNAL = sig
 
   (** {3 hooks for the theory} *)
 
-  val raise_conflict : t -> theory_actions -> lit list -> dproof -> 'a
+  val raise_conflict : t -> theory_actions -> lit list -> proof_step -> 'a
   (** Give a conflict clause to the solver *)
 
   val push_decision : t -> theory_actions -> lit -> unit
@@ -791,27 +844,27 @@ module type SOLVER_INTERNAL = sig
       If the SAT solver backtracks, this (potential) decision is removed
       and forgotten. *)
 
-  val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * dproof) -> unit
+  val propagate: t -> theory_actions -> lit -> reason:(unit -> lit list * proof_step) -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  val propagate_l: t -> theory_actions -> lit -> lit list -> dproof -> unit
+  val propagate_l: t -> theory_actions -> lit -> lit list -> proof_step -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 
-  val add_clause_temp : t -> theory_actions -> lit list -> dproof -> unit
+  val add_clause_temp : t -> theory_actions -> lit list -> proof_step -> unit
   (** Add local clause to the SAT solver. This clause will be
       removed when the solver backtracks. *)
 
-  val add_clause_permanent : t -> theory_actions -> lit list -> dproof -> unit
+  val add_clause_permanent : t -> theory_actions -> lit list -> proof_step -> unit
   (** Add toplevel clause to the SAT solver. This clause will
       not be backtracked. *)
 
   val mk_lit : t -> theory_actions -> ?sign:bool -> term -> lit
   (** Create a literal. This automatically preprocesses the term. *)
 
-  val preprocess_term : t -> preprocess_actions -> term -> term
-  (** Preprocess a term. The preprocessing proof is automatically emitted. *)
+  val preprocess_term : t -> preprocess_actions -> term -> term * proof_step option
+  (** Preprocess a term. *)
 
   val add_lit : t -> theory_actions -> ?default_pol:bool -> lit -> unit
   (** Add the given literal to the SAT solver, so it gets assigned
@@ -867,7 +920,7 @@ module type SOLVER_INTERNAL = sig
   val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
   (** Callback called on every CC conflict *)
 
-  val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * dproof) -> unit) -> unit
+  val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof_step) -> unit) -> unit
   (** Callback called on every CC propagation *)
 
   val on_partial_check : t -> (t -> theory_actions -> lit Iter.t -> unit) -> unit
@@ -914,13 +967,19 @@ module type SOLVER = sig
   module T : TERM
   module Lit : LIT with module T = T
   type proof
-  module P : PROOF with type lit = Lit.t and type t = proof and type term = T.Term.t
+  type proof_step
+  module P : PROOF
+    with type lit = Lit.t
+     and type t = proof
+     and type proof_step = proof_step
+     and type term = T.Term.t
 
   module Solver_internal
     : SOLVER_INTERNAL
       with module T = T
        and module Lit = Lit
        and type proof = proof
+       and type proof_step = proof_step
        and module P = P
   (** Internal solver, available to theories.  *)
 
@@ -931,8 +990,6 @@ module type SOLVER = sig
   type term = T.Term.t
   type ty = T.Ty.t
   type lit = Lit.t
-  type dproof = proof -> unit
-  (** Delayed proof. This is used to build a proof step on demand. *)
 
   (** {3 A theory}
 
@@ -1026,6 +1083,7 @@ module type SOLVER = sig
   val stats : t -> Stat.t
   val tst : t -> T.Term.store
   val ty_st : t -> T.Ty.store
+  val proof : t -> proof
 
   val create :
     ?stat:Stat.t ->
@@ -1067,11 +1125,11 @@ module type SOLVER = sig
 
       The proof of [|- lit = lit'] is directly added to the solver's proof. *)
 
-  val add_clause : t -> lit IArray.t -> dproof -> unit
+  val add_clause : t -> lit IArray.t -> proof_step -> unit
   (** [add_clause solver cs] adds a boolean clause to the solver.
       Subsequent calls to {!solve} will need to satisfy this clause. *)
 
-  val add_clause_l : t -> lit list -> dproof -> unit
+  val add_clause_l : t -> lit list -> proof_step -> unit
   (** Add a clause to the solver, given as a list. *)
 
   val assert_terms : t -> term list -> unit
@@ -1086,7 +1144,11 @@ module type SOLVER = sig
   type res =
     | Sat of Model.t (** Satisfiable *)
     | Unsat of {
-        unsat_core: unit -> lit Iter.t; (** subset of assumptions responsible for unsat *)
+        unsat_core: unit -> lit Iter.t;
+        (** Unsat core (subset of assumptions), or empty *)
+
+        unsat_proof_step : unit -> proof_step option;
+        (** Proof step for the empty clause *)
       } (** Unsatisfiable *)
     | Unknown of Unknown.t
     (** Unknown, obtained after a timeout, memory limit, etc. *)
@@ -1214,7 +1276,7 @@ end = struct
     else None
 
   let on_new_term self cc n (t:T.t) : unit =
-    Log.debugf 50 (fun k->k "@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);
+    (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*)
     let maybe_m, l = M.of_term cc n t in
     begin match maybe_m with
       | Some v ->

src/drup/sidekick_drup.ml

@@ -1,12 +1,12 @@
 
 (** DRUP trace checker.
 
-    This module provides a checker for DRUP traces, including step-by-step
+    This module provides a checker for DRUP traces, including proof_rule-by-proof_rule
     checking for traces that interleave DRUP steps with other kinds of steps.
 *)
 
 module Fmt = CCFormat
-module VecI32 = VecI32
+module VecSmallInt = VecSmallInt
 
 (* TODO: resolution proof construction, optionally *)
 
@@ -108,7 +108,7 @@ module Make() : S = struct
       let set = Vec.set
     end
     module Stack = struct
-      include VecI32
+      include VecSmallInt
       let create()=create()
     end
   end

src/lra/sidekick_arith_lra.ml

@@ -60,7 +60,7 @@ module type ARG = sig
   val has_ty_real : term -> bool
   (** Does this term have the type [Real] *)
 
-  val lemma_lra : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rule
 
   module Gensym : sig
     type t
@@ -82,6 +82,7 @@ module type S = sig
   type state
 
   val create : ?stat:Stat.t ->
+    A.S.P.t ->
     A.S.T.Term.store ->
     A.S.T.Ty.store ->
     state
@@ -140,6 +141,7 @@ module Make(A : ARG) : S with module A = A = struct
   type state = {
     tst: T.store;
     ty_st: Ty.store;
+    proof: SI.P.t;
     simps: T.t T.Tbl.t; (* cache *)
     gensym: A.Gensym.t;
     encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
@@ -150,8 +152,9 @@ module Make(A : ARG) : S with module A = A = struct
     stat_th_comb: int Stat.counter;
   }
 
-  let create ?(stat=Stat.create()) tst ty_st : state =
+  let create ?(stat=Stat.create()) proof tst ty_st : state =
     { tst; ty_st;
+      proof;
       simps=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
       encoded_eqs=T.Tbl.create 8;
@@ -232,18 +235,25 @@ module Make(A : ARG) : S with module A = A = struct
         );
         proxy
 
-  let add_clause_lra_ (module PA:SI.PREPROCESS_ACTS) lits =
-    let pr = A.lemma_lra (Iter.of_list lits) in
+  let add_clause_lra_ ?using (module PA:SI.PREPROCESS_ACTS) lits =
+    let pr = A.lemma_lra (Iter.of_list lits) PA.proof in
+    let pr = match using with
+      | None -> pr
+      | Some using -> SI.P.lemma_rw_clause pr ~res:(Iter.of_list lits) ~using PA.proof in
     PA.add_clause lits pr
 
   (* preprocess linear expressions away *)
   let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS)
-      (t:T.t) : T.t option =
+      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
     Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
     let tst = SI.tst si in
 
     (* preprocess subterm *)
-    let preproc_t t = SI.preprocess_term si (module PA) t in
+    let preproc_t ~steps t =
+      let u, pr = SI.preprocess_term si (module PA) t in
+      CCOpt.iter (fun s -> steps := s :: !steps) pr;
+      u
+    in
 
     (* tell the CC this term exists *)
     let declare_term_to_cc t =
@@ -262,9 +272,9 @@ module Make(A : ARG) : S with module A = A = struct
         T.Tbl.add self.encoded_eqs t ();
 
         (* encode [t <=> (u1 /\ u2)] *)
-        let lit_t = PA.mk_lit t in
-        let lit_u1 = PA.mk_lit u1 in
-        let lit_u2 = PA.mk_lit u2 in
+        let lit_t = PA.mk_lit_nopreproc t in
+        let lit_u1 = PA.mk_lit_nopreproc u1 in
+        let lit_u2 = PA.mk_lit_nopreproc u2 in
         add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
         add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
         add_clause_lra_ (module PA)
@@ -273,8 +283,9 @@ module Make(A : ARG) : S with module A = A = struct
       None
 
     | LRA_pred (pred, t1, t2) ->
-      let l1 = as_linexp ~f:preproc_t t1 in
-      let l2 = as_linexp ~f:preproc_t t2 in
+      let steps = ref [] in
+      let l1 = as_linexp ~f:(preproc_t ~steps) t1 in
+      let l2 = as_linexp ~f:(preproc_t ~steps) t2 in
       let le = LE.(l1 - l2) in
       let le_comb, le_const = LE.comb le, LE.const le in
       let le_const = A.Q.neg le_const in
@@ -284,6 +295,8 @@ module Make(A : ARG) : S with module A = A = struct
         | None, _ ->
           (* non trivial linexp, give it a fresh name in the simplex *)
           let proxy = var_encoding_comb self ~pre:"_le" le_comb in
+          let pr_def = SI.P.define_term proxy t PA.proof in
+          steps := pr_def :: !steps;
           declare_term_to_cc proxy;
 
           let op =
@@ -297,14 +310,13 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
           begin
-            let lit = PA.mk_lit new_t in
+            let lit = PA.mk_lit_nopreproc new_t in
             let constr = SimpSolver.Constraint.mk proxy op le_const in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
-          (* FIXME: emit proof: by def proxy + LRA *)
-          Some new_t
+          Some (new_t, Iter.of_list !steps)
 
         | Some (coeff, v), pred ->
           (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@@ -323,28 +335,31 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
           begin
-            let lit = PA.mk_lit new_t in
+            let lit = PA.mk_lit_nopreproc new_t in
             let constr = SimpSolver.Constraint.mk v op q in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
-          (* FIXME: preprocess proof *)
-          Some new_t
+          Some (new_t, Iter.of_list !steps)
       end
 
     | LRA_op _ | LRA_mult _ ->
-      let le = as_linexp ~f:preproc_t t in
+      let steps = ref [] in
+      let le = as_linexp ~f:(preproc_t ~steps) t in
       let le_comb, le_const = LE.comb le, LE.const le in
 
       if A.Q.(le_const = zero) then (
         (* if there is no constant, define [proxy] as [proxy := le_comb] and
            return [proxy] *)
         let proxy = var_encoding_comb self ~pre:"_le" le_comb in
+        begin
+          let pr_def = SI.P.define_term proxy t PA.proof in
+          steps := pr_def :: !steps;
+        end;
         declare_term_to_cc proxy;
 
-        (* FIXME: proof by def of proxy *)
-        Some proxy
+        Some (proxy, Iter.of_list !steps)
       ) else (
         (* a bit more complicated: we cannot just define [proxy := le_comb]
            because of the coefficient.
@@ -352,7 +367,14 @@ module Make(A : ARG) : S with module A = A = struct
            variable [proxy2 := le_comb - proxy]
            and asserting [proxy2 = -le_const] *)
         let proxy = fresh_term self ~pre:"_le" (T.ty t) in
+        begin
+          let pr_def = SI.P.define_term proxy t PA.proof in
+          steps := pr_def :: !steps;
+        end;
         let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
+        let pr_def2 =
+          SI.P.define_term proxy (A.mk_lra tst (LRA_op (Minus, t, proxy))) PA.proof
+        in
 
         SimpSolver.add_var self.simplex proxy;
         LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
@@ -367,29 +389,39 @@ module Make(A : ARG) : S with module A = A = struct
         declare_term_to_cc proxy;
         declare_term_to_cc proxy2;
 
-        PA.add_clause [
-          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
-        ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
-        PA.add_clause [
-          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
-        ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
+        add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
+          PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
+        ];
+        add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
+          PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
+        ];
 
-        (* FIXME: actual proof *)
-        Some proxy
+        Some (proxy, Iter.of_list !steps)
       )
 
     | LRA_other t when A.has_ty_real t -> None
     | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
       None
 
-  let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
+  let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
+
+    let proof_eq t u =
+      A.lemma_lra
+        (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof
+    in
+    let proof_bool t ~sign:b =
+      let lit = SI.Lit.atom ~sign:b self.tst t in
+      A.lemma_lra (Iter.return lit) self.proof
+    in
+
     match A.view_as_lra t with
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp_id t in
       if LE.is_const le then (
         let c = LE.const le in
-        (* FIXME: proof *)
-        Some (A.mk_lra self.tst (LRA_const c))
+        let u = A.mk_lra self.tst (LRA_const c) in
+        let pr = proof_eq t u in
+        Some (u, Iter.return pr)
       ) else None
     | LRA_pred (pred, l1, l2) ->
       let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@@ -403,8 +435,9 @@ module Make(A : ARG) : S with module A = A = struct
           | Eq -> A.Q.(c = zero)
           | Neq -> A.Q.(c <> zero)
         in
-        (* FIXME: proof *)
-        Some (A.mk_bool self.tst is_true)
+        let u = A.mk_bool self.tst is_true in
+        let pr = proof_bool t ~sign:is_true in
+        Some (u, Iter.return pr)
       ) else None
     | _ -> None
 
@@ -418,7 +451,7 @@ module Make(A : ARG) : S with module A = A = struct
       |> CCList.flat_map (Tag.to_lits si)
       |>  List.rev_map SI.Lit.neg
     in
-    let pr = A.lemma_lra (Iter.of_list confl) in
+    let pr = A.lemma_lra (Iter.of_list confl) (SI.proof si) in
     SI.raise_conflict si acts confl pr
 
   let on_propagate_ si acts lit ~reason =
@@ -428,7 +461,7 @@ module Make(A : ARG) : S with module A = A = struct
       SI.propagate si acts lit
         ~reason:(fun() ->
            let lits = CCList.flat_map (Tag.to_lits si) reason in
-           let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in
+           let pr = A.lemma_lra Iter.(cons lit (of_list lits)) (SI.proof si) in
            CCList.flat_map (Tag.to_lits si) reason, pr)
     | _ -> ()
 
@@ -594,7 +627,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   (* look for subterms of type Real, for they will need theory combination *)
   let on_subterm (self:state) _ (t:T.t) : unit =
-    Log.debugf 50 (fun k->k "lra: cc-on-subterm %a" T.pp t);
+    Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t);
     if A.has_ty_real t &&
        not (T.Tbl.mem self.needs_th_combination t) then (
       Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t);
@@ -604,7 +637,7 @@ module Make(A : ARG) : S with module A = A = struct
   let create_and_setup si =
     Log.debug 2 "(th-lra.setup)";
     let stat = SI.stats si in
-    let st = create ~stat (SI.tst si) (SI.ty_st si) in
+    let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
     SI.on_preprocess si (preproc_lra st);
     SI.on_final_check si (final_check_ st);

src/lra/simplex2.ml

@@ -138,7 +138,7 @@ end
 
 (* TODO(optim): page 14, paragraph 2: we could detect which variables occur in no
    atom after preprocessing; then these variables can be "inlined" (removed
-   by Gaussian elimination) as a preprocessing step, and this removes one column
+   by Gaussian elimination) as a preprocessing proof_rule, and this removes one column
    and maybe one row if it was basic. *)
 
 module Make(Q : RATIONAL)(Var: VAR)

src/lra/tests/test_simplex2.real.ml

@@ -98,7 +98,7 @@ module Step = struct
     let rec aux n vars acc =
       if n<=0 then return (List.rev acc)
       else (
-        let* vars, step =
+        let* vars, proof_rule =
           frequency @@ List.flatten [
             (* add a bound *)
             (match vars with
@@ -138,7 +138,7 @@ module Step = struct
             ) else []);
           ]
         in
-        aux (n-1) vars (step::acc)
+        aux (n-1) vars (proof_rule::acc)
       )
     in
     aux n [] []
@@ -162,7 +162,7 @@ end
 
 let on_propagate _ ~reason:_ = ()
 
-(* add a single step to the simplexe *)
+(* add a single proof_rule to the simplexe *)
 let add_step simplex (s:Step.t) : unit =
   begin match s with
     | Step.S_new_var v -> Spl.add_var simplex v
@@ -242,7 +242,7 @@ let prop_sound ?(inv=false) pb =
              let v_x = get_val x in
              if Q.(v_x < n) then failwith (spf "val=%s, n=%s"(q_dbg v_x)(q_dbg n))
          with e ->
-           QC.Test.fail_reportf "step failed: %a@.exn:@.%s@."
+           QC.Test.fail_reportf "proof_rule failed: %a@.exn:@.%s@."
              Step.pp_ s (Printexc.to_string e)
         );
         if inv then Spl._check_invariants simplex;

src/main/main.ml

@@ -30,6 +30,8 @@ let p_stat = ref false
 let p_gc_stat = ref false
 let p_progress = ref false
 let proof_file = ref ""
+let proof_store_memory = ref false
+let proof_store_file = ref ""
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -69,6 +71,8 @@ let argspec = Arg.align [
     "--stat", Arg.Set p_stat, " print statistics";
     "--proof", Arg.Set p_proof, " print proof";
     "--no-proof", Arg.Clear p_proof, " do not print proof";
+    "--proof-in-memory", Arg.Set proof_store_memory, " store temporary proof in memory";
+    "--proof-trace-file", Arg.Set_string proof_store_file, " 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";
     "--no-model", Arg.Clear p_model, " do not print model";
@@ -96,10 +100,42 @@ let check_limits () =
 let main_smt () : _ result =
   let module Proof = Sidekick_smtlib.Proof in
   let tst = Term.create ~size:4_096 () in
-  (* FIXME: use this to enable/disable actual proof
-    let store_proof = !check || !p_proof || !proof_file <> "" in
-     *)
-  let proof = Proof.create() in
+
+  let enable_proof_ = !check || !p_proof || !proof_file <> "" in
+  Log.debugf 1 (fun k->k"(@[proof-enable@ %B@])" enable_proof_);
+
+  (* call [k] with the name of a temporary proof file, and cleanup if necessary *)
+  let run_with_tmp_file k =
+    (* TODO: use memory writer if [!proof_store_memory] *)
+    if enable_proof_ then (
+      if !proof_store_file <> "" then (
+        let file = !proof_store_file in
+        k file
+      ) else (
+        CCIO.File.with_temp
+          ~temp_dir:"." ~prefix:".sidekick-proof" ~suffix:".dat" k
+      )
+    ) else (
+      k "/dev/null"
+    )
+  in
+
+  run_with_tmp_file @@ fun temp_proof_file ->
+  Log.debugf 1 (fun k->k"(@[temp-proof-file@ %S@])" temp_proof_file);
+
+  let config =
+    if enable_proof_ then (
+      Proof.Config.default
+      |> Proof.Config.enable true
+      |> Proof.Config.store_on_disk_at temp_proof_file
+    ) else (
+      Proof.Config.empty
+    )
+  in
+
+  (* main proof object *)
+  let proof = Proof.create ~config () in
+
   let solver =
     let theories =
       (* TODO: probes, to load only required theories *)
@@ -111,6 +147,7 @@ let main_smt () : _ result =
     in
     Process.Solver.create ~proof ~theories tst () ()
   in
+
   (* FIXME: emit an actual proof *)
   let proof_file = if !proof_file ="" then None else Some !proof_file in
   if !check then (
@@ -129,7 +166,7 @@ let main_smt () : _ result =
            Process.process_stmt
              ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf
              ~time:!time_limit ~memory:!size_limit
-             ~pp_model:!p_model
+             ~pp_model:!p_model ?proof_file
              ~check:!check ~progress:!p_progress
              solver)
         () input

src/main/pure_sat_solver.ml

@@ -48,12 +48,13 @@ end = struct
         oc: out_channel;
         close: (unit -> unit);
       }
+  type proof_step = unit
+  type proof_rule = t -> proof_step
+  module Step_vec = Vec_unit
 
-  type dproof = t -> unit
-
-  let[@inline] with_proof pr f = match pr with
-    | Dummy -> ()
-    | Inner _ | Out _ -> f pr
+  let[@inline] enabled pr = match pr with
+    | Dummy -> false
+    | Inner _ | Out _ -> true
 
   let[@inline] emit_lits_buf_ buf lits =
     lits (fun i -> bpf buf "%d " i)
@@ -68,14 +69,14 @@ end = struct
     | Out {oc;_} ->
       fpf oc "i "; emit_lits_out_ oc lits; fpf oc "0\n"
 
-  let emit_redundant_clause lits self =
+  let emit_redundant_clause lits ~hyps:_ self =
     match self with
     | Dummy -> ()
     | Inner buf ->
       bpf buf "r "; emit_lits_buf_ buf lits; bpf buf "0\n"
     | Out {oc;_} -> fpf oc "r "; emit_lits_out_ oc lits; fpf oc "0\n"
 
-  let del_clause lits self =
+  let del_clause () lits self =
     match self with
     | Dummy -> ()
     | Inner buf ->
@@ -83,6 +84,9 @@ end = struct
     | Out {oc; _}->
       fpf oc "d "; emit_lits_out_ oc lits; fpf oc "0\n"
 
+  let emit_unsat _ _ = ()
+  let emit_unsat_core _ _ = ()
+
   (* lifetime *)
 
   let dummy : t = Dummy
@@ -130,6 +134,7 @@ module Arg = struct
   type lit = Lit.t
   module Proof = Proof
   type proof = Proof.t
+  type proof_step = Proof.proof_step
 end
 
 module SAT = Sidekick_sat.Make_pure_sat(Arg)

src/proof-trace-dump/dune

@@ -0,0 +1,6 @@
+
+(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-dump/proof_trace_dump.ml

@@ -0,0 +1,45 @@
+
+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.bs=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/Storage.ml

@@ -0,0 +1,41 @@
+
+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 ->
+    begin 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
+    end

src/proof-trace/Storage.mli

@@ -0,0 +1,8 @@
+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/proof-trace/dune

@@ -0,0 +1,14 @@
+
+(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/proof-trace/proof_ser.bare

@@ -0,0 +1,128 @@
+
+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
+}
+
+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 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_true
+  | Fun_decl
+  | Expr_def
+  | Expr_bool
+  | Expr_if
+  | Expr_not
+  | Expr_eq
+  | Expr_app
+  )
+
+type Step {
+  id: ID
+  view: Step_view
+}
+
+

src/proof-trace/sidekick_base_proof_trace.ml

@@ -0,0 +1,11 @@
+
+(** 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/Proof.ml

@@ -1,536 +0,0 @@
-
-(*
-open Base_types
-
-module T = Term
-module Ty = Ty
-type term = T.t
-type ty = Ty.t
-
-type lit =
-  | L_eq of bool * term * term
-  | L_a of bool * term
-
-let lit_not = function
-  | L_eq (sign,a,b) -> L_eq(not sign,a,b)
-  | L_a (sign,t) -> L_a (not sign,t)
-
-let pp_lit_with ~pp_t out =
-  let strsign = function true -> "+" | false -> "-" in
-  function
-  | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u
-  | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t
-let pp_lit = pp_lit_with ~pp_t:Term.pp
-
-let lit_a t = L_a (true,t)
-let lit_na t = L_a (false,t)
-let lit_eq t u = L_eq (true,t,u)
-let lit_neq t u = L_eq (false,t,u)
-let lit_mk b t = L_a (b,t)
-let lit_sign = function L_a (b,_) | L_eq (b,_,_) -> b
-
-type clause = lit list
-
-type t =
-  | Unspecified
-  | Sorry (* NOTE: v. bad as we don't even specify the return *)
-  | Sorry_c of clause
-  | Named of string (* refers to previously defined clause *)
-  | Refl of term
-  | CC_lemma_imply of t list * term * term
-  | CC_lemma of clause
-  | Assertion of term
-  | Assertion_c of clause
-  | Drup_res of clause
-  | Hres of t * hres_step list
-  | Res of term * t * t
-  | Res1 of t * t
-  | DT_isa_split of ty * term list
-  | DT_isa_disj of ty * term * term
-  | DT_cstor_inj of Cstor.t * int * term list * term list (* [c t…=c u… |- t_i=u_i] *)
-  | Bool_true_is_true
-  | Bool_true_neq_false
-  | Bool_eq of term * term (* equal by pure boolean reasoning *)
-  | Bool_c of bool_c_name * term list (* boolean tautology *)
-  | Nn of t (* negation normalization *)
-  | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
-  | Ite_false of term
-  | LRA of clause
-  | Composite of {
-      (* some named (atomic) assumptions *)
-      assumptions: (string * lit) list;
-      steps: composite_step array; (* last step is the proof *)
-    }
-
-and bool_c_name = string
-
-and composite_step =
-  | S_step_c of {
-      name: string; (* name *)
-      res: clause; (* result of [proof] *)
-      proof: t; (* sub-proof *)
-    }
-  | S_define_t of term * term (* [const := t] *)
-  | S_define_t_name of string * term (* [const := t] *)
-
-  (* TODO: be able to name clauses, to be expanded at parsing.
-     note that this is not the same as [S_step_c] which defines an
-     explicit step with a conclusion and proofs that can be exploited
-     separately.
-
-     We could introduce that in Compress.rename…
-
-  | S_define_c of string * clause (* [name := c] *)
-   *)
-
-and hres_step =
-  | R of { pivot: term; p: t}
-  | R1 of t
-  | P of { lhs: term; rhs: term; p: t}
-  | P1 of t
-
-let r p ~pivot : hres_step = R { pivot; p }
-let r1 p = R1 p
-let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
-let p1 p = P1 p
-
-let stepc ~name res proof : composite_step = S_step_c {proof;name;res}
-let deft c rhs : composite_step = S_define_t (c,rhs)
-let deft_name c rhs : composite_step = S_define_t_name (c,rhs)
-
-let is_trivial_refl = function
-  | Refl _ -> true
-  | _ -> false
-
-let default=Unspecified
-let sorry_c c = Sorry_c (Iter.to_rev_list c)
-let sorry_c_l c = Sorry_c c
-let sorry = Sorry
-let refl t : t = Refl t
-let ref_by_name name : t = Named name
-let cc_lemma c : t = CC_lemma c
-let cc_imply_l l t u : t =
-  let l = List.filter (fun p -> not (is_trivial_refl p)) l in
-  match l with
-  | [] -> refl t (* only possible way [t=u] *)
-  | l -> CC_lemma_imply (l, t, u)
-let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u)
-let assertion t = Assertion t
-let assertion_c c = Assertion_c (Iter.to_rev_list c)
-let assertion_c_l c = Assertion_c c
-let composite_a ?(assms=[]) steps : t =
-  Composite {assumptions=assms; steps}
-let composite_l ?(assms=[]) steps : t =
-  Composite {assumptions=assms; steps=Array.of_list steps}
-let composite_iter ?(assms=[]) steps : t =
-  let steps = Iter.to_array steps in
-  Composite {assumptions=assms; steps}
-
-let isa_split ty i = DT_isa_split (ty, Iter.to_rev_list i)
-let isa_disj ty t u = DT_isa_disj (ty, t, u)
-let cstor_inj c i t u = DT_cstor_inj (c, i, t, u)
-
-let ite_true t = Ite_true t
-let ite_false t = Ite_false t
-let true_is_true : t = Bool_true_is_true
-let true_neq_false : t = Bool_true_neq_false
-let bool_eq a b : t = Bool_eq (a,b)
-let bool_c name c : t = Bool_c (name, c)
-let nn c : t = Nn c
-
-let drup_res c : t = Drup_res c
-let hres_l p l : t =
-  let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
-  if l=[] then p else Hres (p,l)
-let hres_iter c i : t = hres_l c (Iter.to_list i)
-let res ~pivot p1 p2 : t = Res (pivot,p1,p2)
-let res1 p1 p2 : t = Res1 (p1,p2)
-
-let lra_l c : t = LRA c
-let lra c = LRA (Iter.to_rev_list c)
-
-let iter_lit ~f_t = function
-  | L_eq (_,a,b) -> f_t a; f_t b
-  | L_a (_,t) -> f_t t
-
-let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit =
-  match p with
-  | Unspecified | Sorry -> ()
-  | Sorry_c c -> f_clause c
-  | Named _ -> ()
-  | Refl t -> f_t t
-  | CC_lemma_imply (ps, t, u) -> List.iter f_p ps; f_t t; f_t u
-  | CC_lemma c | Assertion_c c -> f_clause c
-  | Assertion t -> f_t t
-  | Drup_res c -> f_clause c
-  | Hres (i, l) ->
-    f_p i;
-    List.iter
-      (function
-        | R1 p -> f_p p
-        | P1 p -> f_p p
-        | R {pivot;p} -> f_p p; f_t pivot
-        | P {lhs;rhs;p} -> f_p p; f_t lhs; f_t rhs)
-      l
-  | Res (t,p1,p2) -> f_t t; f_p p1; f_p p2
-  | Res1 (p1,p2) -> f_p p1; f_p p2
-  | DT_isa_split (_, l) -> List.iter f_t l
-  | DT_isa_disj (_, t, u) -> f_t t; f_t u
-  | DT_cstor_inj (_, _c, ts, us) -> List.iter f_t ts; List.iter f_t us
-  | Bool_true_is_true | Bool_true_neq_false -> ()
-  | Bool_eq (t, u) -> f_t t; f_t u
-  | Bool_c (_, ts) -> List.iter f_t ts
-  | Nn p -> f_p p
-  | Ite_true t | Ite_false t -> f_t t
-  | LRA c -> f_clause c
-  | Composite { assumptions; steps } ->
-    List.iter (fun (_,lit) -> iter_lit ~f_t lit) assumptions;
-    Array.iter f_step steps;
-
-(** {2 Compress by making more sharing explicit} *)
-module Compress = struct
-  type 'a shared_status =
-    | First (* first occurrence of t *)
-    | Shared (* multiple occurrences observed *)
-    | Pre_named of 'a (* another step names it *)
-    | Named of 'a (* already named it *)
-
-  (* is [t] too small to be shared? *)
-  let rec is_small_ t =
-    let open Term_cell in
-    match T.view t with
-    | Bool _ -> true
-    | App_fun (_, a) -> IArray.is_empty a (* only constants are small *)
-    | Not u -> is_small_ u
-    | Eq (_, _) | Ite (_, _, _) -> false
-    | LRA _ -> false
-
-  type name = N_s of string | N_t of T.t
-  type sharing_info = {
-    terms: name shared_status T.Tbl.t; (* sharing for non-small terms *)
-  }
-
-  let no_sharing : sharing_info =
-    { terms = T.Tbl.create 8 }
-
-  (* traverse [p] and apply [f_t] to subterms (except to [c] in [c := rhs]) *)
-  let rec traverse_proof_ ?on_step ~f_t (p:t) : unit =
-    let recurse = traverse_proof_ ?on_step ~f_t in
-    let f_step s =
-      CCOpt.iter (fun f->f s) on_step;
-      traverse_step_ ~f_t s
-    in
-    iter_p p
-      ~f_t
-      ~f_clause:(traverse_clause_ ~f_t)
-      ~f_step
-      ~f_p:recurse
-  and traverse_step_ ~f_t = function
-    | S_define_t_name (_, rhs)
-    | S_define_t (_, rhs) -> f_t rhs
-    | S_step_c {name=_; res; proof} ->
-      traverse_clause_ ~f_t res; traverse_proof_ ~f_t proof
-  and traverse_clause_ ~f_t c : unit =
-    List.iter (iter_lit ~f_t) c
-
-  (** [find_sharing p] returns a {!sharing_info} which contains sharing information.
-      This information can be used during printing to reduce the
-      number of duplicated sub-terms that are printed. *)
-  let find_sharing p : sharing_info =
-    let self = {terms=T.Tbl.create 32} in
-
-    let traverse_t t =
-      T.iter_dag t
-        (fun u ->
-           if not (is_small_ u) then (
-             match T.Tbl.get self.terms u with
-             | None -> T.Tbl.add self.terms u First
-             | Some First -> T.Tbl.replace self.terms u Shared
-             | Some (Shared | Named _ | Pre_named _) -> ()
-           ))
-    in
-
-    (* if a term is already name, remember that, do not rename it *)
-    let on_step = function
-      | S_define_t_name (n,rhs) ->
-        T.Tbl.replace self.terms rhs (Pre_named (N_s n));
-      | S_define_t (c,rhs) ->
-        T.Tbl.replace self.terms rhs (Pre_named (N_t c));
-      | S_step_c _ -> ()
-    in
-
-    traverse_proof_ p ~on_step ~f_t:traverse_t;
-    self
-
-  (** [renaming sharing p] returns a new proof [p'] with more definitions.
-      It also modifies [sharing] so that the newly defined objects are
-      mapped to {!Named}, which we can use during printing. *)
-  let rename sharing (p:t) : t =
-    let n = ref 0 in
-    let new_name () = incr n; Printf.sprintf "$t%d" !n in
-
-    match p with
-    | Composite {assumptions; steps} ->
-      (* now traverse again, renaming some things on the fly *)
-      let new_steps = Vec.create() in
-
-      (* definitions we can skip *)
-      let skip_name_s = Hashtbl.create 8 in
-      let skip_name_t = T.Tbl.create 8 in
-
-      (* traverse [t], and if there's a subterm that is shared but
-         not named yet, name it now.
-      *)
-      let traverse_t t : unit =
-        T.iter_dag_with ~order:T.Iter_dag.Post t
-          (fun u ->
-              match T.Tbl.get sharing.terms u with
-              | Some Shared ->
-                (* shared, but not named yet *)
-                let name = new_name() in
-                Vec.push new_steps (deft_name name u);
-                T.Tbl.replace sharing.terms u (Named (N_s name))
-              | Some (Pre_named name) ->
-                (* named later in the file, declare it earlier to preserve
-                   a well ordering on definitions since we need it right now *)
-                Vec.push new_steps
-                  (match name with
-                   | N_s n -> Hashtbl.add skip_name_s n (); deft_name n u
-                   | N_t t -> T.Tbl.add skip_name_t t (); deft t u);
-                T.Tbl.replace sharing.terms u (Named name)
-              | _ -> ())
-      in
-
-      (* introduce naming in [step], then push it into {!new_steps} *)
-      let process_step_ step =
-        traverse_step_ step ~f_t:traverse_t;
-        (* see if we print the step or skip it *)
-        begin match step with
-          | S_define_t (t,_) when T.Tbl.mem skip_name_t t -> ()
-          | S_define_t_name (s,_) when Hashtbl.mem skip_name_s s -> ()
-          | _ ->
-            Vec.push new_steps step;
-        end
-      in
-
-      Array.iter process_step_ steps;
-      composite_a ~assms:assumptions (Vec.to_array new_steps)
-
-    | p -> p (* TODO: warning? *)
-end
-
-(** {2 Print to Quip}
-
-    Print to a format for checking by an external tool *)
-module Quip = struct
-  module type OUT = sig
-    type out
-    type printer = out -> unit
-    val l : printer list -> printer
-    val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer
-    (* list of steps, should be printed vertically if possible *)
-    val a : string -> printer
-  end
-
-  (*
-  TODO: make sure we print terms properly
-  *)
-
-  module Make(Out : OUT) = struct
-    open Out
-
-    let rec pp_t sharing (t:Term.t) : printer =
-      match T.Tbl.get sharing.Compress.terms t with
-      | Some (Named (N_s s)) -> a s(* use the newly introduced name *)
-      | Some (Named (N_t t)) -> pp_t sharing t (* use name *)
-      | _ -> pp_t_nonshare_root sharing t
-
-    and pp_t_nonshare_root sharing t =
-      let pp_t = pp_t sharing in
-      match Term.view t with
-      | Bool true -> a"true"
-      | Bool false -> a"false"
-      | App_fun (c, args) when IArray.is_empty args -> a (ID.to_string (id_of_fun c))
-      | App_fun (c, args) ->
-        l(a (ID.to_string (id_of_fun c)) :: IArray.to_list_map pp_t args)
-      | Eq (t,u) -> l[a"=";pp_t t;pp_t u]
-      | Not u -> l[a"not";pp_t u]
-      | Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3]
-      | LRA lra ->
-        begin match lra with
-          | LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2]
-          | LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2]
-          | LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x]
-          | LRA_const q -> a(Q.to_string q)
-          | LRA_simplex_var v -> pp_t v
-          | LRA_simplex_pred (v, op, q) ->
-            l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)]
-          | LRA_other x -> pp_t x
-        end
-
-    let rec pp_ty ty : printer =
-      match Ty.view ty with
-      | Ty_bool -> a"Bool"
-      | Ty_real -> a"Real"
-      | Ty_atomic {def;args=[];finite=_} ->
-        let id = Ty.id_of_def def in
-        a(ID.to_string id)
-      | Ty_atomic {def;args;finite=_} ->
-        let id = Ty.id_of_def def in
-        l(a(ID.to_string id)::List.map pp_ty args)
-
-    let pp_l ppx xs = l (List.map ppx xs)
-    let pp_lit ~pp_t lit = match lit with
-      | L_a(b,t) -> l[a(if b then"+" else"-");pp_t t]
-      | L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]]
-    let pp_cl ~pp_t c =
-      l (a "cl" :: List.map (pp_lit ~pp_t) c)
-
-    let rec pp_rec (sharing:Compress.sharing_info) (self:t) : printer =
-      let pp_rec = pp_rec sharing in
-      let pp_t = pp_t sharing in
-      let pp_cl = pp_cl ~pp_t in
-      match self with
-      | Unspecified -> a "<unspecified>"
-      | Named s -> l[a "@"; a s]
-      | CC_lemma c -> l[a"ccl"; pp_cl c]
-      | CC_lemma_imply (hyps,t,u) ->
-        l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u]
-      | Refl t -> l[a"refl"; pp_t t]
-      | Sorry -> a"sorry"
-      | Sorry_c c -> l[a"sorry-c"; pp_cl c]
-      | Bool_true_is_true -> a"t-is-t"
-      | Bool_true_neq_false -> a"t-ne-f"
-      | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2]
-      | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts)
-      | Nn p -> l[a"nn";pp_rec p]
-      | Assertion t -> l[a"assert";pp_t t]
-      | Assertion_c c -> l[a"assert-c";pp_cl c]
-      | Drup_res c -> l[a"drup";pp_cl c]
-      | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map (pp_hres_step sharing) steps)]
-      | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2]
-      | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2]
-      | DT_isa_split (ty,cs) ->
-        l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)]
-      | DT_isa_disj (ty,t,u) ->
-        l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u]
-      | DT_cstor_inj (c,i,ts,us) ->
-        l[a"dt.cstor.inj";a(ID.to_string(Cstor.id c));
-          a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)]
-      | Ite_true t -> l[a"ite-true"; pp_t t]
-      | Ite_false t -> l[a"ite-false"; pp_t t]
-      | LRA c -> l[a"lra";pp_cl c]
-      | Composite {steps; assumptions} ->
-        let pp_ass (n,ass) : printer =
-          l[a"assuming";a n;pp_lit ~pp_t ass] in
-        l[a"steps";l(List.map pp_ass assumptions);
-          iter_toplist (pp_composite_step sharing) (Iter.of_array steps)]
-
-    and pp_composite_step sharing step : printer =
-      let pp_t = pp_t sharing in
-      let pp_cl = pp_cl ~pp_t in
-      match step with
-      | S_step_c {name;res;proof} ->
-        l[a"stepc";a name;pp_cl res;pp_rec sharing proof]
-      | S_define_t (c,rhs) ->
-        (* disable sharing for [rhs], otherwise it'd print [c] *)
-        l[a"deft";pp_t c; pp_t_nonshare_root sharing rhs]
-      | S_define_t_name (c,rhs) ->
-        l[a"deft";a c; pp_t_nonshare_root sharing rhs]
-
-    (*
-      | S_define_t (name, t) ->
-        Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t
-    *)
-
-    and pp_hres_step sharing = function
-      | R {pivot; p} -> l[a"r";pp_t sharing pivot; pp_rec sharing p]
-      | R1 p -> l[a"r1";pp_rec sharing p]
-      | P {p; lhs; rhs} ->
-        l[a"r"; pp_t sharing lhs; pp_t sharing rhs; pp_rec sharing p]
-      | P1 p -> l[a"p1"; pp_rec sharing p]
-
-    (* toplevel wrapper *)
-    let pp self : printer =
-      (* find sharing *)
-      let sharing = Profile.with1 "proof.find-sharing" Compress.find_sharing self in
-      (* introduce names *)
-      let self = Profile.with2 "proof.rename" Compress.rename sharing self in
-      (* now print *)
-      l[a"quip"; a"1"; pp_rec sharing self]
-
-    let pp_debug ~sharing self : printer =
-      if sharing then pp self
-      else pp_rec Compress.no_sharing self
-  end
-
-  module Out_csexp = struct
-    type out = out_channel
-    type printer = out -> unit
-    let l prs out =
-      output_char out '(';
-      List.iter (fun x->x out) prs;
-      output_char out ')'
-    let a s out = Printf.fprintf out "%d:%s" (String.length s) s
-    let iter_toplist f it out =
-      output_char out '(';
-      it (fun x -> f x out);
-      output_char out ')'
-  end
-
-  module Out_sexp = struct
-    type out = out_channel
-    type printer = out -> unit
-    let l prs out =
-      output_char out '(';
-      List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs;
-      output_char out ')'
-    let a =
-      let buf = Buffer.create 128 in
-      fun s out ->
-        Buffer.clear buf;
-        CCSexp.to_buf buf (`Atom s);
-        Buffer.output_buffer out buf
-    let iter_toplist f it out =
-      output_char out '(';
-      let first=ref true in
-      it (fun x -> if !first then first := false else output_char out '\n'; f x out);
-      output_char out ')'
-  end
-
-  type out_format = Sexp | CSexp
-  let default_out_format = Sexp
-
-  let out_format_ = match Sys.getenv "PROOF_FMT" with
-    | "csexp" -> CSexp
-    | "sexp" -> Sexp
-    | s -> failwith (Printf.sprintf "unknown proof format %S" s)
-    | exception _ -> default_out_format
-
-  let output oc (self:t) : unit =
-    match out_format_ with
-    | Sexp -> let module M = Make(Out_sexp) in M.pp self oc
-    | CSexp ->
-      (* canonical sexp *)
-      let module M = Make(Out_csexp) in M.pp self oc
-end
-
-let pp_debug ~sharing out p =
-  let module Out = struct
-    type out = Format.formatter
-    type printer = out -> unit
-    let l prs out =
-      Fmt.fprintf out "(@[";
-      List.iteri(fun i x -> if i>0 then Fmt.fprintf out "@ "; x out) prs;
-      Fmt.fprintf out "@])"
-    let a s out = Fmt.string out s
-    let iter_toplist f it out =
-      Fmt.fprintf out "(@[<v>";
-      let first=ref true in
-      it (fun x -> if !first then first := false else Fmt.fprintf out "@ "; f x out);
-      Fmt.fprintf out "@])"
-  end
-  in
-  let module M = Quip.Make(Out) in
-  M.pp_debug ~sharing p out
-   *)

src/proof/Proof.mli

@@ -1,31 +0,0 @@
-
-(*
-(** Proofs of unsatisfiability
-
-    Proofs are used in sidekick when the problem is found {b unsatisfiable}.
-    A proof collects inferences made by the solver into a list of steps,
-    each with its own kind of justification (e.g. "by congruence"),
-    and outputs it in some kind of format.
-
-    Currently we target {{: https://c-cube.github.io/quip-book/ } Quip}
-    as an experimental proof backend.
-*)
-
-open Base_types
-
-include Sidekick_core.PROOF
-  with type term = Term.t
-   and type ty = Ty.t
-
-val isa_split : ty -> term Iter.t -> t
-val isa_disj : ty -> term -> term -> t
-val cstor_inj : Cstor.t -> int -> term list -> term list -> t
-
-val bool_eq : term -> term -> t
-val bool_c : string -> term list -> t
-val ite_true : term -> t
-val ite_false : term -> t
-
-val lra : lit Iter.t -> t
-val lra_l : lit list -> t
-   *)

src/quip/Proof.ml

@@ -0,0 +1,209 @@
+
+(** A reference to a previously defined object in the proof *)
+type id = int
+
+(** Representation of types *)
+module Ty = struct
+  type t =
+    | Bool
+    | Arrow of t array * t
+    | App of string * t array
+    | Ref of string
+
+  let equal : t -> t -> bool = (=)
+  let hash : t -> int = CCHash.poly
+  let[@inline] view (self:t) : t = self
+
+  let rec pp out (self:t) =
+    match self with
+    | Bool -> Fmt.string out "Bool"
+    | Arrow (args, ret) ->
+      Fmt.fprintf out "(@[->@ %a@ %a@])" (Util.pp_array pp) args pp ret
+    | App (c, [||]) -> Fmt.string out c
+    | App (c, args) ->
+      Fmt.fprintf out "(@[%s@ %a@])" c (Util.pp_array pp) args
+    | Ref name -> Fmt.fprintf out "(@@ %s)" name
+end
+
+module Fun = struct
+  type t = string
+  let pp out (self:t) = Fmt.string out self
+  let equal : t -> t -> bool = (=)
+  let hash : t -> int = CCHash.poly
+end
+
+module Cstor = Fun
+
+(** Representation of terms, with explicit sharing *)
+module T = struct
+  type t =
+    | Bool of bool
+    | App_fun of Fun.t * t array
+    | App_ho of t * t
+    | Ite of t * t * t
+    | Not of t
+    | Eq of t * t
+    | Ref of string
+  let[@inline] view (self:t) : t = self
+
+  let equal : t -> t -> bool = (=)
+  let hash : t -> int = CCHash.poly
+
+  let true_ : t = Bool true
+  let false_ : t = Bool false
+  let bool b = Bool b
+  let not_ = function Not x -> x | x -> Not x
+  let eq a b : t = Eq (a,b)
+  let ref name : t = Ref name
+  let app_fun f args : t = App_fun (f, args)
+  let const c = app_fun c [||]
+  let app_ho a b : t = App_ho (a,b)
+  let ite a b c : t = Ite (a,b,c)
+
+  let rec pp out = function
+    | Bool b -> Fmt.bool out b
+    | Ite (a,b,c) -> Fmt.fprintf out "(@[if@ %a@ %a@ %a@])" pp a pp b pp c
+    | App_fun (f,[||]) -> Fmt.string out f
+    | App_fun (f,args) ->
+      Fmt.fprintf out "(@[%a@ %a@])" Fun.pp f (Util.pp_array pp) args
+    | App_ho (f,a) -> Fmt.fprintf out "(@[%a@ %a@])" pp f pp a
+    | Not a -> Fmt.fprintf out "(@[not@ %a@])" pp a
+    | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b
+    | Ref name -> Fmt.fprintf out "(@@ %s)" name
+end
+
+type term = T.t
+type ty = Ty.t
+
+module Lit = struct
+  type t =
+    | L_eq of term * term
+    | L_a of bool * term
+
+  let pp_with ~pp_t out =
+    function
+    | L_eq (t,u) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp_t t pp_t u
+    | L_a (false,t) -> Fmt.fprintf out "(@[not@ %a@])" pp_t t
+    | L_a (true,t) -> pp_t out t
+
+  let pp = pp_with ~pp_t:T.pp
+
+  let eq t u = L_eq (t,u)
+  let mk b t = L_a (b,t)
+end
+
+type clause = Lit.t list
+
+type t =
+  | Unspecified
+  | Sorry (* NOTE: v. bad as we don't even specify the return *)
+  | Sorry_c of clause
+  | Named of string (* refers to previously defined clause *)
+  | Refl of term
+  | CC_lemma_imply of t list * term * term
+  | CC_lemma of clause
+  | Assertion of term
+  | Assertion_c of clause
+  | Hres of t * hres_step list
+  | Res of term * t * t
+  | Res1 of t * t
+  | Paramod1 of t * t
+  | Rup of clause * t list
+  | Clause_rw of {
+      res: clause;
+      c0: t;
+      using: t list; (** the rewriting equations/atoms *)
+    }
+  | DT_isa_split of ty * term list
+  | DT_isa_disj of ty * term * term
+  | DT_cstor_inj of Cstor.t * int * term list * term list (* [c t…=c u… |- t_i=u_i] *)
+  | Bool_true_is_true
+  | Bool_true_neq_false
+  | Bool_eq of term * term (* equal by pure boolean reasoning *)
+  | Bool_c of bool_c_name * term list (* boolean tautology *)
+  | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
+  | Ite_false of term
+  | LRA of clause
+  | Composite of {
+      (* some named (atomic) assumptions *)
+      assumptions: (string * Lit.t) list;
+      steps: composite_step array; (* last proof_rule is the proof *)
+    }
+
+and bool_c_name = string
+
+and composite_step =
+  | S_step_c of {
+      name: string; (* name *)
+      res: clause; (* result of [proof] *)
+      proof: t; (* sub-proof *)
+    }
+  | S_define_t of term * term (* [const := t] *)
+  | S_define_t_name of string * term (* [const := t] *)
+
+and hres_step =
+  | R of { pivot: term; p: t}
+  | R1 of t
+  | P of { lhs: term; rhs: term; p: t}
+  | P1 of t
+
+let r p ~pivot : hres_step = R { pivot; p }
+let r1 p = R1 p
+let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
+let p1 p = P1 p
+
+let stepc ~name res proof : composite_step = S_step_c {proof;name;res}
+let deft c rhs : composite_step = S_define_t (c,rhs)
+let deft_name c rhs : composite_step = S_define_t_name (c,rhs)
+
+let is_trivial_refl = function
+  | Refl _ -> true
+  | _ -> false
+
+let default=Unspecified
+let sorry_c c = Sorry_c (Iter.to_rev_list c)
+let sorry_c_l c = Sorry_c c
+let sorry = Sorry
+let refl t : t = Refl t
+let ref_by_name name : t = Named name
+let cc_lemma c : t = CC_lemma c
+let cc_imply_l l t u : t =
+  let l = List.filter (fun p -> not (is_trivial_refl p)) l in
+  match l with
+  | [] -> refl t (* only possible way [t=u] *)
+  | l -> CC_lemma_imply (l, t, u)
+let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u)
+let assertion t = Assertion t
+let assertion_c c = Assertion_c (Iter.to_rev_list c)
+let assertion_c_l c = Assertion_c c
+let rup c hyps : t = Rup (c,hyps)
+let clause_rw c0 ~res ~using : t = Clause_rw{res;c0;using}
+let composite_a ?(assms=[]) steps : t =
+  Composite {assumptions=assms; steps}
+let composite_l ?(assms=[]) steps : t =
+  Composite {assumptions=assms; steps=Array.of_list steps}
+let composite_iter ?(assms=[]) steps : t =
+  let steps = Iter.to_array steps in
+  Composite {assumptions=assms; steps}
+
+let isa_split ty i = DT_isa_split (ty, Iter.to_rev_list i)
+let isa_disj ty t u = DT_isa_disj (ty, t, u)
+let cstor_inj c i t u = DT_cstor_inj (c, i, t, u)
+
+let ite_true t = Ite_true t
+let ite_false t = Ite_false t
+let true_is_true : t = Bool_true_is_true
+let true_neq_false : t = Bool_true_neq_false
+let bool_eq a b : t = Bool_eq (a,b)
+let bool_c name c : t = Bool_c (name, c)
+
+let hres_l p l : t =
+  let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in
+  if l=[] then p else Hres (p,l)
+let hres_iter c i : t = hres_l c (Iter.to_list i)
+let res ~pivot p1 p2 : t = Res (pivot,p1,p2)
+let res1 p1 p2 : t = Res1 (p1,p2)
+let paramod1 p1 p2 : t = Paramod1(p1,p2)
+
+let lra_l c : t = LRA c
+let lra c = LRA (Iter.to_rev_list c)

src/quip/Sidekick_quip.ml

@@ -0,0 +1,213 @@
+
+module Proof = Proof
+open Proof
+
+type t = Proof.t
+
+(** {2 Print to Quip}
+
+    Print to a format for checking by an external tool *)
+
+module type OUT = sig
+  type out
+  type printer = out -> unit
+  val l : printer list -> printer
+  val iter_toplist : ('a -> printer) -> 'a Iter.t -> printer
+  (* list of steps, should be printed vertically if possible *)
+  val a : string -> printer
+end
+
+(** Build a printer that uses {!Out} *)
+module Make_printer(Out : OUT) = struct
+  open Out
+
+  let rec pp_t t =
+    match T.view t with
+    | T.Bool true -> a"true"
+    | T.Bool false -> a"false"
+    | T.App_fun (c, [||]) -> a c
+    | T.App_fun (c, args) ->
+      l(a c :: Util.array_to_list_map pp_t args)
+    | T.Ref name -> l[a"@"; a name]
+    | T.App_ho(f,a) -> l[pp_t f;pp_t a]
+    | T.Eq (t,u) -> l[a"=";pp_t t;pp_t u]
+    | T.Not u -> l[a"not";pp_t u]
+    | T.Ite (t1,t2,t3) -> l[a"ite";pp_t t1;pp_t t2;pp_t t3]
+    (*
+    | T.LRA lra ->
+      begin match lra with
+        | LRA_pred (p, t1, t2) -> l[a (string_of_lra_pred p); pp_t t1; pp_t t2]
+        | LRA_op (p, t1, t2) -> l[a (string_of_lra_op p); pp_t t1; pp_t t2]
+        | LRA_mult (n, x) -> l[a"lra.*"; a(Q.to_string n);pp_t x]
+        | LRA_const q -> a(Q.to_string q)
+        | LRA_simplex_var v -> pp_t v
+        | LRA_simplex_pred (v, op, q) ->
+          l[a(Sidekick_arith_lra.S_op.to_string op); pp_t v; a(Q.to_string q)]
+        | LRA_other x -> pp_t x
+      end
+       *)
+
+  let rec pp_ty ty : printer =
+    match Ty.view ty with
+    | Ty.Bool -> a"Bool"
+    | Ty.App (c,[||]) ->
+      a c
+    | Ty.App (c,args) ->
+      l(a c::Util.array_to_list_map pp_ty args)
+    | Ty.Ref name -> l[a "@"; a name]
+    | Ty.Arrow (args,b) ->
+      l (a "->" :: Util.array_to_list_map pp_ty args @ [pp_ty b])
+
+  let pp_l ppx xs = l (List.map ppx xs)
+  let pp_lit ~pp_t lit = match lit with
+    | Lit.L_a(true,t) -> pp_t t
+    | Lit.L_a(false,t) -> l[a"not";pp_t t]
+    | Lit.L_eq(t,u) -> l[a"=";pp_t t;pp_t u]
+  let pp_cl ~pp_t c =
+    l (a "cl" :: List.map (pp_lit ~pp_t) c)
+
+  let rec pp_rec (self:t) : printer =
+    let pp_cl = pp_cl ~pp_t in
+    match self with
+    | Unspecified -> a "<unspecified>"
+    | Named s -> l[a "@"; a s]
+    | CC_lemma c -> l[a"ccl"; pp_cl c]
+    | CC_lemma_imply (hyps,t,u) ->
+      l[a"ccli"; pp_l pp_rec hyps; pp_t t; pp_t u]
+    | Refl t -> l[a"refl"; pp_t t]
+    | Sorry -> a"sorry"
+    | Sorry_c c -> l[a"sorry-c"; pp_cl c]
+    | Bool_true_is_true -> a"t-is-t"
+    | Bool_true_neq_false -> a"t-ne-f"
+    | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2]
+    | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts)
+    | Assertion t -> l[a"assert";pp_t t]
+    | Assertion_c c -> l[a"assert-c";pp_cl c]
+    | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map pp_hres_step steps)]
+    | Res (t,p1,p2) -> l[a"r";pp_t t;pp_rec p1;pp_rec p2]
+    | Res1 (p1,p2) -> l[a"r1";pp_rec p1;pp_rec p2]
+    | Paramod1 (p1,p2) -> l[a"p1";pp_rec p1;pp_rec p2]
+    | Rup (c, hyps) ->
+      l[a"rup";pp_cl c;l(List.map pp_rec hyps)]
+    | Clause_rw{res; c0; using} ->
+      l[a"clause-rw";pp_cl res;pp_rec c0;l(List.map pp_rec using)]
+    | DT_isa_split (ty,cs) ->
+      l[a"dt.isa.split";pp_ty ty;l(a"cases"::List.map pp_t cs)]
+    | DT_isa_disj (ty,t,u) ->
+      l[a"dt.isa.disj";pp_ty ty;pp_t t;pp_t u]
+    | DT_cstor_inj (c,i,ts,us) ->
+      l[a"dt.cstor.inj";a c;
+        a(string_of_int i); l(List.map pp_t ts); l(List.map pp_t us)]
+    | Ite_true t -> l[a"ite-true"; pp_t t]
+    | Ite_false t -> l[a"ite-false"; pp_t t]
+    | LRA c -> l[a"lra";pp_cl c]
+    | Composite {steps; assumptions} ->
+      let pp_ass (n,ass) : printer =
+        l[a"assuming";a n;pp_lit ~pp_t ass] in
+      l[a"steps";l(List.map pp_ass assumptions);
+        iter_toplist pp_composite_step (Iter.of_array steps)]
+
+  and pp_composite_step proof_rule : printer =
+    let pp_cl = pp_cl ~pp_t in
+    match proof_rule with
+    | S_step_c {name;res;proof} ->
+      l[a"stepc";a name;pp_cl res;pp_rec proof]
+    | S_define_t (c,rhs) ->
+      (* disable sharing for [rhs], otherwise it'd print [c] *)
+      l[a"deft";pp_t c; pp_t rhs]
+    | S_define_t_name (c,rhs) ->
+      l[a"deft";a c; pp_t rhs]
+
+  (*
+    | S_define_t (name, t) ->
+      Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t
+  *)
+
+  and pp_hres_step = function
+    | R {pivot; p} -> l[a"r";pp_t pivot; pp_rec p]
+    | R1 p -> l[a"r1";pp_rec p]
+    | P {p; lhs; rhs} ->
+      l[a"r"; pp_t lhs; pp_t rhs; pp_rec p]
+    | P1 p -> l[a"p1"; pp_rec p]
+
+  (* toplevel wrapper *)
+  let pp self : printer =
+    fun out ->
+    Profile.with_ "quip.print" @@ fun () ->
+    l[a"quip"; a"1"; pp_rec self] out
+
+  let pp_debug self : printer = pp self
+end
+
+(** Output to canonical S-expressions *)
+module Out_csexp = struct
+  type out = out_channel
+  type printer = out -> unit
+  let l prs out =
+    output_char out '(';
+    List.iter (fun x->x out) prs;
+    output_char out ')'
+  let a s out = Printf.fprintf out "%d:%s" (String.length s) s
+  let iter_toplist f it out =
+    output_char out '(';
+    it (fun x -> f x out);
+    output_char out ')'
+end
+
+(** Output to classic S-expressions *)
+module Out_sexp = struct
+  type out = out_channel
+  type printer = out -> unit
+  let l prs out =
+    output_char out '(';
+    List.iteri (fun i x->if i>0 then output_char out ' ';x out) prs;
+    output_char out ')'
+  let a =
+    let buf = Buffer.create 128 in
+    fun s out ->
+      Buffer.clear buf;
+      CCSexp.to_buf buf (`Atom s);
+      Buffer.output_buffer out buf
+  let iter_toplist f it out =
+    output_char out '(';
+    let first=ref true in
+    it (fun x -> if !first then first := false else output_char out '\n'; f x out);
+    output_char out ')'
+end
+
+type out_format = Sexp | CSexp
+let string_of_out_format = function
+  | Sexp -> "sexp"
+  | CSexp -> "csexp"
+let pp_out_format out f = Fmt.string out (string_of_out_format f)
+
+let default_out_format = Sexp
+
+let output ?(fmt=Sexp) oc (self:t) : unit =
+  match fmt with
+  | Sexp ->
+    let module M = Make_printer(Out_sexp) in
+    M.pp self oc
+  | CSexp ->
+    let module M = Make_printer(Out_csexp) in
+    M.pp self oc
+
+let pp_debug out p =
+  let module Out = struct
+    type out = Format.formatter
+    type printer = out -> unit
+    let l prs out =
+      Fmt.fprintf out "(@[";
+      List.iteri(fun i x -> if i>0 then Fmt.fprintf out "@ "; x out) prs;
+      Fmt.fprintf out "@])"
+    let a s out = Fmt.string out s
+    let iter_toplist f it out =
+      Fmt.fprintf out "(@[<v>";
+      let first=ref true in
+      it (fun x -> if !first then first := false else Fmt.fprintf out "@ "; f x out);
+      Fmt.fprintf out "@])"
+  end
+  in
+  let module M = Make_printer(Out) in
+  M.pp_debug p out
+

src/quip/Sidekick_quip.mli

@@ -0,0 +1,25 @@
+
+(** Proofs of unsatisfiability in the Quip proof format..
+
+    This targets {{: https://c-cube.github.io/quip-book/ } Quip}
+    as an {b experimental} proof backend.
+*)
+
+module Proof = Proof
+
+type t = Proof.t
+(** The state holding the whole proof. *)
+
+(** What format to use to serialize the proof? *)
+type out_format =
+  | Sexp
+    (** S-expressions *)
+
+  | CSexp
+    (** Canonical S-expressions *)
+
+val pp_out_format : out_format Fmt.printer
+
+val output : ?fmt:out_format -> out_channel -> t -> unit
+
+val pp_debug : t Fmt.printer

src/quip/dune

@@ -0,0 +1,6 @@
+
+(library
+  (name sidekick_quip)
+  (public_name sidekick.quip)
+  (libraries sidekick.util)
+  (flags :standard -warn-error -a+8 -w -37 -open Sidekick_util))

src/sat/Heap.ml

@@ -9,14 +9,14 @@ module Make(Elt : RANKED) = struct
 
   type t = {
     store : elt_store;
-    heap : VecI32.t; (* vec of elements *)
+    heap : VecSmallInt.t; (* vec of elements *)
   }
 
   let _absent_index = -1
 
   let create store : t =
     { store;
-      heap = VecI32.create(); }
+      heap = VecSmallInt.create(); }
 
   let[@inline] left i = (i lsl 1) + 1 (* i*2 + 1 *)
   let[@inline] right i = (i + 1) lsl 1 (* (i+1)*2 *)
@@ -24,15 +24,15 @@ module Make(Elt : RANKED) = struct
 
   (*
   let rec heap_property cmp ({heap=heap} as s) i =
-    i >= (VecI32.size heap)  ||
+    i >= (VecSmallInt.size heap)  ||
       ((i = 0 || not(cmp (Vec. get heap i) (Vec.get heap (parent i))))
        && heap_property cmp s (left i) && heap_property cmp s (right i))
 
   let heap_property cmp s = heap_property cmp s 1
   *)
 
-  let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecI32.get self.heap i)
-  let[@inline] set_elt_ self i elt = VecI32.set self.heap i (elt:Elt.t:>int)
+  let[@inline] get_elt_ self i = Elt.of_int_unsafe (VecSmallInt.get self.heap i)
+  let[@inline] set_elt_ self i elt = VecSmallInt.set self.heap i (elt:Elt.t:>int)
 
   (* [elt] is above or at its expected position. Move it up the heap
      (towards high indices) to restore the heap property *)
@@ -49,7 +49,7 @@ module Make(Elt : RANKED) = struct
     Elt.set_heap_idx self.store elt !i
 
   let percolate_down (self:t) (elt:Elt.t): unit =
-    let sz = VecI32.size self.heap in
+    let sz = VecSmallInt.size self.heap in
     let li = ref (left (Elt.heap_idx self.store elt)) in
     let ri = ref (right (Elt.heap_idx self.store elt)) in
     let i = ref (Elt.heap_idx self.store elt) in
@@ -85,7 +85,7 @@ module Make(Elt : RANKED) = struct
 
   let filter (self:t) filt : unit =
     let j = ref 0 in
-    let lim = VecI32.size self.heap in
+    let lim = VecSmallInt.size self.heap in
     for i = 0 to lim - 1 do
       if filt (get_elt_ self i) then (
         set_elt_ self !j (get_elt_ self i);
@@ -95,24 +95,24 @@ module Make(Elt : RANKED) = struct
         Elt.set_heap_idx self.store (get_elt_ self i) _absent_index;
       );
     done;
-    VecI32.shrink self.heap (lim - !j);
+    VecSmallInt.shrink self.heap (lim - !j);
     for i = (lim / 2) - 1 downto 0 do
       percolate_down self (get_elt_ self i)
     done
 
-  let[@inline] size s = VecI32.size s.heap
-  let[@inline] is_empty s = VecI32.is_empty s.heap
+  let[@inline] size s = VecSmallInt.size s.heap
+  let[@inline] is_empty s = VecSmallInt.is_empty s.heap
 
   let clear self : unit =
-    VecI32.iter self.heap
+    VecSmallInt.iter self.heap
       ~f:(fun e -> Elt.set_heap_idx self.store (Elt.of_int_unsafe e) _absent_index);
-    VecI32.clear self.heap;
+    VecSmallInt.clear self.heap;
     ()
 
   let insert self elt =
     if not (in_heap self elt) then (
-      Elt.set_heap_idx self.store elt (VecI32.size self.heap);
-      VecI32.push self.heap (elt:Elt.t:>int);
+      Elt.set_heap_idx self.store elt (VecSmallInt.size self.heap);
+      VecSmallInt.push self.heap (elt:Elt.t:>int);
       percolate_up self elt;
     )
 
@@ -131,20 +131,20 @@ module Make(Elt : RANKED) = struct
   *)
 
   let remove_min self =
-    match VecI32.size self.heap with
+    match VecSmallInt.size self.heap with
     | 0 -> raise Not_found
     | 1 ->
-      let x = Elt.of_int_unsafe (VecI32.pop self.heap) in
+      let x = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in
       Elt.set_heap_idx self.store x _absent_index;
       x
     | _ ->
       let x = get_elt_ self 0 in
-      let new_hd = Elt.of_int_unsafe (VecI32.pop self.heap) in (* heap.last() *)
+      let new_hd = Elt.of_int_unsafe (VecSmallInt.pop self.heap) in (* heap.last() *)
       set_elt_ self 0 new_hd;
       Elt.set_heap_idx self.store x _absent_index;
       Elt.set_heap_idx self.store new_hd 0;
       (* enforce heap property again *)
-      if VecI32.size self.heap > 1 then (
+      if VecSmallInt.size self.heap > 1 then (
         percolate_down self new_hd;
       );
       x

src/sat/Sidekick_sat.ml

@@ -17,7 +17,7 @@ type ('lit, 'proof) reason = ('lit, 'proof) Solver_intf.reason =
   | Consequence of (unit -> 'lit list * 'proof) [@@unboxed]
 
 module type ACTS = Solver_intf.ACTS
-type ('lit, 'proof) acts = ('lit, 'proof) Solver_intf.acts
+type ('lit, 'proof, 'proof_step) acts = ('lit, 'proof, 'proof_step) Solver_intf.acts
 
 type negated = bool
 

src/sat/Solver.mli

@@ -6,6 +6,7 @@ module Make_pure_sat(Th: Solver_intf.PLUGIN_SAT)
   : S with type lit = Th.lit
        and module Lit = Th.Lit
        and type proof = Th.proof
+       and type proof_step = Th.proof_step
        and module Proof = Th.Proof
        and type theory = unit
 
@@ -13,5 +14,6 @@ module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T)
   : S with type lit = Th.lit
        and module Lit = Th.Lit
        and type proof = Th.proof
+       and type proof_step = Th.proof_step
        and module Proof = Th.Proof
        and type theory = Th.t

src/sat/Solver_intf.ml

@@ -40,17 +40,21 @@ type 'form sat_state = (module SAT_STATE with type lit = 'form)
 module type UNSAT_STATE = sig
   type lit
   type clause
+  type proof
 
   val unsat_conflict : unit -> clause
   (** Returns the unsat clause found at the toplevel *)
 
   val unsat_assumptions : unit -> lit Iter.t
   (** Subset of assumptions responsible for "unsat" *)
+
+  val unsat_proof : unit -> proof
 end
 
-type ('lit, 'clause) unsat_state =
+type ('lit, 'clause, 'proof) unsat_state =
   (module UNSAT_STATE with type lit = 'lit
-                       and type clause = 'clause)
+                       and type clause = 'clause
+                       and type proof = 'proof)
 (** The type of values returned when the solver reaches an UNSAT state. *)
 
 type same_sign = bool
@@ -98,8 +102,10 @@ end
 module type ACTS = sig
   type lit
   type proof
+  type proof_step
   type clause_pool_id = Clause_pool_id.t
-  type dproof = proof -> unit
+
+  val proof : proof
 
   val iter_assumptions: (lit -> unit) -> unit
   (** Traverse the new assumptions on the boolean trail. *)
@@ -111,7 +117,7 @@ module type ACTS = sig
   (** Map the given lit to an internal atom, which will be decided by the
       SAT solver. *)
 
-  val add_clause: ?keep:bool -> lit list -> dproof -> unit
+  val add_clause: ?keep:bool -> lit list -> proof_step -> unit
   (** Add a clause to the solver.
       @param keep if true, the clause will be kept by the solver.
         Otherwise the solver is allowed to GC the clause and propose this
@@ -119,16 +125,16 @@ module type ACTS = sig
       - [C_use_allocator alloc] puts the clause in the given allocator.
   *)
 
-  val add_clause_in_pool : pool:clause_pool_id -> lit list -> dproof -> unit
+  val add_clause_in_pool : pool:clause_pool_id -> lit list -> proof_step -> unit
   (** Like {!add_clause} but uses a custom clause pool for the clause,
       with its own lifetime. *)
 
-  val raise_conflict: lit list -> dproof -> 'b
+  val raise_conflict: lit list -> proof_step -> 'b
   (** Raise a conflict, yielding control back to the solver.
       The list of atoms must be a valid theory lemma that is false in the
       current trail. *)
 
-  val propagate: lit -> (lit, dproof) reason -> unit
+  val propagate: lit -> (lit, proof_step) reason -> unit
   (** Propagate a lit, i.e. the theory can evaluate the lit to be true
       (see the definition of {!type:eval_res} *)
 
@@ -138,9 +144,10 @@ module type ACTS = sig
       Useful for theory combination. This will be undone on backtracking. *)
 end
 
-type ('lit, 'proof) acts =
+type ('lit, 'proof, 'proof_step) acts =
   (module ACTS with type lit = 'lit
-                and type proof = 'proof)
+                and type proof = 'proof
+                and type proof_step = 'proof_step)
 (** The type for a slice of assertions to assume/propagate in the theory. *)
 
 exception No_proof
@@ -184,9 +191,13 @@ module type PLUGIN_CDCL_T = sig
   type proof
   (** Proof storage/recording *)
 
+  type proof_step
+  (** Identifier for a clause precendently added/proved *)
+
   module Proof : PROOF
     with type t = proof
      and type lit = lit
+     and type proof_step = proof_step
 
   val push_level : t -> unit
   (** Create a new backtrack level *)
@@ -194,12 +205,12 @@ module type PLUGIN_CDCL_T = sig
   val pop_levels : t -> int -> unit
   (** Pop [n] levels of the theory *)
 
-  val partial_check : t -> (lit, proof) acts -> unit
+  val partial_check : t -> (lit, proof, proof_step) acts -> unit
   (** Assume the lits in the slice, possibly using the [slice]
       to push new lits to be propagated or to raising a conflict or to add
       new lemmas. *)
 
-  val final_check : t -> (lit, proof) acts -> unit
+  val final_check : t -> (lit, proof, proof_step) acts -> unit
   (** Called at the end of the search in case a model has been found.
       If no new clause is pushed, then proof search ends and "sat" is returned;
       if lemmas are added, search is resumed;
@@ -212,7 +223,11 @@ module type PLUGIN_SAT = sig
   module Lit : LIT with type t = lit
 
   type proof
-  module Proof : PROOF with type t = proof and type lit = lit
+  type proof_step
+  module Proof : PROOF
+    with type t = proof
+     and type lit = lit
+     and type proof_step = proof_step
 end
 
 (** The external interface implemented by safe solvers, such as the one
@@ -236,7 +251,7 @@ module type S = sig
   type proof
   (** A representation of a full proof *)
 
-  type dproof = proof -> unit
+  type proof_step
 
   type solver
   (** The main solver type. *)
@@ -330,7 +345,7 @@ module type S = sig
   (** Result type for the solver *)
   type res =
     | Sat of lit sat_state (** Returned when the solver reaches SAT, with a model *)
-    | Unsat of (lit,clause) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
+    | Unsat of (lit,clause,proof_step) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
 
   exception UndecidedLit
   (** Exception raised by the evaluating functions when a literal
@@ -342,10 +357,10 @@ module type S = sig
   (** Add the list of clauses to the current set of assumptions.
       Modifies the sat solver state in place. *)
 
-  val add_clause : t -> lit list -> dproof -> unit
+  val add_clause : t -> lit list -> proof_step -> unit
   (** Lower level addition of clauses *)
 
-  val add_clause_a : t -> lit array -> dproof -> unit
+  val add_clause_a : t -> lit array -> proof_step -> unit
   (** Lower level addition of clauses *)
 
   val add_input_clause : t -> lit list -> unit
@@ -354,10 +369,10 @@ module type S = sig
   val add_input_clause_a : t -> lit array -> unit
   (** Like {!add_clause_a} but with justification of being an input clause *)
 
-  val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> dproof -> unit
+  val add_clause_in_pool : t -> pool:clause_pool_id -> lit list -> proof_step -> unit
   (** Like {!add_clause} but using a specific clause pool *)
 
-  val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> dproof -> unit
+  val add_clause_a_in_pool : t -> pool:clause_pool_id -> lit array -> proof_step -> unit
   (** Like {!add_clause_a} but using a specific clause pool *)
 
   (* TODO: API to push/pop/clear assumptions from an inner vector *)

src/smt-solver/Sidekick_smt_solver.ml

@@ -13,9 +13,11 @@ module type ARG = sig
   module T : TERM
   module Lit : LIT with module T = T
   type proof
+  type proof_step
   module P : PROOF
     with type term = T.Term.t
      and type t = proof
+     and type proof_step = proof_step
      and type lit = Lit.t
 
   val cc_view : T.Term.t -> (T.Fun.t, T.Term.t, T.Term.t Iter.t) CC_view.t
@@ -32,6 +34,7 @@ module Make(A : ARG)
   : S
     with module T = A.T
      and type proof = A.proof
+     and type proof_step = A.proof_step
      and module Lit = A.Lit
      and module P = A.P
 = struct
@@ -43,11 +46,11 @@ module Make(A : ARG)
   type term = Term.t
   type ty = Ty.t
   type proof = A.proof
-  type dproof = proof -> unit
+  type proof_step = A.proof_step
   type lit = Lit.t
 
   (* actions from the sat solver *)
-  type sat_acts = (lit, proof) Sidekick_sat.acts
+  type sat_acts = (lit, proof, proof_step) Sidekick_sat.acts
 
   (* the full argument to the congruence closure *)
   module CC_actions = struct
@@ -55,6 +58,7 @@ module Make(A : ARG)
     module P = P
     module Lit = Lit
     type nonrec proof = proof
+    type nonrec proof_step = proof_step
     let cc_view = A.cc_view
 
     module Actions = struct
@@ -62,11 +66,14 @@ module Make(A : ARG)
       module P = P
       module Lit = Lit
       type nonrec proof = proof
-      type dproof = proof -> unit
+      type nonrec proof_step = proof_step
       type t = sat_acts
-      let[@inline] raise_conflict (a:t) lits (dp:dproof) =
+      let[@inline] proof (a:t) =
         let (module A) = a in
-        A.raise_conflict lits dp
+        A.proof
+      let[@inline] raise_conflict (a:t) lits (pr:proof_step) =
+        let (module A) = a in
+        A.raise_conflict lits pr
       let[@inline] propagate (a:t) lit ~reason =
         let (module A) = a in
         let reason = Sidekick_sat.Consequence reason in
@@ -85,7 +92,7 @@ module Make(A : ARG)
     module CC = CC
     module N = CC.N
     type nonrec proof = proof
-    type dproof = proof -> unit
+    type nonrec proof_step = proof_step
     type term = Term.t
     type ty = Ty.t
     type lit = Lit.t
@@ -110,57 +117,79 @@ module Make(A : ARG)
         ty_st: ty_store;
         proof: proof;
         mutable hooks: hook list;
-        cache: Term.t Term.Tbl.t;
+        (* store [t --> u by proof_steps] in the cache.
+           We use a bag for the proof steps because it gives us structural
+           sharing of subproofs. *)
+        cache: (Term.t * proof_step Bag.t) Term.Tbl.t;
       }
-      and hook = t -> term -> term option
+
+      and hook = t -> term -> (term * proof_step Iter.t) option
 
       let create tst ty_st ~proof : t =
         {tst; ty_st; proof; hooks=[]; cache=Term.Tbl.create 32;}
 
       let[@inline] tst self = self.tst
       let[@inline] ty_st self = self.ty_st
-      let[@inline] with_proof self f = P.with_proof self.proof f
+      let[@inline] proof self = self.proof
       let add_hook self f = self.hooks <- f :: self.hooks
       let clear self = Term.Tbl.clear self.cache
 
-      let normalize (self:t) (t:Term.t) : Term.t option =
+      let normalize (self:t) (t:Term.t) : (Term.t * proof_step) option =
         (* compute and cache normal form of [t] *)
-        let rec aux t : Term.t =
+        let rec loop t : Term.t * _ Bag.t =
           match Term.Tbl.find self.cache t with
-          | u -> u
+          | res -> res
           | exception Not_found ->
-            let u = aux_rec t self.hooks in
-            Term.Tbl.add self.cache t u;
-            u
+            let steps_u = ref Bag.empty in
+            let u = aux_rec ~steps:steps_u t self.hooks in
+            Term.Tbl.add self.cache t (u, !steps_u);
+            u, !steps_u
+
+        and loop_add ~steps t =
+          let u, pr_u = loop t in
+          steps := Bag.append !steps pr_u;
+          u
+
         (* try each function in [hooks] successively, and rewrite subterms *)
-        and aux_rec t hooks = match hooks with
+        and aux_rec ~steps t hooks : Term.t =
+          match hooks with
           | [] ->
-            let u = Term.map_shallow self.tst aux t in
-            if Term.equal t u then t else aux u
+            let u = Term.map_shallow self.tst (loop_add ~steps) t in
+            if Term.equal t u
+            then t
+            else loop_add ~steps u
           | h :: hooks_tl ->
             match h self t with
-            | None -> aux_rec t hooks_tl
-            | Some u when Term.equal t u -> aux_rec t hooks_tl
-            | Some u -> aux u (* fixpoint *)
+            | None -> aux_rec ~steps t hooks_tl
+            | Some (u, _) when Term.equal t u -> aux_rec ~steps t hooks_tl
+            | Some (u, pr_u) ->
+              let bag_u = Bag.of_iter pr_u in
+              steps := Bag.append !steps bag_u;
+              let v, pr_v = loop u in (* fixpoint *)
+              steps := Bag.append !steps pr_v;
+              v
         in
-        let u = aux t in
+        let u, pr_u = loop t in
         if Term.equal t u then None
         else (
           (* proof: [sub_proofs |- t=u] by CC + subproof *)
-          P.with_proof self.proof (P.lemma_preprocess t u);
-          Some u
+          let step =
+            P.lemma_preprocess t u ~using:(Bag.to_iter pr_u) self.proof in
+          Some (u, step)
         )
 
       let normalize_t self t =
         match normalize self t with
-        | Some u -> u
-        | None -> t
+        | Some (u, pr_u) -> u, Some pr_u
+        | None -> t, None
     end
     type simplify_hook = Simplify.hook
 
     module type PREPROCESS_ACTS = sig
-      val mk_lit : ?sign:bool -> term -> lit
-      val add_clause : lit list -> dproof -> unit
+      val proof : proof
+      val mk_lit_nopreproc : ?sign:bool -> term -> lit
+      val mk_lit : ?sign:bool -> term -> lit * proof_step option
+      val add_clause : lit list -> proof_step -> unit
       val add_lit : ?default_pol:bool -> lit -> unit
     end
     type preprocess_actions = (module PREPROCESS_ACTS)
@@ -179,7 +208,7 @@ module Make(A : ARG)
       simp: Simplify.t;
       mutable preprocess: preprocess_hook list;
       mutable mk_model: model_hook list;
-      preprocess_cache: Term.t Term.Tbl.t;
+      preprocess_cache: (Term.t * proof_step Bag.t) Term.Tbl.t;
       mutable t_defs : (term*term) list; (* term definitions *)
       mutable th_states : th_states; (** Set of theories *)
       mutable on_partial_check: (t -> theory_actions -> lit Iter.t -> unit) list;
@@ -190,7 +219,7 @@ module Make(A : ARG)
     and preprocess_hook =
       t ->
       preprocess_actions ->
-      term -> term option
+      term -> (term * proof_step Iter.t) option
 
     and model_hook =
       recurse:(t -> CC.N.t -> term) ->
@@ -203,15 +232,12 @@ module Make(A : ARG)
     let[@inline] cc (t:t) = Lazy.force t.cc
     let[@inline] tst t = t.tst
     let[@inline] ty_st t = t.ty_st
-    let[@inline] with_proof self f = Proof.with_proof self.proof f
+    let[@inline] proof self = self.proof
     let stats t = t.stat
 
-    let define_const (self:t) ~const ~rhs : unit =
-      self.t_defs <- (const,rhs) :: self.t_defs
-
     let simplifier self = self.simp
     let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
-    let simp_t self (t:Term.t) : Term.t = Simplify.normalize_t self.simp t
+    let simp_t self (t:Term.t) : Term.t * _ = Simplify.normalize_t self.simp t
 
     let add_simplifier (self:t) f : unit = Simplify.add_hook self.simp f
 
@@ -236,12 +262,12 @@ module Make(A : ARG)
     let[@inline] propagate_l self acts p cs proof : unit =
       propagate self acts p ~reason:(fun()->cs,proof)
 
-    let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:dproof) : unit =
+    let add_sat_clause_ self (acts:theory_actions) ~keep lits (proof:proof_step) : unit =
       let (module A) = acts in
       Stat.incr self.count_axiom;
       A.add_clause ~keep lits proof
 
-    let add_sat_clause_pool_ self (acts:theory_actions) ~pool lits (proof:dproof) : unit =
+    let add_sat_clause_pool_ self (acts:theory_actions) ~pool lits (proof:proof_step) : unit =
       let (module A) = acts in
       Stat.incr self.count_axiom;
       A.add_clause_in_pool ~pool lits proof
@@ -253,8 +279,8 @@ module Make(A : ARG)
     (* actual preprocessing logic, acting on terms.
        this calls all the preprocessing hooks on subterms, ensuring
        a fixpoint. *)
-    let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term =
-      let mk_lit_nopreproc t = Lit.atom self.tst t in (* no further simplification *)
+    let preprocess_term_ (self:t) (module A0:PREPROCESS_ACTS) (t:term) : term * proof_step option =
+      let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.tst t in (* no further simplification *)
 
       (* compute and cache normal form [u] of [t].
 
@@ -263,19 +289,23 @@ module Make(A : ARG)
          next time we preprocess [t], we will have to re-emit the same
          proofs, even though we will not do any actual preprocessing work.
       *)
-      let rec preproc_rec t : term =
+      let rec preproc_rec ~steps t : term =
         match Term.Tbl.find self.preprocess_cache t with
-        | u -> u
+        | u, pr_u ->
+          steps := Bag.append pr_u !steps;
+          u
+
         | exception Not_found ->
           (* try rewrite at root *)
-          let t1 = preproc_with_hooks t self.preprocess in
+          let steps = ref Bag.empty in
+          let t1 = preproc_with_hooks ~steps t self.preprocess in
 
           (* map subterms *)
-          let t2 = Term.map_shallow self.tst preproc_rec t1 in
+          let t2 = Term.map_shallow self.tst (preproc_rec ~steps) t1 in
 
           let u =
             if not (Term.equal t t2) then (
-              preproc_rec t2 (* fixpoint *)
+              preproc_rec ~steps t2 (* fixpoint *)
             ) else (
               t2
             )
@@ -303,75 +333,109 @@ module Make(A : ARG)
                   Term.pp t Term.pp u);
           );
 
-          Term.Tbl.add self.preprocess_cache t u;
+          let pr_t_u = !steps in
+          Term.Tbl.add self.preprocess_cache t (u, pr_t_u);
           u
 
       (* try each function in [hooks] successively *)
-      and preproc_with_hooks t hooks : term =
+      and preproc_with_hooks ~steps t hooks : term =
+        let[@inline] add_step s = steps := Bag.cons s !steps in
         match hooks with
         | [] -> t
         | h :: hooks_tl ->
           (* call hook, using [pacts] which will ensure all new
              literals and clauses are also preprocessed *)
           match h self (Lazy.force pacts) t with
-          | None -> preproc_with_hooks t hooks_tl
-          | Some u -> preproc_rec u
+          | None -> preproc_with_hooks ~steps t hooks_tl
+          | Some (u, pr_u) ->
+            Iter.iter add_step pr_u;
+            preproc_rec ~steps u
 
       (* create literal and preprocess it with [pacts], which uses [A0]
          for the base operations, and preprocesses new literals and clauses
          recursively. *)
-      and mk_lit ?sign t =
-        let u = preproc_rec t in
-        if not (Term.equal t u) then (
-          Log.debugf 10
-            (fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
-                Term.pp t Term.pp u);
-        );
-        Lit.atom self.tst ?sign u
+      and mk_lit ?sign t : _ * proof_step option =
+        let steps = ref Bag.empty in
+        let u = preproc_rec ~steps t in
+        let pr_t_u =
+          if not (Term.equal t u) then (
+            Log.debugf 10
+              (fun k->k "(@[smt-solver.preprocess.t@ :t %a@ :into %a@])"
+                  Term.pp t Term.pp u);
 
-      and preprocess_lit (lit:lit) : lit =
+            let p =
+              A.P.lemma_preprocess t u ~using:(Bag.to_iter !steps) self.proof
+            in
+            Some p
+          ) else None
+        in
+        Lit.atom self.tst ?sign u, pr_t_u
+
+      and preprocess_lit ~steps (lit:lit) : lit =
         let t = Lit.term lit in
         let sign = Lit.sign lit in
-        mk_lit ~sign t
+        let lit, pr = mk_lit ~sign t in
+        CCOpt.iter (fun s -> steps := s :: !steps) pr;
+        lit
 
       (* wrap [A0] so that all operations go throught preprocessing *)
       and pacts = lazy (
         (module struct
+          let proof = A0.proof
+
           let add_lit ?default_pol lit =
-            let lit = preprocess_lit lit in
+            (* just drop the proof *)
+            (* TODO: add a clause instead [lit => preprocess(lit)]? *)
+            let lit = preprocess_lit ~steps:(ref []) lit in
             A0.add_lit ?default_pol lit
-          let add_clause c pr =
+
+          let add_clause c pr_c =
             Stat.incr self.count_preprocess_clause;
-            let c = CCList.map preprocess_lit c in
-            A0.add_clause c pr
+            let steps = ref [] in
+            let c' = CCList.map (preprocess_lit ~steps) c in
+            let pr_c' =
+              A.P.lemma_rw_clause pr_c
+                ~res:(Iter.of_list c')
+                ~using:(Iter.of_list !steps) proof
+            in
+            A0.add_clause c' pr_c'
+
+          let mk_lit_nopreproc = mk_lit_nopreproc
+
           let mk_lit = mk_lit
         end : PREPROCESS_ACTS)
       ) in
 
-      P.begin_subproof self.proof;
+      let steps = ref Bag.empty in
+      let[@inline] add_step s = steps := Bag.cons s !steps in
 
       (* simplify the term *)
-      let t1 = simp_t self t in
+      let t1, pr_1 = simp_t self t in
+      CCOpt.iter add_step pr_1;
 
       (* preprocess *)
-      let u = preproc_rec t1 in
-      (* emit [|- t=u] *)
-      if not (Term.equal t u) then (
-        P.with_proof self.proof (P.lemma_preprocess t u);
-      );
+      let u = preproc_rec ~steps t1 in
 
-      P.end_subproof self.proof;
-      u
+      (* emit [|- t=u] *)
+      let pr_u =
+        if not (Term.equal t u) then (
+          let p = P.lemma_preprocess t u ~using:(Bag.to_iter !steps) self.proof in
+          Some p
+        ) else None
+      in
+
+      u, pr_u
 
     (* return preprocessed lit *)
-    let preprocess_lit_ (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
+    let preprocess_lit_ ~steps (self:t) (pacts:preprocess_actions) (lit:lit) : lit =
       let t = Lit.term lit in
       let sign = Lit.sign lit in
-      let u = preprocess_term_ self pacts t in
+      let u, pr_u = preprocess_term_ self pacts t in
+      CCOpt.iter (fun s -> steps := s :: !steps) pr_u;
       Lit.atom self.tst ~sign u
 
     (* add a clause using [acts] *)
-    let add_clause_ self acts lits (proof:dproof) : unit =
+    let add_clause_ self acts lits (proof:proof_step) : unit =
       add_sat_clause_ self acts ~keep:true lits proof
 
     let[@inline] add_lit _self (acts:theory_actions) ?default_pol lit : unit =
@@ -380,30 +444,40 @@ module Make(A : ARG)
 
     let preprocess_acts_of_acts (self:t) (acts:theory_actions) : preprocess_actions =
       (module struct
-        let mk_lit ?sign t = Lit.atom self.tst ?sign t
+        let proof = self.proof
+        let mk_lit_nopreproc ?sign t = Lit.atom self.tst ?sign t
+        let mk_lit ?sign t = Lit.atom self.tst ?sign t, None
         let add_clause = add_clause_ self acts
         let add_lit = add_lit self acts
       end)
 
-    let preprocess_clause_ (self:t) (acts:theory_actions) (c:lit list) : lit list =
+    let preprocess_clause_ (self:t) (acts:theory_actions)
+        (c:lit list) (proof:proof_step) : lit list * proof_step =
+      let steps = ref [] in
       let pacts = preprocess_acts_of_acts self acts in
-      let c = CCList.map (preprocess_lit_ self pacts) c in
-      c
+      let c = CCList.map (preprocess_lit_ ~steps self pacts) c in
+      let pr =
+        P.lemma_rw_clause proof
+          ~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof
+      in
+      c, pr
 
     (* make literal and preprocess it *)
     let[@inline] mk_plit (self:t) (pacts:preprocess_actions) ?sign (t:term) : lit =
       let lit = Lit.atom self.tst ?sign t in
-      preprocess_lit_ self pacts lit
+      let steps = ref [] in
+      preprocess_lit_ ~steps self pacts lit
 
-    let[@inline] preprocess_term self (pacts:preprocess_actions) (t:term) : term =
+    let[@inline] preprocess_term self
+        (pacts:preprocess_actions) (t:term) : term * _ option =
       preprocess_term_ self pacts t
 
-    let[@inline] add_clause_temp self acts c (proof:dproof) : unit =
-      let c = preprocess_clause_ self acts c in
+    let[@inline] add_clause_temp self acts c (proof:proof_step) : unit =
+      let c, proof = preprocess_clause_ self acts c proof in
       add_sat_clause_ self acts ~keep:false c proof
 
-    let[@inline] add_clause_permanent self acts c (proof:dproof) : unit =
-      let c = preprocess_clause_ self acts c in
+    let[@inline] add_clause_permanent self acts c (proof:proof_step) : unit =
+      let c, proof = preprocess_clause_ self acts c proof in
       add_sat_clause_ self acts ~keep:true c proof
 
     let[@inline] mk_lit (self:t) (acts:theory_actions) ?sign t : lit =
@@ -516,7 +590,7 @@ module Make(A : ARG)
         ty_st;
         cc = lazy (
           (* lazily tie the knot *)
-          CC.create ~size:`Big self.tst;
+          CC.create ~size:`Big self.tst self.proof;
         );
         proof;
         th_states=Ths_nil;
@@ -608,7 +682,7 @@ module Make(A : ARG)
       let t_true = Term.bool tst true in
       Sat_solver.add_clause self.solver
         [Lit.atom tst t_true]
-        (P.lemma_true t_true)
+        (P.lemma_true t_true self.proof)
     end;
     self
 
@@ -617,11 +691,14 @@ module Make(A : ARG)
   let[@inline] stats self = self.stat
   let[@inline] tst self = Solver_internal.tst self.si
   let[@inline] ty_st self = Solver_internal.ty_st self.si
+  let[@inline] proof self = self.si.proof
 
   let preprocess_acts_of_solver_
       (self:t) : (module Solver_internal.PREPROCESS_ACTS) =
     (module struct
-      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t
+      let proof = self.proof
+      let mk_lit_nopreproc ?sign t = Lit.atom ?sign self.si.tst t
+      let mk_lit ?sign t = Lit.atom ?sign self.si.tst t, None
       let add_lit ?default_pol lit =
         Sat_solver.add_lit self.solver ?default_pol lit
       let add_clause c pr =
@@ -629,9 +706,9 @@ module Make(A : ARG)
     end)
 
   (* preprocess literal *)
-  let preprocess_lit_ (self:t) (lit:lit) : lit =
+  let preprocess_lit_ ~steps (self:t) (lit:lit) : lit =
     let pacts = preprocess_acts_of_solver_ self in
-    Solver_internal.preprocess_lit_ self.si pacts lit
+    Solver_internal.preprocess_lit_ ~steps self.si pacts lit
 
   (* make a literal from a term, ensuring it is properly preprocessed *)
   let mk_lit_t (self:t) ?sign (t:term) : lit =
@@ -678,6 +755,10 @@ module Make(A : ARG)
     | Sat of Model.t
     | Unsat of {
         unsat_core: unit -> lit Iter.t;
+        (** Unsat core (subset of assumptions), or empty *)
+
+        unsat_proof_step: unit -> proof_step option;
+        (** Proof step for the empty clause *)
       }
     | Unknown of Unknown.t
     (** Result of solving for the current set of clauses *)
@@ -687,7 +768,7 @@ module Make(A : ARG)
   let pp_stats out (self:t) : unit =
     Stat.pp_all out (Stat.all @@ stats self)
 
-  let add_clause (self:t) (c:lit IArray.t) (proof:dproof) : unit =
+  let add_clause (self:t) (c:lit IArray.t) (proof:proof_step) : unit =
     Stat.incr self.count_clause;
     Log.debugf 50 (fun k->
         k "(@[solver.add-clause@ %a@])"
@@ -699,12 +780,15 @@ module Make(A : ARG)
   let add_clause_l self c p = add_clause self (IArray.of_list c) p
 
   let assert_terms self c =
+    let steps = ref [] in
     let c = CCList.map (fun t -> Lit.atom (tst self) t) c in
-    let c = CCList.map (preprocess_lit_ self) c in
+    let c = CCList.map (preprocess_lit_ ~steps self) c in
     (* TODO: if c != c0 then P.emit_redundant_clause c
        because we jsut preprocessed it away? *)
-    let dp = P.emit_input_clause (Iter.of_list c) in
-    add_clause_l self c dp
+    let pr = P.emit_input_clause (Iter.of_list c) self.proof in
+    let pr = P.lemma_rw_clause pr
+        ~res:(Iter.of_list c) ~using:(Iter.of_list !steps) self.proof in
+    add_clause_l self c pr
 
   let assert_term self t = assert_terms self [t]
 
@@ -782,8 +866,9 @@ module Make(A : ARG)
 
     | Sat_solver.Unsat (module UNSAT) ->
       let unsat_core () = UNSAT.unsat_assumptions () in
+      let unsat_proof_step () = Some (UNSAT.unsat_proof()) in
       do_on_exit ();
-      Unsat {unsat_core}
+      Unsat {unsat_core; unsat_proof_step}
 
   let mk_theory (type st)
       ~name ~create_and_setup

src/smtlib/Process.ml

@@ -129,10 +129,20 @@ let mk_progress (_s:Solver.t) : _ -> unit =
       flush stdout
     )
 
+let with_file_out (file:string) (f:out_channel -> 'a): 'a =
+  if Filename.extension file = ".gz" then (
+    let p =
+      Unix.open_process_out
+        (Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file))
+    in
+    CCFun.finally1 ~h:(fun () -> Unix.close_process_out p) f p
+  ) else CCIO.with_out file f
+
 (* call the solver to check-sat *)
 let solve
     ?gc:_
     ?restarts:_
+    ?proof_file
     ?(pp_model=false)
     ?(check=false)
     ?time:_ ?memory:_ ?(progress=false)
@@ -163,7 +173,7 @@ let solve
          *)
       let t3 = Sys.time () -. t2 in
       Format.printf "Sat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
-    | Solver.Unsat _ ->
+    | Solver.Unsat { unsat_proof_step; unsat_core=_ } ->
 
       if check then (
         ()
@@ -175,16 +185,23 @@ let solve
            *)
       );
 
-      (* FIXME: instead, create a proof if proof file or --check is given
-      begin match proof_file, proof with
-        | Some file, lazy (Some p) ->
-          Profile.with_ "proof.write-file" @@ fun () ->
-          let p = Profile.with1 "proof.mk-proof" Solver.Pre_proof.to_proof p in
-          CCIO.with_out file
-            (fun oc -> Proof.Quip.output oc p; flush oc)
+      begin match proof_file with
+        | Some file ->
+          begin match unsat_proof_step() with
+            | None -> ()
+            | Some unsat_step ->
+              let proof = Solver.proof s in
+              let proof_quip =
+                Profile.with_ "proof.to-quip" @@ fun () ->
+                Proof_quip.of_proof proof ~unsat:unsat_step
+              in
+              Profile.with_ "proof.write-file" @@ fun () ->
+              with_file_out file @@ fun oc ->
+              Proof_quip.output oc proof_quip;
+              flush oc
+          end
         | _ -> ()
       end;
-         *)
 
       let t3 = Sys.time () -. t2 in
       Format.printf "Unsat (%.3f/%.3f/%.3f)@." t1 (t2-.t1) t3;
@@ -196,7 +213,7 @@ let solve
 (* process a single statement *)
 let process_stmt
     ?gc ?restarts ?(pp_cnf=false)
-    ?pp_model ?(check=false)
+    ?proof_file ?pp_model ?(check=false)
     ?time ?memory ?progress
     (solver:Solver.t)
     (stmt:Statement.t) : unit or_error =
@@ -234,7 +251,7 @@ let process_stmt
           l
       in
       solve
-        ?gc ?restarts ~check ?pp_model
+        ?gc ?restarts ~check ?pp_model ?proof_file
         ?time ?memory ?progress
         ~assumptions
         solver;
@@ -252,7 +269,7 @@ let process_stmt
       );
       let lit = Solver.mk_lit_t solver t in
       Solver.add_clause solver (IArray.singleton lit)
-        (Solver.P.emit_input_clause (Iter.singleton lit));
+        (Solver.P.emit_input_clause (Iter.singleton lit) (Solver.proof solver));
       E.return()
 
     | Statement.Stmt_assert_clause c_ts ->
@@ -263,14 +280,14 @@ let process_stmt
       let c = CCList.map (fun t -> Solver.mk_lit_t solver t) c_ts in
 
       (* proof of assert-input + preprocessing *)
-      let emit_proof p =
+      let pr =
         let module P = Solver.P in
+        let proof = Solver.proof solver in
         let tst = Solver.tst solver in
-        P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) p;
-        P.emit_redundant_clause (Iter.of_list c) p;
+        P.emit_input_clause (Iter.of_list c_ts |> Iter.map (Lit.atom tst)) proof
       in
 
-      Solver.add_clause solver (IArray.of_list c) emit_proof;
+      Solver.add_clause solver (IArray.of_list c) pr;
       E.return()
 
     | Statement.Stmt_data _ ->

src/smtlib/Process.mli

@@ -7,7 +7,7 @@ module Solver
                             and type T.Term.store = Term.store
                             and type T.Ty.t = Ty.t
                             and type T.Ty.store = Ty.store
-                            and type proof = Proof_stub.t
+                            and type proof = Proof.t
 
 val th_bool : Solver.theory
 val th_data : Solver.theory
@@ -24,6 +24,7 @@ val process_stmt :
   ?gc:bool ->
   ?restarts:bool ->
   ?pp_cnf:bool ->
+  ?proof_file:string ->
   ?pp_model:bool ->
   ?check:bool ->
   ?time:float ->

src/smtlib/Sidekick_smtlib.ml

@@ -6,7 +6,7 @@ module Process = Process
 module Solver = Process.Solver
 module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
-module Proof = Sidekick_base.Proof_stub
+module Proof = Sidekick_base.Proof
 
 type 'a or_error = ('a, string) CCResult.t
 

src/smtlib/Sidekick_smtlib.mli

@@ -10,7 +10,7 @@ module Term = Sidekick_base.Term
 module Stmt = Sidekick_base.Statement
 module Process = Process
 module Solver = Process.Solver
-module Proof = Sidekick_base.Proof_stub (* FIXME: actual DRUP(T) proof *)
+module Proof = Sidekick_base.Proof
 
 val parse : Term.store -> string -> Stmt.t list or_error
 

src/tests/basic.drup.expected

@@ -9,5 +9,6 @@ i 1 -2 -4 0
 r -4 -1 0
 r -1 0
 r -3 0
-r -2 -4 1 0
+r 4 0
+r -2 0
 r 0

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -18,6 +18,29 @@ type ('a, 'args) bool_view =
   | B_opaque_bool of 'a (* do not enter *)
   | B_atom of 'a
 
+module type PROOF = sig
+  type proof
+  type proof_step
+  type term
+  type lit
+
+  val lemma_bool_tauto : lit Iter.t -> proof -> proof_step
+  (** Boolean tautology lemma (clause) *)
+
+  val lemma_bool_c : string -> term list -> proof -> proof_step
+  (** Basic boolean logic lemma for a clause [|- c].
+      [proof_bool_c b name cs] is the rule designated by [name]. *)
+
+  val lemma_bool_equiv : term -> term -> proof -> proof_step
+  (** Boolean tautology lemma (equivalence) *)
+
+  val lemma_ite_true : ite:term -> proof -> proof_step
+  (** lemma [a ==> ite a b c = b] *)
+
+  val lemma_ite_false : ite:term -> proof -> proof_step
+  (** lemma [¬a ==> ite a b c = c] *)
+end
+
 (** Argument to the theory *)
 module type ARG = sig
   module S : Sidekick_core.SOLVER
@@ -36,21 +59,11 @@ module type ARG = sig
       Only enable if some theories are susceptible to
       create boolean formulas during the proof search. *)
 
-  val lemma_bool_tauto : S.Lit.t Iter.t -> S.P.t -> unit
-  (** Boolean tautology lemma (clause) *)
-
-  val lemma_bool_c : string -> term list -> S.P.t -> unit
-  (** Basic boolean logic lemma for a clause [|- c].
-      [proof_bool_c b name cs] is the rule designated by [name]. *)
-
-  val lemma_bool_equiv : term -> term -> S.P.t -> unit
-  (** Boolean tautology lemma (equivalence) *)
-
-  val lemma_ite_true : a:term -> ite:term -> S.P.t -> unit
-  (** lemma [a => ite a b c = b] *)
-
-  val lemma_ite_false : a:term -> ite:term -> S.P.t -> unit
-  (** lemma [¬a => ite a b c = c] *)
+  include PROOF
+    with type proof := S.P.t
+     and type proof_step := S.P.proof_step
+     and type lit := S.Lit.t
+     and type term := S.T.Term.t
 
   (** Fresh symbol generator.
 
@@ -116,21 +129,32 @@ module Make(A : ARG) : S with module A = A = struct
   let is_true t = match T.as_bool t with Some true -> true | _ -> false
   let is_false t = match T.as_bool t with Some false -> true | _ -> false
 
-  let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : T.t option =
+  let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
     let tst = self.tst in
-    let ret u =
-      if not (T.equal t u) then (
-        SI.Simplify.with_proof simp (fun p ->
-          A.lemma_bool_equiv t u p;
-          A.S.P.lemma_preprocess t u p;
-        );
-      );
-      Some u
+
+    let proof = SI.Simplify.proof simp in
+    let steps = ref [] in
+    let add_step_ s = steps := s :: !steps in
+
+    let add_step_eq a b ~using ~c0 :unit =
+      add_step_ @@ SI.P.lemma_rw_clause c0 (SI.Simplify.proof simp)
+        ~using
+        ~res:(Iter.return (Lit.atom tst (A.mk_bool tst (B_eq (a,b)))))
     in
+
+    let[@inline] ret u =
+      Some (u, Iter.of_list !steps)
+    in
+    (* proof is [t <=> u] *)
+    let ret_bequiv t1 u =
+      add_step_ @@ A.lemma_bool_equiv t1 u @@ SI.Simplify.proof simp;
+      ret u
+    in
+
     match A.view_as_bool t with
     | B_bool _ -> None
-    | B_not u when is_true u -> ret (T.bool tst false)
-    | B_not u when is_false u -> ret (T.bool tst true)
+    | B_not u when is_true u -> ret_bequiv t (T.bool tst false)
+    | B_not u when is_false u -> ret_bequiv t (T.bool tst true)
     | B_not _ -> None
     | B_opaque_bool _ -> None
     | B_and a ->
@@ -148,28 +172,33 @@ module Make(A : ARG) : S with module A = A = struct
     | B_ite (a,b,c) ->
       (* directly simplify [a] so that maybe we never will simplify one
          of the branches *)
-      let a = SI.Simplify.normalize_t simp a in
+      let a, prf_a = SI.Simplify.normalize_t simp a in
+      CCOpt.iter add_step_ prf_a;
       begin match A.view_as_bool a with
         | B_bool true ->
-          SI.Simplify.with_proof simp (A.lemma_ite_true ~a ~ite:t);
-          Some b
+          add_step_eq t b ~using:(Iter.of_opt prf_a)
+            ~c0:(A.lemma_ite_true ~ite:t proof);
+          ret b
+
         | B_bool false ->
-          SI.Simplify.with_proof simp (A.lemma_ite_false ~a ~ite:t);
-          Some c
+          add_step_eq t c ~using:(Iter.of_opt prf_a)
+            ~c0:(A.lemma_ite_false ~ite:t proof);
+          ret c
+
         | _ ->
           None
       end
-    | B_equiv (a,b) when is_true a -> ret b
-    | B_equiv (a,b) when is_false a -> ret (not_ tst b)
-    | B_equiv (a,b) when is_true b -> ret a
-    | B_equiv (a,b) when is_false b -> ret (not_ tst a)
-    | B_xor (a,b) when is_false a -> ret b
-    | B_xor (a,b) when is_true a -> ret (not_ tst b)
-    | B_xor (a,b) when is_false b -> ret a
-    | B_xor (a,b) when is_true b -> ret (not_ tst a)
+    | B_equiv (a,b) when is_true a -> ret_bequiv t b
+    | B_equiv (a,b) when is_false a -> ret_bequiv t (not_ tst b)
+    | B_equiv (a,b) when is_true b -> ret_bequiv t a
+    | B_equiv (a,b) when is_false b -> ret_bequiv t (not_ tst a)
+    | B_xor (a,b) when is_false a -> ret_bequiv t b
+    | B_xor (a,b) when is_true a -> ret_bequiv t (not_ tst b)
+    | B_xor (a,b) when is_false b -> ret_bequiv t a
+    | B_xor (a,b) when is_true b -> ret_bequiv t (not_ tst a)
     | B_equiv _ | B_xor _ -> None
-    | B_eq (a,b) when T.equal a b -> ret (T.bool tst true)
-    | B_neq (a,b) when T.equal a b -> ret (T.bool tst true)
+    | B_eq (a,b) when T.equal a b -> ret_bequiv t (T.bool tst true)
+    | B_neq (a,b) when T.equal a b -> ret_bequiv t (T.bool tst true)
     | B_eq _ | B_neq _ -> None
     | B_atom _ -> None
 
@@ -185,67 +214,91 @@ module Make(A : ARG) : S with module A = A = struct
     let proxy = fresh_term ~for_t ~pre self (Ty.bool self.ty_st) in
     proxy, mk_lit proxy
 
+  let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p
+  let pr_p1_opt p s1 s2 : SI.proof_step =
+    CCOpt.map_or ~default:s2 (fun s1 -> SI.P.proof_p1 s1 s2 p) s1
+
   (* preprocess "ite" away *)
-  let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
+  let preproc_ite self si (module PA:SI.PREPROCESS_ACTS)
+      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
+    let steps = ref [] in
+    let add_step_ s = steps := s :: !steps in
+
+    let ret t = Some (t, Iter.of_list !steps) in
+
+    let add_clause_rw lits ~using ~c0 : unit =
+      PA.add_clause lits @@
+      SI.P.lemma_rw_clause c0 ~res:(Iter.of_list lits) ~using PA.proof
+    in
+
     match A.view_as_bool t with
     | B_ite (a,b,c) ->
-      let a = SI.simp_t si a in
-      begin match A.view_as_bool a with
+      let a', pr_a = SI.simp_t si a in
+      CCOpt.iter add_step_ pr_a;
+      begin match A.view_as_bool a' with
         | B_bool true ->
-          (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
-          SI.with_proof si (A.lemma_ite_true ~a ~ite:t);
-          Some b
+          (* [a |- ite a b c=b],  [a=true] implies [ite a b c=b] *)
+          add_step_
+            (pr_p1_opt PA.proof pr_a @@ A.lemma_ite_true ~ite:t PA.proof);
+          ret b
+
         | B_bool false ->
-          (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
-          SI.with_proof si (A.lemma_ite_false ~a ~ite:t);
-          Some c
+          (* [¬a |- ite a b c=c],  [a=false] implies [ite a b c=c] *)
+          add_step_
+            (pr_p1_opt PA.proof pr_a @@ A.lemma_ite_false ~ite:t PA.proof);
+          ret c
+
         | _ ->
           let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
-          SI.define_const si ~const:t_ite ~rhs:t;
-          SI.with_proof si (SI.P.define_term t_ite t);
-          let lit_a = PA.mk_lit a in
-          PA.add_clause [Lit.neg lit_a; PA.mk_lit (eq self.tst t_ite b)]
-            (fun p -> A.lemma_ite_true ~a ~ite:t p);
-          PA.add_clause [lit_a; PA.mk_lit (eq self.tst t_ite c)]
-            (fun p -> A.lemma_ite_false p ~a ~ite:t);
-          Some t_ite
+          let pr_def = SI.P.define_term t_ite t PA.proof in
+          let lit_a = PA.mk_lit_nopreproc a' in
+          add_clause_rw [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)]
+            ~using:Iter.(append (return pr_def) (of_opt pr_a))
+            ~c0:(A.lemma_ite_true ~ite:t PA.proof);
+          add_clause_rw [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)]
+            ~using:Iter.(append (return pr_def) (of_opt pr_a))
+            ~c0:(A.lemma_ite_false ~ite:t PA.proof);
+          ret t_ite
       end
     | _ -> None
 
   (* TODO: polarity? *)
-  let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS) (t:T.t) : T.t option =
+  let cnf (self:state) (si:SI.t) (module PA:SI.PREPROCESS_ACTS)
+      (t:T.t) : (T.t * _ Iter.t) option =
     Log.debugf 50 (fun k->k"(@[th-bool.cnf@ %a@])" T.pp t);
-
-    let mk_lit = PA.mk_lit in
+    let steps = ref [] in
+    let[@inline] add_step s = steps := s :: !steps in
 
     (* handle boolean equality *)
-    let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
-      let a = mk_lit t_a in
-      let b = mk_lit t_b in
+    let equiv_ _si ~is_xor ~for_t t_a t_b : Lit.t =
+      let a = PA.mk_lit_nopreproc t_a in
+      let b = PA.mk_lit_nopreproc t_b in
       let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
-      let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit ~pre:"equiv_" self in
+      let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in
 
-      SI.define_const si ~const:t_proxy ~rhs:for_t;
-      SI.with_proof si (SI.P.define_term t_proxy for_t);
+      let pr_def = SI.P.define_term t_proxy for_t PA.proof in
+      add_step pr_def;
 
-      let add_clause c pr =
-        PA.add_clause c pr
-      in
+      let[@inline] add_clause c pr = PA.add_clause c pr in
 
       (* proxy => a<=> b,
          ¬proxy => a xor b *)
       add_clause [Lit.neg proxy; Lit.neg a; b]
-        (if is_xor then A.lemma_bool_c "xor-e+" [t_proxy]
-         else A.lemma_bool_c "eq-e" [t_proxy; t_a]);
+        (pr_p1 PA.proof pr_def @@
+         if is_xor then A.lemma_bool_c "xor-e+" [for_t] PA.proof
+         else A.lemma_bool_c "eq-e" [for_t; t_a] PA.proof);
       add_clause [Lit.neg proxy; Lit.neg b; a]
-        (if is_xor then A.lemma_bool_c "xor-e-" [t_proxy]
-         else A.lemma_bool_c "eq-e" [t_proxy; t_b]);
+        (pr_p1 PA.proof pr_def @@
+         if is_xor then A.lemma_bool_c "xor-e-" [for_t] PA.proof
+         else A.lemma_bool_c "eq-e" [for_t; t_b] PA.proof);
       add_clause [proxy; a; b]
-        (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_a]
-         else A.lemma_bool_c "eq-i+" [t_proxy]);
+        (pr_p1 PA.proof pr_def @@
+         if is_xor then A.lemma_bool_c "xor-i" [for_t; t_a] PA.proof
+         else A.lemma_bool_c "eq-i+" [for_t] PA.proof);
       add_clause [proxy; Lit.neg a; Lit.neg b]
-        (if is_xor then A.lemma_bool_c "xor-i" [t_proxy; t_b]
-         else A.lemma_bool_c "eq-i-" [t_proxy]);
+        (pr_p1 PA.proof pr_def @@
+         if is_xor then A.lemma_bool_c "xor-i" [for_t; t_b] PA.proof
+         else A.lemma_bool_c "eq-i-" [for_t] PA.proof);
       proxy
     in
 
@@ -260,57 +313,63 @@ module Make(A : ARG) : S with module A = A = struct
 
       | B_and l ->
         let t_subs = Iter.to_list l in
-        let subs = List.map mk_lit t_subs in
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"and_" self in
-        SI.define_const si ~const:t_proxy ~rhs:t;
-        SI.with_proof si (SI.P.define_term t_proxy t);
+        let subs = List.map PA.mk_lit_nopreproc t_subs in
+        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in
+        let pr_def = SI.P.define_term t_proxy t PA.proof in
+        add_step pr_def;
+
         (* add clauses *)
         List.iter2
           (fun t_u u ->
              PA.add_clause
                [Lit.neg proxy; u]
-               (A.lemma_bool_c "and-e" [t_proxy; t_u]))
+               (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-e" [t; t_u] PA.proof))
           t_subs subs;
         PA.add_clause (proxy :: List.map Lit.neg subs)
-          (A.lemma_bool_c "and-i" [t_proxy]);
+          (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "and-i" [t] PA.proof);
         Some proxy
 
       | B_or l ->
         let t_subs = Iter.to_list l in
-        let subs = List.map mk_lit t_subs in
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"or_" self in
-        SI.define_const si ~const:t_proxy ~rhs:t;
-        SI.with_proof si (SI.P.define_term t_proxy t);
+        let subs = List.map PA.mk_lit_nopreproc t_subs in
+        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in
+        let pr_def = SI.P.define_term t_proxy t PA.proof in
+        add_step pr_def;
+
         (* add clauses *)
         List.iter2
           (fun t_u u ->
              PA.add_clause [Lit.neg u; proxy]
-               (A.lemma_bool_c "or-i" [t_proxy; t_u]))
+               (pr_p1 PA.proof pr_def @@
+                A.lemma_bool_c "or-i" [t; t_u] PA.proof))
           t_subs subs;
         PA.add_clause (Lit.neg proxy :: subs)
-          (A.lemma_bool_c "or-e" [t_proxy]);
+          (pr_p1 PA.proof pr_def @@ A.lemma_bool_c "or-e" [t] PA.proof);
         Some proxy
 
       | B_imply (t_args, t_u) ->
         (* transform into [¬args \/ u] on the fly *)
         let t_args = Iter.to_list t_args in
-        let args = List.map (fun t -> Lit.neg (mk_lit t)) t_args in
-        let u = mk_lit t_u in
+        let args = List.map (fun t -> Lit.neg (PA.mk_lit_nopreproc t)) t_args in
+        let u = PA.mk_lit_nopreproc t_u in
         let subs = u :: args in
 
         (* now the or-encoding *)
-        let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit ~pre:"implies_" self in
-        SI.define_const si ~const:t_proxy ~rhs:t;
-        SI.with_proof si (SI.P.define_term t_proxy t);
+        let t_proxy, proxy =
+          fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in
+        let pr_def = SI.P.define_term t_proxy t PA.proof in
+        add_step pr_def;
 
         (* add clauses *)
         List.iter2
           (fun t_u u ->
              PA.add_clause [Lit.neg u; proxy]
-               (A.lemma_bool_c "imp-i" [t_proxy; t_u]))
+               (pr_p1 PA.proof pr_def @@
+                A.lemma_bool_c "imp-i" [t_proxy; t_u] PA.proof))
           (t_u::t_args) subs;
         PA.add_clause (Lit.neg proxy :: subs)
-          (A.lemma_bool_c "imp-e" [t_proxy]);
+          (pr_p1 PA.proof pr_def @@
+           A.lemma_bool_c "imp-e" [t_proxy] PA.proof);
         Some proxy
 
       | B_ite _ | B_eq _ | B_neq _ -> None
@@ -325,7 +384,7 @@ module Make(A : ARG) : S with module A = A = struct
         let u = Lit.term lit in
         (* put sign back as a "not" *)
         let u = if Lit.sign lit then u else A.mk_bool self.tst (B_not u) in
-        if T.equal u t then None else Some u
+        if T.equal u t then None else Some (u, Iter.of_list !steps)
     end
 
   (* check if new terms were added to the congruence closure, that can be turned
@@ -346,11 +405,15 @@ module Make(A : ARG) : S with module A = A = struct
       all_terms
         (fun t -> match cnf_of t with
            | None -> ()
-           | Some u ->
+           | Some (u, pr_t_u) ->
              Log.debugf 5
                (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
                    T.pp t T.pp u);
-             SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
+
+             (* produce a single step proof of [|- t=u] *)
+             let proof = SI.proof si in
+             let pr = SI.P.lemma_preprocess t u ~using:pr_t_u proof in
+             SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_theory pr []);
              ());
     end;
     ()

src/th-data/Sidekick_th_data.ml

@@ -1,22 +1,7 @@
 
 (** Theory for datatypes. *)
 
-type ('c,'t) data_view =
-  | T_cstor of 'c * 't IArray.t
-  | T_select of 'c * int * 't
-  | T_is_a of 'c * 't
-  | T_other of 't
-
-(** View of types in a way that is directly useful for the theory of datatypes *)
-type ('c, 'ty) data_ty_view =
-  | Ty_arrow of 'ty Iter.t * 'ty
-  | Ty_app of {
-      args: 'ty Iter.t;
-    }
-  | Ty_data of {
-      cstors: 'c;
-    }
-  | Ty_other
+include Th_intf
 
 let name = "th-data"
 
@@ -52,30 +37,6 @@ module C = struct
   let pp out self = Fmt.string out (to_string self)
 end
 
-module type ARG = sig
-  module S : Sidekick_core.SOLVER
-
-  module Cstor : sig
-    type t
-    val ty_args : t -> S.T.Ty.t Iter.t
-    val pp : t Fmt.printer
-    val equal : t -> t -> bool
-  end
-
-  val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view
-  val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
-  val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
-  val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t
-  val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
-  val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t
-  val ty_is_finite : S.T.Ty.t -> bool
-  val ty_set_is_finite : S.T.Ty.t -> bool -> unit
-
-  val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
-  val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
-  val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
-end
-
 (** Helper to compute the cardinality of types *)
 module Compute_card(A : ARG) : sig
   type t
@@ -231,26 +192,36 @@ module Make(A : ARG) : S with module A = A = struct
       Log.debugf 5
         (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])"
             name N.pp n1 pp c1 N.pp n2 pp c2);
-      (* build full explanation of why the constructor terms are equal *)
-      (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *)
-      let expl =
-        Expl.mk_theory @@ Expl.mk_list [
+
+      let mk_expl pr =
+        Expl.mk_theory pr @@ [
           e_n1_n2;
           Expl.mk_merge n1 c1.c_n;
           Expl.mk_merge n2 c2.c_n;
         ]
       in
+
       if A.Cstor.equal c1.c_cstor c2.c_cstor then (
         (* same function: injectivity *)
-        (* FIXME proof *)
+
+        let expl_merge i =
+          mk_expl @@
+          A.lemma_cstor_inj (N.term c1.c_n) (N.term c2.c_n) i (SI.CC.proof cc)
+        in
+
         assert (IArray.length c1.c_args = IArray.length c2.c_args);
-        IArray.iter2
-          (fun u1 u2 -> SI.CC.merge cc u1 u2 expl)
+        IArray.iteri2
+          (fun i u1 u2 -> SI.CC.merge cc u1 u2 (expl_merge i))
           c1.c_args c2.c_args;
         Ok c1
       ) else (
         (* different function: disjointness *)
-        (* FIXME proof *)
+
+        let expl =
+          mk_expl @@
+          A.lemma_cstor_distinct (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc)
+        in
+
         Error expl
       )
   end
@@ -323,6 +294,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   type t = {
     tst: T.store;
+    proof: SI.P.t;
     cstors: ST_cstors.t; (* repr -> cstor for the class *)
     parents: ST_parents.t; (* repr -> parents for the class *)
     cards: Card.t; (* remember finiteness *)
@@ -379,8 +351,9 @@ module Make(A : ARG) : S with module A = A = struct
           Log.debugf 5
             (fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])"
                 name T.pp t is_true N.pp n Monoid_cstor.pp cstor);
+          let pr = A.lemma_isa_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) in
           SI.CC.merge cc n (SI.CC.n_bool cc is_true)
-            Expl.(mk_theory @@ mk_merge n_u cstor.c_n)
+            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
       end
     | T_select (c_t, i, u) ->
       let n_u = SI.CC.add_term cc u in
@@ -392,7 +365,9 @@ module Make(A : ARG) : S with module A = A = struct
                 name N.pp n i A.Cstor.pp c_t);
           assert (i < IArray.length cstor.c_args);
           let u_i = IArray.get cstor.c_args i in
-          SI.CC.merge cc n u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n)
+          let pr = A.lemma_select_cstor ~cstor_t:(N.term cstor.c_n) t (SI.CC.proof cc) in
+          SI.CC.merge cc n u_i
+            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
         | Some _ -> ()
         | None ->
           N_tbl.add self.to_decide repr_u (); (* needs to be decided *)
@@ -410,9 +385,12 @@ module Make(A : ARG) : S with module A = A = struct
       Log.debugf 50
         (fun k->k "(@[%s.on-merge.is-a.reduce@ %a@ :to %B@ :n1 %a@ :n2 %a@ :sub-cstor %a@])"
             name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1);
+      let pr =
+        A.lemma_isa_cstor ~cstor_t:(N.term c1.c_n) (N.term is_a2.is_a_n) self.proof in
       SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true)
-        Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2;
-                       mk_merge n2 is_a2.is_a_arg] |> mk_theory)
+        Expl.(mk_theory pr
+                [mk_merge n1 c1.c_n; mk_merge n1 n2;
+                 mk_merge n2 is_a2.is_a_arg])
     in
     let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) =
       if A.Cstor.equal c1.c_cstor sel2.sel_cstor then (
@@ -420,10 +398,13 @@ module Make(A : ARG) : S with module A = A = struct
           (fun k->k "(@[%s.on-merge.select.reduce@ :n2 %a@ :sel get[%d]-%a@])"
               name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
         assert (sel2.sel_idx < IArray.length c1.c_args);
+        let pr =
+          A.lemma_select_cstor ~cstor_t:(N.term c1.c_n) (N.term sel2.sel_n) self.proof in
         let u_i = IArray.get c1.c_args sel2.sel_idx in
         SI.CC.merge cc sel2.sel_n u_i
-          Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2;
-                         mk_merge n2 sel2.sel_arg] |> mk_theory);
+          Expl.(mk_theory pr
+                  [mk_merge n1 c1.c_n; mk_merge n1 n2;
+                   mk_merge n2 sel2.sel_arg]);
       )
     in
     let merge_c_p n1 n2 =
@@ -507,6 +488,11 @@ module Make(A : ARG) : S with module A = A = struct
         | {flag=Open; cstor_n; _} as node ->
           (* conflict: the [path] forms a cycle *)
           let path = (n, node) :: path in
+          let pr =
+            A.lemma_acyclicity
+              (Iter.of_list path |> Iter.map (fun (a,b) -> N.term a, N.term b.repr))
+              self.proof
+          in
           let expl =
             path
             |> CCList.flat_map
@@ -514,7 +500,7 @@ module Make(A : ARG) : S with module A = A = struct
                  [ Expl.mk_merge node.cstor_n node.repr;
                    Expl.mk_merge n node.repr;
                  ])
-            |> Expl.mk_list |> Expl.mk_theory
+            |> Expl.mk_theory pr
           in
           Stat.incr self.stat_acycl_conflict;
           Log.debugf 5
@@ -548,12 +534,13 @@ module Make(A : ARG) : S with module A = A = struct
         Log.debugf 50
           (fun k->k"(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])"
               name T.pp u  T.pp rhs SI.Lit.pp lit);
-        SI.cc_merge_t solver acts u rhs (Expl.mk_theory @@ Expl.mk_lit lit)
+        let pr = A.lemma_isa_sel t self.proof in
+        SI.cc_merge_t solver acts u rhs (Expl.mk_theory pr [Expl.mk_lit lit])
       | _ -> ()
     in
     Iter.iter check_lit trail
 
-  (* add clauses [∨_c is-c(n)] and [¬(is-a n) ∨ ¬(is-b n)] *)
+  (* add clauses [\Or_c is-c(n)] and [¬(is-a n) ∨ ¬(is-b n)] *)
   let decide_class_ (self:t) (solver:SI.t) acts (n:N.t) : unit =
     let t = N.term n in
     (* [t] might have been expanded already, in case of duplicates in [l] *)
@@ -570,13 +557,13 @@ module Make(A : ARG) : S with module A = A = struct
         |> Iter.to_rev_list
       in
       SI.add_clause_permanent solver acts c
-        (A.lemma_isa_split (Iter.of_list c));
+        (A.lemma_isa_split t (Iter.of_list c) self.proof);
       Iter.diagonal_l c
-        (fun (c1,c2) ->
+        (fun (l1,l2) ->
            let pr =
-             A.lemma_isa_disj (Iter.of_list [SI.Lit.neg c1; SI.Lit.neg c2]) in
+             A.lemma_isa_disj (SI.Lit.neg l1) (SI.Lit.neg l2) self.proof in
            SI.add_clause_permanent solver acts
-             [SI.Lit.neg c1; SI.Lit.neg c2] pr);
+             [SI.Lit.neg l1; SI.Lit.neg l2] pr);
     )
 
   (* on final check, check acyclicity,
@@ -665,6 +652,7 @@ module Make(A : ARG) : S with module A = A = struct
   let create_and_setup (solver:SI.t) : t =
     let self = {
       tst=SI.tst solver;
+      proof=SI.proof solver;
       cstors=ST_cstors.create_and_setup ~size:32 solver;
       parents=ST_parents.create_and_setup ~size:32 solver;
       to_decide=N_tbl.create ~size:16 ();

src/th-data/Sidekick_th_data.mli

@@ -1,83 +1,6 @@
 (** Theory for datatypes. *)
 
-(** Datatype-oriented view of terms.
-
-    - ['c] is the representation of constructors
-    - ['t] is the representation of terms
-*)
-type ('c,'t) data_view =
-  | T_cstor of 'c * 't IArray.t (** [T_cstor (c,args)] is the term [c(args)] *)
-  | T_select of 'c * int * 't
-  (** [T_select (c,i,u)] means the [i]-th argument of [u], which should
-      start with constructor [c] *)
-  | T_is_a of 'c * 't (** [T_is_a (c,u)] means [u] starts with constructor [c] *)
-  | T_other of 't (** non-datatype term *)
-
-(* TODO: use ['ts] rather than IArray? *)
-
-(** View of types in a way that is directly useful for the theory of datatypes *)
-type ('c, 'ty) data_ty_view =
-  | Ty_arrow of 'ty Iter.t * 'ty
-  | Ty_app of {
-      args: 'ty Iter.t;
-    }
-  | Ty_data of {
-      cstors: 'c;
-    }
-  | Ty_other
-
-(** Argument to the functor *)
-module type ARG = sig
-  module S : Sidekick_core.SOLVER
-
-  (** Constructor symbols.
-
-      A constructor is an injective symbol, part of a datatype (or "sum type").
-      For example, in [type option a = Some a | None],
-      the constructors are [Some] and [None]. *)
-  module Cstor : sig
-    type t
-    (** Constructor *)
-
-    val ty_args : t -> S.T.Ty.t Iter.t
-    (** Type arguments, for a polymorphic constructor *)
-
-    val pp : t Fmt.printer
-    val equal : t -> t -> bool
-    (** Comparison *)
-  end
-
-  val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view
-  (** Try to view type as a datatype (with its constructors) *)
-
-  val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
-  (** Try to view term as a datatype term *)
-
-  val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
-  (** Make a constructor application term *)
-
-  val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t
-  (** Make a [is-a] term *)
-
-  val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
-  (** Make a selector term *)
-
-  val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t
-  (** Make a term equality *)
-
-  val ty_is_finite : S.T.Ty.t -> bool
-  (** Is the given type known to be finite? For example a finite datatype
-      (an "enum" in C parlance), or [Bool], or [Array Bool Bool]. *)
-
-  val ty_set_is_finite : S.T.Ty.t -> bool -> unit
-  (** Modify the "finite" field (see {!ty_is_finite}) *)
-
-  (* TODO: should we store this ourself? would be simpler… *)
-
-  val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
-  val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
-  val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
-end
+include module type of Th_intf
 
 module type S = sig
   module A : ARG

src/th-data/th_intf.ml

@@ -0,0 +1,113 @@
+
+(** Datatype-oriented view of terms.
+
+    - ['c] is the representation of constructors
+    - ['t] is the representation of terms
+*)
+type ('c,'t) data_view =
+  | T_cstor of 'c * 't IArray.t
+  | T_select of 'c * int * 't
+  | T_is_a of 'c * 't
+  | T_other of 't
+
+(** View of types in a way that is directly useful for the theory of datatypes *)
+type ('c, 'ty) data_ty_view =
+  | Ty_arrow of 'ty Iter.t * 'ty
+  | Ty_app of {
+      args: 'ty Iter.t;
+    }
+  | Ty_data of {
+      cstors: 'c;
+    }
+  | Ty_other
+
+module type PROOF = sig
+  type term
+  type lit
+  type proof_step
+  type proof
+
+  val lemma_isa_cstor : cstor_t:term -> term -> proof -> proof_step
+  (** [lemma_isa_cstor (d …) (is-c t)] returns the clause
+      [(c …) = t |- is-c t] or [(d …) = t |- ¬ (is-c t)] *)
+
+  val lemma_select_cstor : cstor_t:term -> term -> proof -> proof_step
+  (** [lemma_select_cstor (c t1…tn) (sel-c-i t)]
+      returns a proof of [t = c t1…tn |- (sel-c-i t) = ti] *)
+
+  val lemma_isa_split : term -> lit Iter.t -> proof -> proof_step
+  (** [lemma_isa_split t lits] is the proof of
+      [is-c1 t \/ is-c2 t \/ … \/ is-c_n t] *)
+
+  val lemma_isa_sel : term -> proof -> proof_step
+  (** [lemma_isa_sel (is-c t)] is the proof of
+      [is-c t |- t = c (sel-c-1 t)…(sel-c-n t)] *)
+
+  val lemma_isa_disj : lit -> lit -> proof -> proof_step
+  (** [lemma_isa_disj (is-c t) (is-d t)] is the proof
+      of [¬ (is-c t) \/ ¬ (is-c t)] *)
+
+  val lemma_cstor_inj : term -> term -> int -> proof -> proof_step
+  (** [lemma_cstor_inj (c t1…tn) (c u1…un) i] is the proof of
+      [c t1…tn = c u1…un |- ti = ui] *)
+
+  val lemma_cstor_distinct : term -> term -> proof -> proof_step
+  (** [lemma_isa_distinct (c …) (d …)] is the proof
+      of the unit clause [|- (c …) ≠ (d …)] *)
+
+  val lemma_acyclicity : (term * term) Iter.t -> proof -> proof_step
+  (** [lemma_acyclicity pairs] is a proof of [t1=u1, …, tn=un |- false]
+      by acyclicity. *)
+end
+
+module type ARG = sig
+  module S : Sidekick_core.SOLVER
+
+  (** Constructor symbols.
+
+      A constructor is an injective symbol, part of a datatype (or "sum type").
+      For example, in [type option a = Some a | None],
+      the constructors are [Some] and [None]. *)
+  module Cstor : sig
+    type t
+    (** Constructor *)
+
+    val ty_args : t -> S.T.Ty.t Iter.t
+    (** Type arguments, for a polymorphic constructor *)
+
+    val pp : t Fmt.printer
+    val equal : t -> t -> bool
+    (** Comparison *)
+  end
+
+  val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) data_ty_view
+  (** Try to view type as a datatype (with its constructors) *)
+
+  val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
+  (** Try to view term as a datatype term *)
+
+  val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
+  (** Make a constructor application term *)
+
+  val mk_is_a: S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t
+  (** Make a [is-a] term *)
+
+  val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
+  (** Make a selector term *)
+
+  val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t
+  (** Make a term equality *)
+
+  val ty_is_finite : S.T.Ty.t -> bool
+  (** Is the given type known to be finite? For example a finite datatype
+      (an "enum" in C parlance), or [Bool], or [Array Bool Bool]. *)
+
+  val ty_set_is_finite : S.T.Ty.t -> bool -> unit
+  (** Modify the "finite" field (see {!ty_is_finite}) *)
+
+  include PROOF
+    with type proof := S.P.t
+     and type proof_step := S.P.proof_step
+     and type term := S.T.Term.t
+     and type lit := S.Lit.t
+end

src/util/Bag.ml

@@ -29,6 +29,17 @@ let cons x t = match t with
   | L _ -> N (L x, t)
   | N (_,_) -> N (L x, t)
 
+let snoc t x = match t with
+  | E -> L x
+  | L _ -> N (t, L x)
+  | N (_, _) -> N (t, L x)
+
+let of_iter i =
+  let r = ref empty in
+
+  i (fun x -> r := snoc !r x);
+  !r
+
 let rec fold f acc = function
   | E -> acc
   | L x -> f acc x

src/util/Bag.mli

@@ -19,8 +19,12 @@ val return : 'a -> 'a t
 
 val cons : 'a -> 'a t -> 'a t
 
+val snoc : 'a t -> 'a -> 'a t
+
 val append : 'a t -> 'a t -> 'a t
 
+val of_iter : 'a Iter.t -> 'a t
+
 val to_iter : 'a t -> 'a Iter.t
 
 val fold : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a

src/util/Chunk_stack.ml

@@ -0,0 +1,174 @@
+
+module Buf = struct
+  type t = {
+    mutable b: bytes;
+    mutable len: int;
+  }
+
+  let create ?(cap=16) () : t =
+    { len=0; b=Bytes.create cap; }
+
+  let[@inline] size self = self.len
+
+  let resize_ self new_len : unit =
+    let size = min (new_len + new_len / 4 + 5) Sys.max_string_length in
+    if new_len > size then failwith "max buf size exceeded";
+
+    let b2 = Bytes.create size in
+    Bytes.blit self.b 0 b2 0 self.len;
+    self.b <- b2
+
+  let[@inline] ensure_size_ (self:t) (new_len:int) : unit =
+    if new_len > Bytes.length self.b then (
+      resize_ self new_len
+    )
+
+  let add_bytes (self:t) (b:bytes) (off:int) (len:int) =
+    Printf.printf "add_bytes len=%d\n%!" len;
+    ensure_size_ self (self.len + len);
+    Bytes.blit b off self.b self.len len;
+    self.len <- self.len + len
+
+  let add_buffer (self:t) (buf:Buffer.t) =
+    ensure_size_ self (size self + Buffer.length buf);
+    Buffer.blit buf 0 self.b self.len (Buffer.length buf)
+
+  let[@inline] add_buf (self:t) (other:t) =
+    add_bytes self other.b 0 other.len
+
+  let clear self = self.len <- 0
+
+  let contents self = Bytes.sub_string self.b 0 self.len
+end
+
+module Writer = struct
+  type t = {
+    write: bytes -> int -> int -> unit;
+    write_buf: Buffer.t -> unit;
+  }
+
+  let nop_ _ = ()
+
+  let dummy : t = {
+    write=(fun _ _ _ -> ());
+    write_buf=(fun _ -> ());
+  }
+
+  let into_buf (into:Buf.t) : t =
+    let blen = Bytes.create 4 in
+    let write b i len =
+      Buf.add_bytes into b i len;
+      (* add len *)
+      Bytes.set_int32_le blen 0 (Int32.of_int len);
+      Buf.add_bytes into blen 0 4;
+    in
+    let write_buf buf =
+      Buf.add_buffer into buf;
+      Bytes.set_int32_le blen 0 (Int32.of_int (Buffer.length buf));
+      Buf.add_bytes into blen 0 4;
+    in
+    { write; write_buf }
+
+  let into_channel (oc:out_channel) : t =
+    let blen = Bytes.create 4 in
+
+    (* add len after chunk *)
+    let[@inline] emit_len_ len =
+      Bytes.set_int32_le blen 0 (Int32.of_int len);
+      output oc blen 0 4;
+      flush oc
+    in
+
+    let write b i len =
+      output oc b i len;
+      emit_len_ len
+
+    and write_buf buf =
+      Buffer.output_buffer oc buf;
+      emit_len_ (Buffer.length buf);
+    in
+    { write; write_buf; }
+
+  let[@inline] add_buf self buf = self.write buf.Buf.b 0 buf.Buf.len
+  let[@inline] add_bytes self b i len = self.write b i len
+  let[@inline] add_string self s =
+    add_bytes self (Bytes.unsafe_of_string s) 0 (String.length s)
+  let[@inline] add_buffer self (buf:Buffer.t) = self.write_buf buf
+end
+
+module Reader = struct
+  type t = {
+    read: 'a. yield:(bytes -> int -> int -> 'a) -> finish:(unit -> 'a) -> 'a;
+  } [@@unboxed]
+
+  let[@inline] next (self:t) ~yield ~finish =
+    self.read ~yield ~finish
+
+  let next_string (self:t) : string option =
+    self.read
+      ~yield:(fun b i len -> Some (Bytes.sub_string b i len))
+      ~finish:(fun () -> None)
+
+  let empty : t = { read=fun ~yield:_ ~finish -> finish() }
+
+  let from_buf (ibuf:Buf.t) : t =
+    let i = ref ibuf.Buf.len in
+
+    (* read next record *)
+    let read ~yield ~finish =
+      if !i > 0 then (
+        Printf.printf "reading (!i = %d)\n%!" !i;
+        assert (!i >= 4);
+
+        i := !i - 4;
+        let chunk_size = Int32.to_int (Bytes.get_int32_le ibuf.Buf.b !i) in
+        Printf.printf "chunk size is %d\n%!" chunk_size;
+
+        i := !i - chunk_size;
+        yield ibuf.Buf.b !i chunk_size
+      ) else (
+        finish()
+      )
+    in
+    { read; }
+
+  let from_channel_backward ?(close_at_end=false) ic =
+    let len = in_channel_length ic in
+    seek_in ic len;
+
+    let buf = Buf.create ~cap:32 () in (* local buffer *)
+
+    let read ~yield ~finish =
+      let pos = pos_in ic in
+      if pos > 0 then (
+        (* read length of preceding chunk *)
+        assert (pos>=4);
+        seek_in ic (pos - 4);
+
+        really_input ic buf.Buf.b 0 4;
+        let chunk_len = Int32.to_int (Bytes.get_int32_le buf.Buf.b 0) in
+
+        (* now read chunk *)
+        Buf.ensure_size_ buf chunk_len;
+        seek_in ic (pos - 4 - chunk_len);
+        really_input ic buf.Buf.b 0 chunk_len;
+        buf.Buf.len <- chunk_len;
+        seek_in ic (pos - 4 - chunk_len);
+
+        yield buf.Buf.b 0 buf.Buf.len
+      ) else (
+        if close_at_end then close_in_noerr ic;
+        finish()
+      )
+    in
+    {read}
+
+  let with_file_backward (filename:string) f =
+    CCIO.with_in ~flags:[Open_binary; Open_rdonly] filename @@ fun ic ->
+    let r = from_channel_backward ~close_at_end:false ic in
+    f r
+end
+
+(*$T
+    false
+    *)

src/util/Chunk_stack.mli

@@ -0,0 +1,69 @@
+
+(** Manage a list of chunks.
+
+    A chunk is used for serializing proof traces, possibly on disk.
+    This way we do not have to keep the whole proof in memory.
+    Each chunk is typically one step of the proof search.
+
+    We produce chunks in forward order (chronological order of their discovery),
+    but once we find a proof of "false", we work our way backward to find
+    chunks transitively needed by this proof of false.
+    Once we obtain this subset of the chunks (as a graph in memory) we can
+    emit a proper proof with no redundant information.
+*)
+
+(** A hand made buffer *)
+module Buf : sig
+  type t = {
+    mutable b: bytes;
+    mutable len: int;
+  }
+
+  val create : ?cap:int -> unit -> t
+
+  val clear : t -> unit
+
+  val contents : t -> string
+end
+
+(** Create a stack of chunks. *)
+module Writer : sig
+  type t
+
+  val dummy : t
+
+  val into_buf : Buf.t -> t
+
+  val into_channel: out_channel -> t
+
+  val add_buf : t -> Buf.t -> unit
+
+  val add_bytes : t -> bytes -> int -> int -> unit
+
+  val add_string : t -> string -> unit
+
+  val add_buffer : t -> Buffer.t -> unit
+end
+
+module Reader : sig
+  type t
+
+  val next : t -> yield:(bytes -> int -> int -> 'a) -> finish:(unit -> 'a) -> 'a
+  (** Read next chunk, call [yield] with a slice of bytes, otherwise call [finish()]. *)
+
+  val next_string : t -> string option
+  (** Read next chunk as a string *)
+
+  val empty : t
+
+  val from_buf : Buf.t -> t
+
+  val from_channel_backward : ?close_at_end:bool -> in_channel -> t
+  (** Read channel from the end, assuming that is possible. *)
+
+  val with_file_backward : string -> (t -> 'a) -> 'a
+  (** [read_file_backward filename f] calls [f] with an iterator
+      over chunks of the file, read from the end.
+
+      Each chunk is assumed to be followed by its length as an int32 LE. *)
+end

src/util/Sidekick_util.ml

@@ -4,9 +4,12 @@ module Fmt = CCFormat
 module Util = Util
 
 module Vec = Vec
+module VecSmallInt = VecSmallInt
 module VecI32 = VecI32
 module Vec_float = Vec_float
+module Vec_unit = Vec_unit
 module Vec_sig = Vec_sig
+
 module Bitvec = Bitvec
 module Int_id = Int_id
 
@@ -26,5 +29,6 @@ module Bag = Bag
 module Stat = Stat
 module Hash = Hash
 module Profile = Profile
+module Chunk_stack = Chunk_stack
 
 module Intf = Sidekick_sigs

src/util/Util.ml

@@ -37,6 +37,9 @@ let array_of_list_map f l =
 let array_to_list_map f arr =
   CCList.init (Array.length arr) (fun i -> f arr.(i))
 
+let lazy_map f x = lazy (let (lazy x) = x in f x)
+let lazy_map2 f x y = lazy (let (lazy x) = x and (lazy y) = y in f x y)
+
 let setup_gc () =
   let g = Gc.get () in
   Gc.set {
@@ -50,3 +53,4 @@ module Int_set = CCSet.Make(CCInt)
 module Int_map = CCMap.Make(CCInt)
 module Int_tbl = CCHashtbl.Make(CCInt)
 
+module Str_tbl = CCHashtbl.Make(CCString)

src/util/Util.mli

@@ -21,9 +21,14 @@ val array_of_list_map : ('a -> 'b) -> 'a list -> 'b array
 
 val array_to_list_map : ('a -> 'b) -> 'a array -> 'b list
 
+val lazy_map : ('a -> 'b) -> 'a lazy_t -> 'b lazy_t
+val lazy_map2 : ('a -> 'b -> 'c) -> 'a lazy_t -> 'b lazy_t -> 'c lazy_t
+
 val setup_gc : unit -> unit
 (** Change parameters of the GC *)
 
 module Int_set : CCSet.S with type elt = int
 module Int_map : CCMap.S with type key = int
 module Int_tbl : CCHashtbl.S with type key = int
+
+module Str_tbl : CCHashtbl.S with type key = string

src/util/Vec.ml

@@ -96,6 +96,16 @@ let[@inline] fast_remove t i =
   Array.unsafe_set t.data i @@ Array.unsafe_get t.data (t.sz - 1);
   t.sz <- t.sz - 1
 
+let append ~into v : unit =
+  if v.sz = 0 then ()
+  else (
+    if v.sz + into.sz > Array.length into.data then (
+      resize_ into v.data.(0) (v.sz + into.sz);
+    );
+    Array.blit v.data 0 into.data into.sz v.sz;
+    into.sz <- into.sz + v.sz;
+  )
+
 let prepend v ~into : unit =
   if v.sz = 0 then ()
   else (
@@ -104,6 +114,7 @@ let prepend v ~into : unit =
     );
     Array.blit into.data 0 into.data v.sz into.sz; (* shift elements *)
     Array.blit v.data 0 into.data 0 v.sz;
+    into.sz <- into.sz + v.sz;
   )
 
 let filter_in_place f vec =

src/util/Vec.mli

@@ -70,6 +70,9 @@ val fast_remove : 'a t -> int -> unit
 (** Remove element at index [i] without preserving order
     (swap with last element) *)
 
+val append : into:'a t -> 'a t -> unit
+(** [append ~into v] pushes elements of [v] in the vector [into] *)
+
 val prepend : 'a t -> into:'a t -> unit
 (** [prepend v ~into] pushes all elements of [v] into [into],
     at the beginning. consumes [v]. *)

src/util/VecI32.ml

@@ -18,6 +18,15 @@ let[@inline] shrink self n = if n < self.sz then self.sz <- n
 let[@inline] size self = self.sz
 let[@inline] is_empty self = self.sz = 0
 
+let copy self =
+  if size self=0 then create ~cap:0 ()
+  else (
+    (* copy bigarray *)
+    let data = mk_arr_ (size self) in
+    A.blit (A.sub self.data 0 (size self)) data;
+    {sz=self.sz; data}
+  )
+
 let[@inline] fast_remove t i =
   assert (i>= 0 && i < t.sz);
   A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);
@@ -26,7 +35,7 @@ let[@inline] fast_remove t i =
 let filter_in_place f vec =
   let i = ref 0 in
   while !i < size vec do
-    if f (Int32.to_int (A.unsafe_get vec.data !i)) then incr i else fast_remove vec !i
+    if f (A.unsafe_get vec.data !i) then incr i else fast_remove vec !i
   done
 
 (* ensure capacity is [new_cap] *)
@@ -50,7 +59,7 @@ let ensure_size self n =
 
 let[@inline] push (self:t) i : unit =
   ensure_cap self (self.sz+1);
-  self.data.{self.sz} <- Int32.of_int i;
+  self.data.{self.sz} <- i;
   self.sz <- 1 + self.sz
 
 let[@inline] push_i32 self i =
@@ -60,39 +69,35 @@ let[@inline] push_i32 self i =
 
 let[@inline] pop self =
   if self.sz > 0 then (
-    let x = Int32.to_int self.data.{self.sz-1} in
+    let x = self.data.{self.sz-1} in
     self.sz <- self.sz - 1;
     x
   ) else failwith "vecI32.pop: empty"
 
-let[@inline] get self i : int =
-  assert (i >= 0 && i < self.sz);
-  Int32.to_int (A.unsafe_get self.data i)
-
-let[@inline] get_i32 self i : int32 =
+let[@inline] get self i : int32 =
   assert (i >= 0 && i < self.sz);
   A.unsafe_get self.data i
 
 let[@inline] set self i x : unit =
   assert (i >= 0 && i < self.sz);
-  A.unsafe_set self.data i (Int32.of_int x)
+  A.unsafe_set self.data i x
 
-let[@inline] set_i32 self i x : unit =
+let[@inline] set self i x : unit =
   assert (i >= 0 && i < self.sz);
   A.unsafe_set self.data i x
 
 let[@inline] iter ~f self =
   for i=0 to self.sz - 1 do
-    f (Int32.to_int self.data.{i})
+    f self.data.{i}
   done
 
 let[@inline] iteri ~f self =
   for i=0 to self.sz - 1 do
-    f i (Int32.to_int self.data.{i})
+    f i self.data.{i}
   done
 
 include Vec_sig.Make_extensions(struct
-    type nonrec elt = int
+    type nonrec elt = int32
     type nonrec t = t
     let get = get
     let size = size

src/util/VecI32.mli

@@ -3,13 +3,4 @@
 
     These vectors are more optimized than {!Vec}. *)
 
-include Vec_sig.S with type elt := int
-
-val ensure_size : t -> int -> unit
-
-val push_i32 : t -> int32 -> unit
-
-val get_i32 : t -> int -> int32
-
-val set_i32 : t -> int -> int32 -> unit
-
+include Vec_sig.S with type elt := int32

src/util/VecSmallInt.ml

@@ -0,0 +1,110 @@
+
+module A = Bigarray.Array1
+
+type int32arr = (int32, Bigarray.int32_elt, Bigarray.c_layout) A.t
+
+type t = {
+  mutable data: int32arr;
+  mutable sz: int;
+}
+
+let mk_arr_ sz : int32arr = A.create Bigarray.int32 Bigarray.c_layout sz
+
+let create ?(cap=16) () : t =
+  { sz=0; data=mk_arr_ cap }
+
+let[@inline] clear self = self.sz <- 0
+let[@inline] shrink self n = if n < self.sz then self.sz <- n
+let[@inline] size self = self.sz
+let[@inline] is_empty self = self.sz = 0
+
+let copy self =
+  if size self=0 then create ~cap:0 ()
+  else (
+    (* copy bigarray *)
+    let data = mk_arr_ (size self) in
+    A.blit self.data data;
+    {sz=self.sz; data}
+  )
+
+let[@inline] fast_remove t i =
+  assert (i>= 0 && i < t.sz);
+  A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);
+  t.sz <- t.sz - 1
+
+let filter_in_place f vec =
+  let i = ref 0 in
+  while !i < size vec do
+    if f (Int32.to_int (A.unsafe_get vec.data !i)) then incr i else fast_remove vec !i
+  done
+
+(* ensure capacity is [new_cap] *)
+let resize_cap_ self new_cap =
+  assert (A.dim self.data < new_cap);
+  let new_data = mk_arr_ new_cap in
+  A.blit self.data (A.sub new_data 0 (A.dim self.data));
+  self.data <- new_data
+
+let ensure_cap self (n:int) =
+  if n > A.dim self.data then (
+    let new_cap = max n (max 4 (A.dim self.data * 2)) in
+    resize_cap_ self new_cap;
+  )
+
+let ensure_size self n =
+  if n > self.sz then (
+    ensure_cap self n;
+    self.sz <- n
+  )
+
+let[@inline] push (self:t) i : unit =
+  ensure_cap self (self.sz+1);
+  self.data.{self.sz} <- Int32.of_int i;
+  self.sz <- 1 + self.sz
+
+let[@inline] push_i32 self i =
+  ensure_cap self (self.sz+1);
+  self.data.{self.sz} <- i;
+  self.sz <- 1 + self.sz
+
+let[@inline] pop self =
+  if self.sz > 0 then (
+    let x = Int32.to_int self.data.{self.sz-1} in
+    self.sz <- self.sz - 1;
+    x
+  ) else failwith "vecI32.pop: empty"
+
+let[@inline] get self i : int =
+  assert (i >= 0 && i < self.sz);
+  Int32.to_int (A.unsafe_get self.data i)
+
+let[@inline] get_i32 self i : int32 =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_get self.data i
+
+let[@inline] set self i x : unit =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_set self.data i (Int32.of_int x)
+
+let[@inline] set_i32 self i x : unit =
+  assert (i >= 0 && i < self.sz);
+  A.unsafe_set self.data i x
+
+let[@inline] iter ~f self =
+  for i=0 to self.sz - 1 do
+    f (Int32.to_int self.data.{i})
+  done
+
+let[@inline] iteri ~f self =
+  for i=0 to self.sz - 1 do
+    f i (Int32.to_int self.data.{i})
+  done
+
+include Vec_sig.Make_extensions(struct
+    type nonrec elt = int
+    type nonrec t = t
+    let get = get
+    let size = size
+    let iter = iter
+    let iteri = iteri
+  end)

src/util/VecSmallInt.mli

@@ -0,0 +1,13 @@
+
+(** Vectors of int32 integers
+
+    These vectors are more optimized than {!Vec}. *)
+
+include Vec_sig.S with type elt := int
+
+val push_i32 : t -> int32 -> unit
+
+val get_i32 : t -> int -> int32
+
+val set_i32 : t -> int -> int32 -> unit
+

src/util/Vec_float.ml

@@ -18,6 +18,15 @@ let[@inline] shrink self n = if n < self.sz then self.sz <- n
 let[@inline] size self = self.sz
 let[@inline] is_empty self = self.sz = 0
 
+let copy self =
+  if size self=0 then create ~cap:0 ()
+  else (
+    (* copy bigarray *)
+    let data = mk_arr_ (size self) in
+    A.blit (A.sub self.data 0 (size self)) data;
+    {sz=self.sz; data}
+  )
+
 let[@inline] fast_remove t i =
   assert (i>= 0 && i < t.sz);
   A.unsafe_set t.data i @@ A.unsafe_get t.data (t.sz - 1);

src/util/Vec_float.mli

@@ -4,5 +4,3 @@
     These vectors are more optimized than {!Vec}. *)
 
 include Vec_sig.S with type elt := float
-
-val ensure_size : t -> int -> unit

src/util/Vec_sig.ml

@@ -19,6 +19,8 @@ module type BASE = sig
 
   val clear : t -> unit
 
+  val copy : t -> t
+
   val is_empty : t -> bool
 
   val push : t -> elt -> unit
@@ -29,6 +31,8 @@ module type BASE = sig
 
   val filter_in_place : (elt -> bool) -> t -> unit
 
+  val ensure_size : t -> int -> unit
+
   val pop : t -> elt
 
   val set : t -> int -> elt -> unit

src/util/Vec_unit.ml

@@ -0,0 +1,28 @@
+
+type elt = unit
+
+(* no need to store anything so we don't even provide an actual vector
+   since unit is a "zero sized type" as rustaceans would say. *)
+type t = {
+  mutable size: int;
+}
+
+let create ?cap:_ () : t = { size=0 }
+let clear self = self.size <- 0
+let copy {size} = {size}
+let get (_self:t) _ = ()
+let size self = self.size
+let iter ~f:_ (_self:t) = ()
+let iteri ~f:_ (_self:t) = ()
+let is_empty self = self.size = 0
+let push (self:t) _ = self.size <- 1 + self.size
+let fast_remove (self:t) _ = self.size <- self.size - 1
+let ensure_size (self:t) i = self.size <- max self.size i
+let set _ _ _ = ()
+let pop self = self.size <- self.size - 1; ()
+let filter_in_place _ _ = ()
+let shrink (self:t) i = self.size <- i
+let to_iter self k = for _i=0 to self.size - 1 do k () done
+let to_array self = Iter.to_array (to_iter self)
+let fold_left f acc self = Iter.fold f acc (to_iter self)
+let pp ppx out self = Iter.pp_seq ppx out (to_iter self)

src/util/Vec_unit.mli

@@ -0,0 +1,2 @@
+
+include Vec_sig.S with type elt= unit

src/util/tests/sidekick_test_util.ml

@@ -1,5 +1,8 @@
 
-let tests = [Test_bitvec.tests]
+let tests = [
+  Test_bitvec.tests;
+  Test_chunk_stack.tests
+]
 
 let props = [
 ]

src/util/tests/test_chunk_stack.ml

@@ -0,0 +1,43 @@
+
+module A = Alcotest
+module C = Chunk_stack
+
+let l : unit Alcotest.test_case list ref = ref []
+
+let (~!) = Printf.sprintf "at line %d"
+let mk_test ?(speed=`Quick) name f =
+  l := (name, speed, f) :: !l
+
+let () = mk_test "inbuf" @@ fun () ->
+  let buf = C.Buf.create() in
+
+  let writer = C.Writer.into_buf buf in
+  C.Writer.add_string writer "hello";
+  C.Writer.add_string writer "world";
+  C.Writer.add_string writer "!!\x00!";
+
+  let reader = C.Reader.from_buf buf in
+  A.check A.(option string) ~!__LINE__ (Some "!!\x00!") (C.Reader.next_string reader);
+  A.check A.(option string) ~!__LINE__ (Some "world") (C.Reader.next_string reader);
+  A.check A.(option string) ~!__LINE__ (Some "hello") (C.Reader.next_string reader);
+  A.check A.(option string) ~!__LINE__ None (C.Reader.next_string reader);
+  ()
+
+let () = mk_test ~speed:`Slow "infile" @@ fun () ->
+  CCIO.File.with_temp ~prefix:"sidekick-test" ~suffix:"dat"
+    (fun file ->
+       CCIO.with_out file (fun oc ->
+           let writer = C.Writer.into_channel oc in
+           C.Writer.add_string writer "hello";
+           C.Writer.add_string writer "world";
+           C.Writer.add_string writer "!!\x00!");
+
+       C.Reader.with_file_backward file (fun reader ->
+           A.check A.(option string) ~!__LINE__ (Some "!!\x00!") (C.Reader.next_string reader);
+           A.check A.(option string) ~!__LINE__ (Some "world") (C.Reader.next_string reader);
+           A.check A.(option string) ~!__LINE__ (Some "hello") (C.Reader.next_string reader);
+           A.check A.(option string) ~!__LINE__ None (C.Reader.next_string reader));
+       ()
+    )
+
+let tests = "chunk_stack", !l