refactor: use new msat lazy propagation

src/cc/Congruence_closure.ml

@@ -781,8 +781,10 @@ module Make(A: ARG) = struct
            let lit = if sign then lit else A.Lit.neg lit in (* apply sign *)
            Log.debugf 5 (fun k->k "(@[cc.bool_propagate@ %a@])" A.Lit.pp lit);
            (* complete explanation with the [u1=t1] chunk *)
-           let expl = explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1 in
-           let reason = Msat.Consequence (expl, A.Proof.default) in
+           let expl () =
+             let e = explain_eq_n ~init:(Lazy.force half_expl) cc u1 t1 in
+             e, A.Proof.default in
+           let reason = Msat.Consequence expl in
            acts.Msat.acts_propagate lit reason
          | _ -> ())
 

src/smt/Theory.ml

@@ -27,12 +27,17 @@ module type ACTIONS = sig
   (** Give a conflict clause to the solver *)
 
   val propagate_eq: Term.t -> Term.t -> Lit.t list -> unit
-  (** Propagate an equality [t = u] because [e] *)
+  (** Propagate an equality [t = u] because [e].
+      TODO: use [CC.Expl] instead, with lit/merge constructors *)
 
   val propagate_distinct: Term.t list -> neq:Term.t -> Lit.t -> unit
   (** Propagate a [distinct l] because [e] (where [e = neq] *)
 
-  val propagate: Lit.t -> Lit.t list -> unit
+  val propagate: Lit.t -> (unit -> Lit.t list) -> unit
+  (** Propagate a boolean using a unit clause.
+      [expl => lit] must be a theory lemma, that is, a T-tautology *)
+
+  val propagate_l: Lit.t -> Lit.t list -> unit
   (** Propagate a boolean using a unit clause.
       [expl => lit] must be a theory lemma, that is, a T-tautology *)
 

src/smt/Theory_combine.ml

@@ -56,7 +56,9 @@ let assert_lits_ ~final (self:t) acts (lits:Lit.t Sequence.t) : unit =
     let[@inline] raise_conflict c : 'a = acts.Msat.acts_raise_conflict c Proof_default
     let[@inline] propagate_eq t u expl : unit = CC.assert_eq cc t u expl
     let propagate_distinct ts ~neq expl = CC.assert_distinct cc ts ~neq expl
-    let[@inline] propagate p cs : unit = acts.Msat.acts_propagate p (Msat.Consequence (cs, Proof_default))
+    let[@inline] propagate p cs : unit =
+      acts.Msat.acts_propagate p (Msat.Consequence (fun () -> cs(), Proof_default))
+    let[@inline] propagate_l p cs : unit = propagate p (fun()->cs)
     let[@inline] add_local_axiom lits : unit =
       acts.Msat.acts_add_clause ~keep:false lits Proof_default
     let[@inline] add_persistent_axiom lits : unit =

src/th-bool/Th_dyn_tseitin.ml

@@ -61,7 +61,7 @@ module Make(Term : ARG) = struct
         IArray.iter
           (fun sub ->
              let sublit = Lit.atom self.tst sub in
-             A.propagate sublit [lit])
+             A.propagate_l sublit [lit])
           subs
       ) else if final && not @@ expanded () then (
         (* axiom [¬lit => ∨_i ¬ subs_i] *)
@@ -91,12 +91,12 @@ module Make(Term : ARG) = struct
         add_axiom c
       ) else if not @@ Lit.sign lit then (
         (* propagate [¬lit => ¬concl] *)
-        A.propagate (Lit.atom self.tst ~sign:false concl) [lit];
+        A.propagate_l (Lit.atom self.tst ~sign:false concl) [lit];
         (* propagate [¬lit => ∧_i guard_i] *)
         IArray.iter
           (fun sub ->
              let sublit = Lit.atom self.tst ~sign:true sub in
-             A.propagate sublit [lit])
+             A.propagate_l sublit [lit])
           guard
       )