feat(proof): progress on preprocessing; proper proofs for th-bool

src/base-term/Proof.ml

@@ -11,7 +11,7 @@ type lit =
   | L_a of term
   | L_na of term
 
-let not = function
+let lit_not = function
   | L_eq (a,b) -> L_neq(a,b)
   | L_neq (a,b) -> L_eq(a,b)
   | L_a t -> L_na t
@@ -23,11 +23,11 @@ let pp_lit out = function
   | L_a t -> Fmt.fprintf out "(@[+@ %a@])" T.pp t
   | L_na t -> Fmt.fprintf out "(@[-@ %a@])" T.pp t
 
-let a t = L_a t
+let lit_a t = L_a t
-let na t = L_na t
+let lit_na t = L_na t
-let eq t u = L_eq (t,u)
+let lit_eq t u = L_eq (t,u)
-let neq t u = L_neq (t,u)
+let lit_neq t u = L_neq (t,u)
-let lit_st (t,b) = if b then a t else na t
+let lit_st (t,b) = if b then lit_a t else lit_na t
 
 type clause = lit list
 
@@ -48,8 +48,10 @@ type t =
   | Bool_true_is_true
   | Bool_true_neq_false
   | Bool_eq of term * term (* equal by pure boolean reasoning *)
+  | Bool_c of clause (* boolean tautology *)
   | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *)
   | Ite_false of term
+  | With_def of term list * t (* [with_def ts p] is [p] using definitions of [ts] *)
   | LRA of clause
   | Composite of {
       (* some named (atomic) assumptions *)
@@ -63,11 +65,10 @@ and composite_step =
       res: clause; (* result of [proof] *)
       proof: t; (* sub-proof *)
     }
+  | S_define_t of term * term (* [const := t] *)
 
-  (* TODO: do we need that here? or is it only during printing
+  (* TODO: step to name a term (not define it), to keep sharing?
-     that it becomes important?
+     or do we do that when we print/serialize the proof *)
-  | S_define_t of string * term (* name this term *)
-     *)
 
 and hres_step =
   | R of { pivot: term; p: t}
@@ -80,8 +81,12 @@ let r1 p = R1 p
 let p p ~lhs ~rhs : hres_step = P { p; lhs; rhs }
 let p1 p = P1 p
 
-let defc ~name res proof : composite_step =
+let defc ~name res proof : composite_step = S_define_c {proof;name;res}
-  S_define_c {proof;name;res}
+let deft c rhs : composite_step = S_define_t (c,rhs)
+
+let is_trivial_refl = function
+  | Refl _ -> true
+  | _ -> false
 
 let default=Unspecified
 let sorry_c c = Sorry_c (Iter.to_rev_list c)
@@ -96,6 +101,7 @@ 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 with_defs ts p = match ts with [] -> p | _ -> With_def (ts, p)
 let composite_l ?(assms=[]) steps : t =
   Composite {assumptions=assms; steps}
 let composite_iter ?(assms=[]) steps : t =
@@ -111,6 +117,7 @@ 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 c : t = Bool_c c
 
 let hres_l c l : t = Hres (c,l)
 let hres_iter c i : t = Hres (c, Iter.to_list i)
@@ -142,11 +149,12 @@ module Quip = struct
     | Bool_true_is_true -> Fmt.string out "true-is-true"
     | Bool_true_neq_false -> Fmt.string out "(@[!= T F@])"
     | Bool_eq (a,b) -> Fmt.fprintf out "(@[bool-eq@ %a@ %a@])" T.pp a T.pp b
+    | Bool_c c -> Fmt.fprintf out "(@[bool-c@ %a@])" pp_cl c
     | Assertion t -> Fmt.fprintf out "(@[assert@ %a@])" T.pp t
     | Assertion_c c ->
       Fmt.fprintf out "(@[assert-c@ %a@])" pp_cl c
     | Hres (c, l) ->
-      Fmt.fprintf out "(@[hres@ (@[init@ %a@]) %a@])" pp_rec c
+      Fmt.fprintf out "(@[hres@ (@[init@ %a@])@ %a@])" pp_rec c
         (pp_l pp_hres_step) l
     | DT_isa_split (ty,l) ->
       Fmt.fprintf out "(@[dt.isa.split@ (@[ty %a@])@ (@[cases@ %a@])@])"
@@ -158,6 +166,8 @@ module Quip = struct
         i Cstor.pp c (pp_l T.pp) ts Cstor.pp c (pp_l T.pp) us
     | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" T.pp t
     | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" T.pp t
+    | With_def (ts,p) ->
+      Fmt.fprintf out "(@[with-defs (@[%a@])@ %a@])" (pp_l T.pp) ts pp_rec p
     | LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c
     | Composite {steps; assumptions} ->
       let pp_ass out (n,a) = Fmt.fprintf out "(@[assuming@ (name %s) %a@])" n pp_lit a in
@@ -166,7 +176,10 @@ module Quip = struct
 
   and pp_composite_step out = function
     | S_define_c {name;res;proof} ->
-      Fmt.fprintf out "(@[defc %s %a@ %a@])" name pp_cl res pp_rec proof
+      Fmt.fprintf out "(@[defc %s@ %a@ %a@])" name pp_cl res pp_rec proof
+    | S_define_t (c,rhs) ->
+      Fmt.fprintf out "(@[deft@ %a@ %a@])" Term.pp c Term.pp rhs
+
   (*
     | S_define_t (name, t) ->
       Fmt.fprintf out "(@[deft %s %a@])" name Term.pp t

src/base-term/Proof.mli

@@ -9,6 +9,7 @@ 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 : lit list -> t
 val ite_true : term -> t
 val ite_false : term -> t
 

src/cc/Sidekick_cc.ml

@@ -661,7 +661,7 @@ module Make (A: CC_ARG)
         let proof =
           let lits =
             Iter.of_list lits
-            |> Iter.map (fun lit -> P.lit_st (Lit.signed_term lit))
+            |> Iter.map (fun lit -> P.lit_not @@ P.lit_st (Lit.signed_term lit))
           in
           P.cc_lemma lits
         in

src/core/Sidekick_core.ml

@@ -170,15 +170,21 @@ module type PROOF = sig
   (** Proof representation of literals *)
 
   val pp_lit : lit Fmt.printer
-  val a : term -> lit
+  val lit_a : term -> lit
-  val na : term -> lit
+  val lit_na : term -> lit
   val lit_st : term * bool -> lit
-  val eq : term -> term -> lit
+  val lit_eq : term -> term -> lit
-  val neq : term -> term -> lit
+  val lit_neq : term -> term -> lit
-  val not : lit -> lit
+  val lit_not : lit -> lit
 
   type composite_step
   val defc : name:string -> lit list -> t -> composite_step
+  val deft : term -> term -> composite_step (** define a (new) atomic term *)
+
+  val is_trivial_refl : t -> bool
+  (** is this a proof of [|- t=t]? This can be used to remove
+      some trivial steps that would build on the proof (e.g. rewriting
+      using [refl t] is useless). *)
 
   val assertion : term -> t
   val assertion_c : lit Iter.t -> t
@@ -189,6 +195,7 @@ module type PROOF = sig
   val refl : term -> t (* proof of [| t=t] *)
   val true_is_true : t (* proof of [|- true] *)
   val true_neq_false : t (* proof of [|- not (true=false)] *)
+  val with_defs : term list -> t -> t (* proof under definition of given terms *)
   val cc_lemma : lit Iter.t -> t (* equality tautology, unsigned *)
   val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *)
   val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *)
@@ -585,8 +592,16 @@ 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 *)
   module CC : CC_S
     with module T = T
      and module P = P
@@ -966,18 +981,22 @@ module type SOLVER = sig
 
   val add_theory_l : t -> theory list -> unit
 
-  val mk_atom_lit : t -> lit -> Atom.t
+  val mk_atom_lit : t -> lit -> Atom.t * P.t
-  (** Turn a literal into a SAT solver literal. *)
+  (** [mk_atom_lit _ lit] returns [atom, pr]
+      where [atom] is an internal atom for the solver,
+      and [pr] is a proof of [|- lit = atom] *)
 
-  val mk_atom_t : t -> ?sign:bool -> term -> Atom.t
+  val mk_atom_t : t -> ?sign:bool -> term -> Atom.t * P.t
-  (** Turn a boolean term, with a sign, into a SAT solver's literal. *)
+  (** [mk_atom_t _ ~sign t] returns [atom, pr]
+      where [atom] is an internal representation of [± t],
+      and [pr] is a proof of [|- atom = (± t)] *)
 
   val add_clause : t -> Atom.t IArray.t -> P.t -> 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 -> Atom.t list -> P.t -> unit
-  (** Same as {!add_clause} but with a list of atoms. *)
+  (** Add a clause to the solver, given as a list. *)
 
   (** {2 Internal representation of proofs}
 

src/lra/sidekick_arith_lra.ml

@@ -212,6 +212,7 @@ module Make(A : ARG) : S with module A = A = struct
       | exception Not_found ->
         (* new variable to represent [le_comb] *)
         let proxy = fresh_term self ~pre (A.ty_lra self.tst) in
+        (* TODO: define proxy *)
         self.encoded_le <- Comb_map.add le_comb proxy self.encoded_le;
         Log.debugf 50
           (fun k->k "(@[lra.encode-le@ `%a`@ :into-var %a@])" LE_.Comb.pp le_comb T.pp proxy);
@@ -269,10 +270,10 @@ module Make(A : ARG) : S with module A = A = struct
         let lit_t = mk_lit t in
         let lit_u1 = mk_lit u1 in
         let lit_u2 = mk_lit u2 in
-        add_clause [SI.Lit.neg lit_t; lit_u1] A.S.P.(A.proof_lra_l [na t; a u1]) ;
+        add_clause [SI.Lit.neg lit_t; lit_u1] A.S.P.(A.proof_lra_l [lit_na t; lit_a u1]) ;
-        add_clause [SI.Lit.neg lit_t; lit_u2] A.S.P.(A.proof_lra_l [na t; a u2]);
+        add_clause [SI.Lit.neg lit_t; lit_u2] A.S.P.(A.proof_lra_l [lit_na t; lit_a u2]);
         add_clause [SI.Lit.neg lit_u1; SI.Lit.neg lit_u2; lit_t]
-          A.S.P.(A.proof_lra_l [a t;na u1;na u2]);
+          A.S.P.(A.proof_lra_l [lit_a t; lit_na u1; lit_na u2]);
       );
       None
 

src/msat-solver/Sidekick_msat_solver.ml

@@ -196,7 +196,8 @@ module Make(A : ARG)
       simp: Simplify.t;
       mutable preprocess: preprocess_hook list;
       mutable mk_model: model_hook list;
-      preprocess_cache: (Term.t * P.t) Term.Tbl.t;
+      preprocess_cache: (Term.t * P.t list) Term.Tbl.t;
+      mutable t_defs : (term*term) list; (* term definitions *)
       mutable th_states : th_states; (** Set of theories *)
       mutable on_partial_check: (t -> actions -> lit Iter.t -> unit) list;
       mutable on_final_check: (t -> actions -> lit Iter.t -> unit) list;
@@ -231,6 +232,9 @@ module Make(A : ARG)
     let[@inline] ty_st t = t.ty_st
     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 * P.t = Simplify.normalize_t self.simp t
@@ -262,12 +266,15 @@ module Make(A : ARG)
     let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
       let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
 
-      (* compute and cache normal form of [t] *)
+      (* compute and cache normal form [u] of [t].
-      let rec aux t : term * proof =
+         Also cache a list of proofs [ps] such
+         that [ps |- t=u] by CC. *)
+      let rec aux t : term * proof list =
         match Term.Tbl.find self.preprocess_cache t with
-        | up -> up
+        | u, ps ->
+          u, ps
         | exception Not_found ->
-          let sub_p = ref [] in
+          let sub_p: P.t list ref = ref [] in
 
           (* try rewrite at root *)
           let t1 = aux_rec ~sub_p t self.preprocess in
@@ -276,9 +283,9 @@ module Make(A : ARG)
           let t2 =
             Term.map_shallow self.tst
               (fun t_sub ->
-                 let u_sub, p_t = aux t_sub in
+                 let u_sub, ps_t = aux t_sub in
                  if not (Term.equal t_sub u_sub) then (
-                   sub_p := p_t :: !sub_p;
+                   sub_p := List.rev_append ps_t !sub_p;
                  );
                  u_sub)
               t1
@@ -287,9 +294,9 @@ module Make(A : ARG)
           let u =
             if not (Term.equal t t2) then (
               (* fixpoint *)
-              let v, p_t2_v = aux t2 in
+              let v, ps_t2_v = aux t2 in
               if not (Term.equal t2 v) then (
-                sub_p := p_t2_v :: !sub_p
+                sub_p := List.rev_append ps_t2_v !sub_p
               );
               v
             ) else (
@@ -299,18 +306,12 @@ module Make(A : ARG)
 
           if t != u then (
             Log.debugf 5
-              (fun k->k "(@[msat-solver.preprocess.term@ \
+              (fun k->k "(@[msat-solver.preprocess.term@ :from %a@ :to %a@])"
-                         :from %a@ :to %a@])" Term.pp t Term.pp u);
+                  Term.pp t Term.pp u);
           );
 
-          let p_t_u =
+          Term.Tbl.add self.preprocess_cache t (u,!sub_p);
-            if t != u then (
+          u, !sub_p
-              P.cc_imply_l !sub_p t u (* proof: [sub_p |- t=u] *)
-            ) else P.refl t
-          in
-
-          Term.Tbl.add self.preprocess_cache t (u,p_t_u);
-          u, p_t_u
 
       (* try each function in [hooks] successively *)
       and aux_rec ~sub_p t hooks : term =
@@ -319,32 +320,41 @@ module Make(A : ARG)
         | h :: hooks_tl ->
           match h self ~mk_lit ~add_clause t with
           | None -> aux_rec ~sub_p t hooks_tl
-          | Some (u, p_t_u) ->
+          | Some (u, ps_t_u) ->
-            sub_p := p_t_u :: !sub_p;
+            sub_p := ps_t_u :: !sub_p;
-            let v, p_u_v = aux u in
+            let v, ps_u_v = aux u in
             if t != v then (
-              sub_p := p_u_v :: !sub_p;
+              sub_p := List.rev_append ps_u_v !sub_p;
             );
             v
       in
 
       let t1, p_t_t1 = simp_t self t in
 
-      let u, p_t1_u = aux t1 in
+      let u, ps_t1_u = aux t1 in
+
+      let pr_t_u =
         if t != u then (
-        let pr = P.cc_imply2 p_t_t1 p_t1_u t u in
+          let hyps =
-        u, pr
+            if t == t1 then ps_t1_u
-      ) else (
+            else p_t_t1 :: ps_t1_u in
-        u, P.refl u
+          P.cc_imply_l hyps t u
-      )
+        ) else P.refl u
+      in
+
+      u, pr_t_u
 
     (* return preprocessed lit + proof they are equal *)
     let preprocess_lit_ (self:t) ~add_clause (lit:lit) : lit * proof =
       let t, p = Lit.term lit |> preprocess_term_ self ~add_clause in
       let lit' = Lit.atom self.tst ~sign:(Lit.sign lit) t in
+
+      if not (Lit.equal lit lit') then (
         Log.debugf 10
           (fun k->k "(@[msat-solver.preprocess.lit@ :lit %a@ :into %a@ :proof %a@])"
-            Lit.pp lit Lit.pp lit' P.Quip.pp p);
+              Lit.pp lit Lit.pp lit' P.pp_debug p);
+      );
+
       lit', p
 
     (* add a clause using [acts] *)
@@ -491,6 +501,7 @@ module Make(A : ARG)
         count_preprocess_clause = Stat.mk_int stat "solver.preprocess-clause";
         count_propagate = Stat.mk_int stat "solver.th-propagations";
         count_conflict = Stat.mk_int stat "solver.th-conflicts";
+        t_defs=[];
         on_partial_check=[];
         on_final_check=[];
         level=0;
@@ -511,6 +522,7 @@ module Make(A : ARG)
 
     type t = {
       msat: Sat_solver.proof;
+      tdefs: (term*term) list; (* term definitions *)
       p: P.t lazy_t;
     }
 
@@ -531,7 +543,7 @@ module Make(A : ARG)
          clause [c] under given assumptions (each assm is a lit),
          and return [-a1 \/ … \/ -an \/ c], discharging assumptions
     *)
-    let conv_proof (msat:Sat_solver.proof) : P.t =
+    let conv_proof (msat:Sat_solver.proof) (t_defs:_ list) : P.t =
       let assms = ref [] in
       let steps = ref [] in
 
@@ -618,10 +630,13 @@ module Make(A : ARG)
       (* this should traverse from the leaves, so that order of [steps] is correct *)
       Sat_solver.Proof.fold tr_node_to_step () msat;
       let assms = !assms in
-      P.composite_l ~assms (List.rev !steps)
 
-    let make (msat: Sat_solver.proof) : t =
+      (* gather all term definitions *)
-      { msat; p=lazy (conv_proof msat) }
+      let t_defs = CCList.map (fun (c,rhs) -> P.deft c rhs) t_defs in
+      P.composite_l ~assms (CCList.append t_defs (List.rev !steps))
+
+    let make (msat: Sat_solver.proof) (tdefs: _ list) : t =
+      { msat; tdefs; p=lazy (conv_proof msat tdefs) }
 
     let check self = SP.check self.msat
     let pp out (self:t) = P.Quip.pp out (to_proof self)
@@ -726,21 +741,36 @@ module Make(A : ARG)
          CC.set_as_lit cc (CC.add_term cc sub ) (Sat_solver.Atom.formula atom);
          ())
 
-  let rec mk_atom_lit self lit : Atom.t =
+  let rec mk_atom_lit self lit : Atom.t * P.t =
-    let lit, _proof = preprocess_lit_ self lit in
+    let lit, proof = preprocess_lit_ self lit in
     add_bool_subterms_ self (Lit.term lit);
-    Sat_solver.make_atom self.solver lit
+    Sat_solver.make_atom self.solver lit, proof
 
   and preprocess_lit_ self lit : Lit.t * P.t =
     Solver_internal.preprocess_lit_
       ~add_clause:(fun lits proof ->
           (* recursively add these sub-literals, so they're also properly processed *)
           Stat.incr self.si.count_preprocess_clause;
-          let atoms = List.map (mk_atom_lit self) lits in
+          let pr_l = ref [] in
+          let atoms =
+            List.map
+              (fun lit ->
+                 let a, pr = mk_atom_lit self lit in
+                 if not (P.is_trivial_refl pr) then (
+                   pr_l := pr :: !pr_l;
+                 );
+                 a)
+              lits
+          in
+          (* do paramodulation if needed *)
+          let proof =
+            if !pr_l=[] then proof
+            else P.(hres_l proof (List.rev_map p1 !pr_l))
+          in
           Sat_solver.add_clause self.solver atoms proof)
       self.si lit
 
-  let[@inline] mk_atom_t self ?sign t : Atom.t =
+  let[@inline] mk_atom_t self ?sign t : Atom.t * P.t =
     let lit = Lit.atom (tst self) ?sign t in
     mk_atom_lit self lit
 
@@ -896,7 +926,7 @@ module Make(A : ARG)
         try
           let pr = us.get_proof () in
           if check then Sat_solver.Proof.check pr;
-          Some (Pre_proof.make pr)
+          Some (Pre_proof.make pr (List.rev self.si.t_defs))
         with Msat.Solver_intf.No_proof -> None
       ) in
       let unsat_core = lazy (us.Msat.unsat_assumptions ()) in

src/smtlib/Process.ml

@@ -250,8 +250,13 @@ let process_stmt
       Log.debug 1 "exit";
       raise Exit
     | Statement.Stmt_check_sat l ->
+      (* FIXME: how to map [l] to [assumptions] in proof? *)
       let assumptions =
-        List.map (fun (sign,t) -> Solver.mk_atom_t solver ~sign t) l
+        List.map
+          (fun (sign,t) ->
+             let a, _pr = Solver.mk_atom_t solver ~sign t in
+             a)
+          l
       in
       solve
         ?gc ?restarts ?dot_proof ~check ?pp_proof ?pp_model
@@ -265,23 +270,41 @@ let process_stmt
     | Statement.Stmt_decl (f,ty_args,ty_ret) ->
       decl_fun f ty_args ty_ret;
       E.return ()
+
     | Statement.Stmt_assert t ->
       if pp_cnf then (
         Format.printf "(@[<hv1>assert@ %a@])@." Term.pp t
       );
-      let atom = Solver.mk_atom_t solver t in
+      let atom, pr_atom = Solver.mk_atom_t solver t in
       CCOpt.iter (fun h -> Vec.push h [atom]) hyps;
-      Solver.add_clause solver (IArray.singleton atom) (Proof.assertion t);
+      Solver.add_clause solver (IArray.singleton atom)
+        Proof.(hres_l (assertion t) [p1 pr_atom]);
       E.return()
+
     | Statement.Stmt_assert_clause c_ts ->
       if pp_cnf then (
         Format.printf "(@[<hv1>assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts
       );
-      let c = List.map (Solver.mk_atom_t solver) c_ts in
+      let pr_l = ref [] in
+      let c =
+        List.map
+          (fun lit ->
+             let a, pr = Solver.mk_atom_t solver lit in
+             if not (Proof.is_trivial_refl pr) then pr_l := pr :: !pr_l;
+             a)
+          c_ts in
       CCOpt.iter (fun h -> Vec.push h c) hyps;
-      let proof = Proof.(assertion_c (Iter.of_list c_ts |> Iter.map (fun t->a t))) in
+
+      let proof =
+        let open Proof in
+        let p = assertion_c (Iter.of_list c_ts |> Iter.map (fun t->lit_a t)) in
+        (* rewrite with preprocessing proofs *)
+        if !pr_l = [] then p else hres_l p (List.rev_map p1 !pr_l)
+      in
+
       Solver.add_clause solver (IArray.of_list c) proof ;
       E.return()
+
     | Statement.Stmt_data _ ->
       E.return()
     | Statement.Stmt_define _ ->
@@ -333,7 +356,8 @@ module Th_bool = Sidekick_th_bool_static.Make(struct
   module S = Solver
   type term = S.T.Term.t
   include Form
-  let proof_bool = Proof.bool_eq
+  let proof_bool_eq = Proof.bool_eq
+  let proof_bool_c = Proof.bool_c
   let proof_ite_true = Proof.ite_true
   let proof_ite_false = Proof.ite_false
 end)

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -33,8 +33,11 @@ module type ARG = sig
   (** [proof_ite_false (ite a b c)] is [a=false |- ite a b c = c] *)
   val proof_ite_false : S.T.Term.t -> S.P.t
 
-  (** By basic boolean logic to prove [a=b] *)
+  (** Basic boolean logic for [|- a=b] *)
-  val proof_bool : S.T.Term.t -> S.T.Term.t -> S.P.t
+  val proof_bool_eq : S.T.Term.t -> S.T.Term.t -> S.P.t
+
+  (** Basic boolean logic for a clause [|- c] *)
+  val proof_bool_c : S.P.lit list -> S.P.t
 
   val mk_bool : S.T.Term.state -> (term, term IArray.t) bool_view -> term
   (** Make a term from the given boolean view. *)
@@ -117,7 +120,7 @@ module Make(A : ARG) : S with module A = A = struct
 
   let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.P.t) option =
     let tst = self.tst in
-    let ret u = Some (u, A.proof_bool t u) in
+    let ret u = Some (u, A.proof_bool_eq t u) in
     match A.view_as_bool t with
     | B_bool _ -> None
     | B_not u when is_true u -> ret (T.bool tst false)
@@ -172,9 +175,9 @@ module Make(A : ARG) : S with module A = A = struct
     assert (Ty.equal ty (T.ty u));
     u
 
-  let fresh_lit (self:state) ~for_ ~mk_lit ~pre : Lit.t =
+  let fresh_lit (self:state) ~for_ ~mk_lit ~pre : T.t * Lit.t =
     let proxy = fresh_term ~for_ ~pre self (Ty.bool self.ty_st) in
-    mk_lit proxy
+    proxy, mk_lit proxy
 
   (* preprocess "ite" away *)
   let preproc_ite self si ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
@@ -192,18 +195,26 @@ module Make(A : ARG) : S with module A = A = struct
           Some (c, proof)
         | _ ->
           let t_ite = fresh_term self ~for_:t ~pre:"ite" (T.ty b) in
+          SI.define_const si ~const:t_ite ~rhs:t;
           let lit_a = mk_lit a in
-          let pr = SI.P.sorry in (* FIXME: proper proof by-def(t_ite) + bool *)
+          add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)]
-          add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] pr;
+            SI.P.(with_defs [t_ite] (A.proof_ite_true t));
-          add_clause [lit_a; mk_lit (eq self.tst t_ite c)] pr;
+          add_clause [lit_a; mk_lit (eq self.tst t_ite c)]
-          (* TODO: by def t_ite + ite-true + ite-false
+            SI.P.(with_defs [t_ite] (A.proof_ite_false t));
-             + case split [a=true \/ a=false] *)
+          Some (t_ite, SI.P.(with_defs [t_ite] (refl t)))
-          Some (t_ite, SI.P.sorry)
       end
     | _ -> None
 
+  let[@inline] pr_lit lit = SI.P.(lit_st (Lit.signed_term lit))
+  let[@inline] pr_def_refl proxy t = SI.P.(with_defs [proxy] (refl t))
+
+  (* prove clause [l] by boolean lemma *)
+  let pr_bool_c proxy l : SI.P.t =
+    let cl = List.rev_map pr_lit l in
+    SI.P.(with_defs [proxy] (A.proof_bool_c cl))
+
   (* TODO: polarity? *)
-  let cnf (self:state) (_si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
+  let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =
     let rec get_lit_and_proof_ (t:T.t) : Lit.t * SI.P.t =
       let t_abs, t_sign = T.abs self.tst t in
       let lit_abs, pr =
@@ -211,7 +222,7 @@ module Make(A : ARG) : S with module A = A = struct
         | lit_pr -> lit_pr (* cached *)
         | exception Not_found ->
           (* compute and cache *)
-          let lit, pr = get_lit_uncached t_abs in
+          let lit, pr = get_lit_uncached si t_abs in
           if not (T.equal (Lit.term lit) t_abs) then (
             T.Tbl.add self.cnf t_abs (lit, pr);
             Log.debugf 20
@@ -224,22 +235,27 @@ module Make(A : ARG) : S with module A = A = struct
       let lit = if t_sign then lit_abs else Lit.neg lit_abs in
       lit, pr
 
-    and equiv_ ~get_lit ~is_xor ~for_ a b : Lit.t =
+    and equiv_ si ~get_lit ~is_xor ~for_ t_a t_b : Lit.t * SI.P.t =
-      let a = get_lit a in
+      let a = get_lit t_a in
-      let b = get_lit b in
+      let b = get_lit t_b in
       let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
-      let proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
+      let t_proxy, proxy = fresh_lit ~for_ ~mk_lit ~pre:"equiv_" self in
+
+      SI.define_const si ~const:t_proxy ~rhs:for_;
+      let add_clause c =
+        add_clause c (pr_bool_c t_proxy c)
+      in
+
       (* proxy => a<=> b,
          ¬proxy => a xor b *)
-      let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
+      add_clause [Lit.neg proxy; Lit.neg a; b];
-      add_clause [Lit.neg proxy; Lit.neg a; b] proof;
+      add_clause [Lit.neg proxy; Lit.neg b; a];
-      add_clause [Lit.neg proxy; Lit.neg b; a] proof;
+      add_clause [proxy; a; b];
-      add_clause [proxy; a; b] proof;
+      add_clause [proxy; Lit.neg a; Lit.neg b];
-      add_clause [proxy; Lit.neg a; Lit.neg b] proof;
+      proxy, pr_def_refl t_proxy for_
-      proxy
 
     (* make a literal for [t], with a proof of [|- abs(t) = abs(lit)] *)
-    and get_lit_uncached t : Lit.t * SI.P.t =
+    and get_lit_uncached si t : Lit.t * SI.P.t =
       let sub_p = ref [] in
 
       let get_lit t =
@@ -250,43 +266,56 @@ module Make(A : ARG) : S with module A = A = struct
         lit
       in
 
+      let add_clause_by_def_ proxy c : unit =
+        let pr = pr_bool_c proxy c in
+        add_clause c pr
+      in
+
       match A.view_as_bool t with
       | B_bool b -> mk_lit (T.bool self.tst b), SI.P.refl t
       | B_opaque_bool t -> mk_lit t, SI.P.refl t
       | B_not u ->
         let lit, pr = get_lit_and_proof_ u in
         Lit.neg lit, pr
+
       | B_and l ->
         let subs = l |> Iter.map get_lit |> Iter.to_list in
-        let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in
+        let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"and_" self in
+        SI.define_const si ~const:t_proxy ~rhs:t;
         (* add clauses *)
-        let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
+        List.iter
-        List.iter (fun u -> add_clause [Lit.neg proxy; u] proof) subs;
+          (fun u -> add_clause_by_def_ t_proxy [Lit.neg proxy; u])
-        add_clause (proxy :: List.map Lit.neg subs) proof;
+          subs;
-        proxy, proof (* FIXME: use sub_p, by-def(proxy), A.proof_bool *)
+        add_clause_by_def_ t_proxy (proxy :: List.map Lit.neg subs);
+        proxy, pr_def_refl t_proxy t
+
       | B_or l ->
         let subs = l |> Iter.map get_lit |> Iter.to_list in
-        let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
+        let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"or_" self in
+        SI.define_const si ~const:t_proxy ~rhs:t;
         (* add clauses *)
-        let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
+        List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs;
-        List.iter (fun u -> add_clause [Lit.neg u; proxy] proof) subs;
+        add_clause_by_def_ t_proxy (Lit.neg proxy :: subs);
-        add_clause (Lit.neg proxy :: subs) proof;
+        proxy, pr_def_refl t_proxy t
-        proxy, proof (* FIXME: use sub_p, by-def(proxy), A.proof_bool *)
+
       | B_imply (args, u) ->
         (* transform into [¬args \/ u] on the fly *)
         let args = args |> Iter.map get_lit |> Iter.map Lit.neg |> Iter.to_list in
         let u = get_lit u in
         let subs = u :: args in
+
         (* now the or-encoding *)
-        let proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in
+        let t_proxy, proxy = fresh_lit ~for_:t ~mk_lit ~pre:"implies_" self in
+        SI.define_const si ~const:t_proxy ~rhs:t;
+
         (* add clauses *)
-        let proof = SI.P.sorry in (* FIXME: by_def(proxy) + bool *)
+        List.iter (fun u -> add_clause_by_def_ t_proxy [Lit.neg u; proxy]) subs;
-        List.iter (fun u -> add_clause [Lit.neg u; proxy] proof) subs;
+        add_clause_by_def_ t_proxy (Lit.neg proxy :: subs);
-        add_clause (Lit.neg proxy :: subs) proof;
+        proxy, pr_def_refl t_proxy t
-        proxy, proof (* FIXME: by_def(proxy) + sub_p + A.proof_bool *)
+
       | B_ite _ | B_eq _ | B_neq _ -> mk_lit t, SI.P.refl t
-      | B_equiv (a,b) -> equiv_ ~get_lit ~for_:t ~is_xor:false a b, SI.P.sorry (* FIXME *)
+      | B_equiv (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:false a b
-      | B_xor  (a,b) -> equiv_ ~get_lit ~for_:t ~is_xor:true a b, SI.P.sorry (* FIXME *)
+      | B_xor  (a,b) -> equiv_ si ~get_lit ~for_:t ~is_xor:true a b
       | B_atom u -> mk_lit u, SI.P.refl u
     in