From de1cc952a5f4ad81a096d06e8d6ee62b22da8ba2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 16 Feb 2019 19:09:43 -0600 Subject: [PATCH] refactor: use new msat lazy propagation --- src/cc/Congruence_closure.ml | 6 ++++-- src/smt/Theory.ml | 9 +++++++-- src/smt/Theory_combine.ml | 4 +++- src/th-bool/Th_dyn_tseitin.ml | 6 +++--- 4 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/cc/Congruence_closure.ml b/src/cc/Congruence_closure.ml index ffadcdb6..2021f68b 100644 --- a/src/cc/Congruence_closure.ml +++ b/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 | _ -> ()) diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index d877d4d9..71893f93 100644 --- a/src/smt/Theory.ml +++ b/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 *) diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index 890f8b4e..991dfa46 100644 --- a/src/smt/Theory_combine.ml +++ b/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 = diff --git a/src/th-bool/Th_dyn_tseitin.ml b/src/th-bool/Th_dyn_tseitin.ml index 7d013ba0..504a19f8 100644 --- a/src/th-bool/Th_dyn_tseitin.ml +++ b/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 )