From 6302d13fe8eaf9cb1a0668b81469ad4e772fb84d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 23 May 2018 22:24:35 -0500 Subject: [PATCH] wip: use Lit.Set.t for explanations --- src/smt/Congruence_closure.ml | 2 +- src/smt/Congruence_closure.mli | 3 +-- src/smt/Theory.ml | 8 ++++---- src/smt/Theory_combine.ml | 4 ---- src/smt/th_bool/Sidekick_th_bool.ml | 14 +++++++------- 5 files changed, 13 insertions(+), 18 deletions(-) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index 92f15484..550e4f52 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -28,7 +28,7 @@ type actions = { raise_conflict: 'a. Lit.Set.t -> 'a; (** Report a conflict *) - propagate: Lit.t -> Explanation.t Bag.t -> unit; + propagate: Lit.t -> Lit.t list -> unit; (** Propagate a literal *) } diff --git a/src/smt/Congruence_closure.mli b/src/smt/Congruence_closure.mli index ac41f5bb..3be07b6a 100644 --- a/src/smt/Congruence_closure.mli +++ b/src/smt/Congruence_closure.mli @@ -21,8 +21,7 @@ type actions = { raise_conflict: 'a. Lit.Set.t -> 'a; (** Report a conflict *) - (* FIXME: take a delayed Lit.Set.t? *) - propagate: Lit.t -> Explanation.t Bag.t -> unit; + propagate: Lit.t -> Lit.t list -> unit; (** Propagate a literal *) } diff --git a/src/smt/Theory.ml b/src/smt/Theory.ml index f3f75baa..7c86cdad 100644 --- a/src/smt/Theory.ml +++ b/src/smt/Theory.ml @@ -41,13 +41,13 @@ type actions = { raise_conflict: 'a. conflict -> 'a; (** Give a conflict clause to the solver *) - propagate_eq: Term.t -> Term.t -> Explanation.t -> unit; + propagate_eq: Term.t -> Term.t -> Lit.Set.t -> unit; (** Propagate an equality [t = u] because [e] *) - propagate_distinct: Term.t list -> neq:Term.t -> Explanation.t -> unit; - (** Propagate a [distinct l] because [e] (where [e = atom neq] *) + propagate_distinct: Term.t list -> neq:Term.t -> Lit.t -> unit; + (** Propagate a [distinct l] because [e] (where [e = neq] *) - propagate: Lit.t -> Explanation.t Bag.t -> unit; + propagate: Lit.t -> Lit.Set.t -> 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 e345ce19..2c6b8bb9 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -126,10 +126,6 @@ let if_sat (self:t) (slice:_) : _ Sat_solver.res = (* forward propagations from CC or theories directly to the SMT core *) let act_propagate (self:t) f guard : unit = let Sat_solver.Actions r = self.cdcl_acts in - let guard = - Congruence_closure.explain_unfold_bag (cc self) guard - |> Lit.Set.to_list - in Sat_solver.Log.debugf 2 (fun k->k "(@[@{propagate@}@ %a@ :guard %a@])" Lit.pp f (Util.pp_list Lit.pp) guard); diff --git a/src/smt/th_bool/Sidekick_th_bool.ml b/src/smt/th_bool/Sidekick_th_bool.ml index e606b0a6..2022de44 100644 --- a/src/smt/th_bool/Sidekick_th_bool.ml +++ b/src/smt/th_bool/Sidekick_th_bool.ml @@ -255,13 +255,13 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit = | B_not _ -> assert false (* normalized *) | B_eq (t,u) -> if Lit.sign lit then ( - self.acts.Theory.propagate_eq t u (Explanation.lit lit) + self.acts.Theory.propagate_eq t u (Lit.Set.singleton lit) ) else ( - self.acts.Theory.propagate_distinct [t;u] ~neq:lit_t (Explanation.lit lit) + self.acts.Theory.propagate_distinct [t;u] ~neq:lit_t lit ) | B_distinct l -> if Lit.sign lit then ( - self.acts.Theory.propagate_distinct l ~neq:lit_t (Explanation.lit lit) + self.acts.Theory.propagate_distinct l ~neq:lit_t lit ) else ( (* TODO: propagate pairwise equalities? *) Error.errorf "cannot process negative distinct lit %a" Lit.pp lit; @@ -269,7 +269,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit = | B_and subs -> if Lit.sign lit then ( (* propagate [lit => subs_i] *) - let expl = Bag.return (Explanation.lit lit) in + let expl = Lit.Set.singleton lit in List.iter (fun sub -> let sublit = Lit.atom sub in @@ -277,7 +277,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit = subs ) else ( (* propagate [¬lit => ∨_i ¬ subs_i] *) - let c = lit :: List.map (Lit.atom ~sign:false) subs in + let c = Lit.neg lit :: List.map (Lit.atom ~sign:false) subs in self.acts.Theory.add_local_axiom (IArray.of_list c) ) | B_or subs -> @@ -287,7 +287,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit = self.acts.Theory.add_local_axiom (IArray.of_list c) ) else ( (* propagate [¬lit => ¬subs_i] *) - let expl = Bag.return (Explanation.lit lit) in + let expl = Lit.Set.singleton lit in List.iter (fun sub -> let sublit = Lit.atom ~sign:false sub in @@ -300,7 +300,7 @@ let tseitin (self:t) (lit:Lit.t) (lit_t:term) (b:term builtin) : unit = let c = Lit.atom concl :: Lit.neg lit :: List.map (Lit.atom ~sign:false) guard in self.acts.Theory.add_local_axiom (IArray.of_list c) ) else ( - let expl = Bag.return (Explanation.lit lit) in + let expl = Lit.Set.singleton lit in (* propagate [¬lit => ¬concl] *) self.acts.Theory.propagate (Lit.atom ~sign:false concl) expl; (* propagate [¬lit => ∧_i guard_i] *)