refactor: remove proof production entirely

Author: c-cube

src/backend/Dot.ml

@@ -8,10 +8,7 @@ type t = actions
 let[@inline] push_clause acts c = acts.act_push_clause c
 let[@inline] level acts = acts.act_level ()
 let[@inline] propagate_bool_eval acts t b ~subs = acts.act_propagate_bool_eval t b ~subs
-let[@inline] propagate_bool_lemma acts t b c l = acts.act_propagate_bool_lemma t b c l
-let[@inline] raise_conflict acts atoms lemma = acts.act_raise_conflict atoms lemma
+let[@inline] propagate_bool_lemma acts t b c = acts.act_propagate_bool_lemma t b c
+let[@inline] raise_conflict acts atoms = acts.act_raise_conflict atoms
 let[@inline] on_backtrack acts f = acts.act_on_backtrack f
 
-let[@inline] propagate_bool_lemma acts t b c l =
-  acts.act_propagate_bool_lemma t b c l
-

src/backend/Dot.mli

@@ -24,15 +24,15 @@ val propagate_bool_eval : t -> term -> bool -> subs:term list -> unit
     relevant (sub)terms [l]
     @param subs subterms used for the propagation *)
 
-val propagate_bool_lemma : t -> term -> bool -> atom list -> lemma -> unit
+val propagate_bool_lemma : t -> term -> bool -> atom list -> unit
 (** [propagate_bool_lemma t b c] propagates the boolean literal [t]
       assigned to boolean value [b], explained by a valid theory
       lemma [c].
       Precondition: [c] is a tautology such that [c == (c' ∨ t=b)], where [c']
       is composed of atoms false in current model.
 *)
 
-val raise_conflict : t -> atom list -> lemma -> 'a
+val raise_conflict : t -> atom list -> 'a
 (** Raise a conflict with the given clause, which must be false
     in the current trail, and with a lemma to explain *)
 

src/backend/backend_intf.ml

@@ -14,15 +14,6 @@ let[@inline] is_builtin (t:term) = match Term.view t with
   | True | False -> true
   | _ -> false
 
-let tcl =
-  let tcl_pp out = function
-    | L_tautology -> Fmt.string out "true_is_true"
-    | _ -> assert false
-  in
-  {tcl_pp}
-
-let lemma_trivial : lemma = Lemma.make L_tautology tcl
-
 let build p_id Plugin.S_nil : Plugin.t =
   let module P = struct
     let id = p_id
@@ -36,10 +27,10 @@ let build p_id Plugin.S_nil : Plugin.t =
     (* on initialization, add clause [true] *)
     let init acts t = match Term.view t with
       | True ->
-        let c_true = Clause.make [Term.Bool.pa t] (Lemma lemma_trivial) in
+        let c_true = Clause.make [Term.Bool.pa t] ~lemma:false in
         Actions.push_clause acts c_true
       | False ->
-        let c = Clause.make [Term.Bool.na t] (Lemma lemma_trivial) in
+        let c = Clause.make [Term.Bool.na t] ~lemma:false in
         Actions.push_clause acts c
       | _ -> assert false