From 9b8c21513af077e1f61d88c0dcfa764504483c6f Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 25 May 2018 21:32:24 -0500 Subject: [PATCH] refactor: internalize terms earlier --- src/sat/Theory_intf.ml | 3 ++ src/smt/Congruence_closure.ml | 62 ++++++++++------------------------- src/smt/Theory_combine.ml | 56 ++++++++++++++++--------------- 3 files changed, 51 insertions(+), 70 deletions(-) diff --git a/src/sat/Theory_intf.ml b/src/sat/Theory_intf.ml index 814de2d2..23780c69 100644 --- a/src/sat/Theory_intf.ml +++ b/src/sat/Theory_intf.ml @@ -124,6 +124,9 @@ module type S = sig (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, and returns the result of the new assumptions. *) + val add_formula : t -> formula -> unit + (** Internalize formula for later use *) + val if_sat : t -> formula slice_actions -> (formula, proof) res (** Called at the end of the search in case a model has been found. If no new clause is pushed, then 'sat' is returned, else search is resumed. *) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index 0d7ef5b5..53f2b147 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -154,8 +154,7 @@ let add_signature cc (t:term) (r:repr): unit = match signature cc t with (* add, but only if not present already *) begin match Sig_tbl.get cc.signatures_tbl s with | None -> - on_backtrack cc - (fun () -> Sig_tbl.remove cc.signatures_tbl s); + on_backtrack cc (fun () -> Sig_tbl.remove cc.signatures_tbl s); Sig_tbl.add cc.signatures_tbl s r; | Some r' -> assert (Equiv_class.equal r r'); @@ -381,18 +380,8 @@ and update_combine cc = assert (is_root_ ra); assert (is_root_ rb); (* We will merge [r_from] into [r_into]. - we try to ensure that [size ra <= size rb] in general, unless - it clashes with the invariant that the representative must - be a normal form if the class contains a normal form *) - let must_solve, r_from, r_into = - match Term.is_semantic ra.n_term, Term.is_semantic rb.n_term with - | true, true -> - if size_ ra > size_ rb then true, rb, ra else true, ra, rb - | false, false -> - if size_ ra > size_ rb then false, rb, ra else false, ra, rb - | true, false -> false, rb, ra (* semantic ==> representative *) - | false, true -> false, ra, rb - in + we try to ensure that [size ra <= size rb] in general *) + let r_from, r_into = if size_ ra > size_ rb then rb, ra else ra, rb in let new_tags = Util.Int_map.union (fun _i (n1,e1) (n2,e2) -> @@ -411,28 +400,6 @@ and update_combine cc = raise_conflict cc @@ Lit.Set.elements lits) ra.n_tags rb.n_tags in - (* solve the equation, if both [ra] and [rb] are semantic. - The equation is between signatures, so as to canonize w.r.t the - current congruence before solving *) - if must_solve then ( - let t_a = ra.n_term and t_b = rb.n_term in - match signature cc t_a, signature cc t_b with - | Some (Custom t1), Some (Custom t2) -> - begin match t1.tc.tc_t_solve t1.view t2.view with - | Solve_ok {subst=l} -> - Log.debugf 5 - (fun k->k "(@[solve@ (@[= %a %a@])@ :yields (@[%a@])@])" - Term.pp t_a Term.pp t_b - (Util.pp_list @@ Util.pp_pair Equiv_class.pp Term.pp) l); - List.iter (fun (u1,u2) -> push_combine cc u1 (add cc u2) e_ab) l - | Solve_fail {expl} -> - Log.debugf 5 - (fun k->k "(@[solve-fail@ (@[= %a %a@])@ :expl %a@])" - Term.pp t_a Term.pp t_b (CCFormat.Dump.list Lit.pp) expl); - raise_conflict cc expl - end - | _ -> assert false - ); (* remove [ra.parents] from signature, put them into [st.pending] *) begin Bag.to_seq (r_from:>node).n_parents @@ -487,6 +454,7 @@ and notify_merge cc (ra:repr) ~into:(rb:repr) (e:explanation): unit = (* add [t] to [cc] when not present already *) and add_new_term cc (t:term) : node = assert (not @@ mem cc t); + Log.debugf 20 (fun k->k "(@[cc.add_term@ %a@])" Term.pp t); let n = Equiv_class.make t in (* how to add a subterm *) let add_to_parents_of_sub_node (sub:node) : unit = @@ -515,32 +483,36 @@ and add_new_term cc (t:term) : node = tc.tc_t_relevant view add_sub_t end; (* remove term when we backtrack *) - on_backtrack cc (fun () -> Term.Tbl.remove cc.tbl t); + on_backtrack cc + (fun () -> + Log.debugf 20 (fun k->k "(@[cc.remove_term@ %a@])" Term.pp t); + Term.Tbl.remove cc.tbl t); (* add term to the table *) Term.Tbl.add cc.tbl t n; (* [n] might be merged with other equiv classes *) push_pending cc n; n -(* TODO? *) -(* add [t=u] to the congruence closure, unconditionally (reduction relation) *) -and[@inline] add_eqn (cc:t) (eqn:merge_op): unit = - let t, u, expl = eqn in - push_combine cc t u expl - (* add a term *) -and[@inline] add cc t = +and[@inline] add cc t : node = try Term.Tbl.find cc.tbl t with Not_found -> add_new_term cc t let[@inline] add_seq cc seq = seq (fun t -> ignore @@ add cc t) +(* before we push tasks into [pending], ensure they are removed when we backtrack *) +let reset_on_backtrack cc : unit = + if Vec.is_empty cc.pending then ( + on_backtrack cc (fun () -> Vec.clear cc.pending); + ) + (* assert that this boolean literal holds *) let assert_lit cc lit : unit = match Lit.view lit with | Lit_fresh _ | Lit_expanded _ -> () | Lit_atom t -> assert (Ty.is_prop t.term_ty); + Log.debugf 5 (fun k->k "(@[cc.assert_lit@ %a@])" Lit.pp lit); let sign = Lit.sign lit in (* equate t and true/false *) let rhs = if sign then true_ cc else false_ cc in @@ -549,6 +521,7 @@ let assert_lit cc lit : unit = match Lit.view lit with basically, just have [n] point to true/false and thus acquire the corresponding value, so its superterms (like [ite]) can evaluate properly *) + reset_on_backtrack cc; push_combine cc n rhs (E_lit lit); () @@ -556,6 +529,7 @@ let assert_eq cc (t:term) (u:term) expl : unit = let n1 = add cc t in let n2 = add cc u in if not (same_class cc n1 n2) then ( + reset_on_backtrack cc; union cc n1 n2 expl ) diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index 872b2605..14c2b163 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -4,6 +4,7 @@ (** Combine the congruence closure with a number of plugins *) module Sat_solver = Sidekick_sat +module C_clos = Congruence_closure open Solver_types module Proof = struct @@ -25,7 +26,7 @@ type t = { (** actions provided by the SAT solver *) tst: Term.state; (** state for managing terms *) - cc: Congruence_closure.t lazy_t; + cc: C_clos.t lazy_t; (** congruence closure *) mutable theories : Theory.state list; (** Set of theories *) @@ -43,7 +44,7 @@ let[@inline] theories (self:t) : Theory.state Sequence.t = (* handle a literal assumed by the SAT solver *) let assume_lit (self:t) (lit:Lit.t) : unit = Sat_solver.Log.debugf 2 - (fun k->k "(@[<1>@{theory_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit); + (fun k->k "(@[<1>@{th_combine.assume_lit@}@ @[%a@]@])" Lit.pp lit); (* check consistency first *) begin match Lit.view lit with | Lit_fresh _ -> () @@ -52,7 +53,7 @@ let assume_lit (self:t) (lit:Lit.t) : unit = | Lit_atom {term_cell=Bool false; _} -> () | Lit_atom _ -> (* transmit to theories. *) - Congruence_closure.assert_lit (cc self) lit; + C_clos.assert_lit (cc self) lit; theories self (fun (module Th) -> Th.on_assert Th.state lit); end @@ -64,14 +65,15 @@ let cdcl_return_res (self:t) : _ Sat_solver.res = | Some lit_set -> let conflict_clause = IArray.of_list_map Lit.neg lit_set in Sat_solver.Log.debugf 3 - (fun k->k "(@[<1>conflict@ clause: %a@])" + (fun k->k "(@[<1>@{th_combine.conflict@}@ :clause %a@])" Theory.Clause.pp conflict_clause); self.conflict <- None; Sat_solver.Unsat (IArray.to_list conflict_clause, Proof.default) end let[@inline] check (self:t) : unit = - Congruence_closure.check (cc self) + Log.debug 5 "(th_combine.check)"; + C_clos.check (cc self) let with_conflict_catch self f = begin @@ -95,27 +97,29 @@ let assume_real (self:t) (slice:Lit.t Sat_solver.slice_actions) = check self ) +let add_formula (self:t) (lit:Lit.t) = + match Lit.view lit with + | Lit_atom t -> + let lazy cc = self.cc in + ignore (C_clos.add cc t : cc_node) + | Lit_expanded _ | Lit_fresh _ -> () + (* propagation from the bool solver *) let assume (self:t) (slice:_ Sat_solver.slice_actions) = match self.conflict with + | Some _ -> cdcl_return_res self (* already in conflict! *) | None -> assume_real self slice - | Some _ -> - (* already in conflict! *) - cdcl_return_res self (* perform final check of the model *) let if_sat (self:t) (slice:Lit.t Sat_solver.slice_actions) : _ Sat_solver.res = - Congruence_closure.final_check (cc self); (* all formulas in the SAT solver's trail *) - let forms = - let (module SA) = slice in - SA.slice_iter - in - (* final check for each theory *) + let (module SA) = slice in with_conflict_catch self (fun () -> + (* final check for CC + each theory *) + C_clos.final_check (cc self); theories self - (fun (module Th) -> Th.final_check Th.state forms)) + (fun (module Th) -> Th.final_check Th.state SA.slice_iter)) (** {2 Various helpers} *) @@ -123,7 +127,7 @@ let if_sat (self:t) (slice:Lit.t Sat_solver.slice_actions) : _ Sat_solver.res = let act_propagate (self:t) f guard : unit = let (module A) = self.cdcl_acts in Sat_solver.Log.debugf 2 - (fun k->k "(@[@{propagate@}@ %a@ :guard %a@])" + (fun k->k "(@[@{th.propagate@}@ %a@ :guard %a@])" Lit.pp f (Util.pp_list Lit.pp) guard); A.propagate f guard Proof.default @@ -136,7 +140,7 @@ let on_merge_from_cc (self:t) r1 r2 e : unit = theories self (fun (module Th) -> Th.on_merge Th.state r1 r2 e) -let mk_cc_actions (self:t) : Congruence_closure.actions = +let mk_cc_actions (self:t) : C_clos.actions = let (module A) = self.cdcl_acts in let module R = struct let on_backtrack = A.on_backtrack @@ -150,34 +154,34 @@ let mk_cc_actions (self:t) : Congruence_closure.actions = (* create a new theory combination *) let create (cdcl_acts:_ Sat_solver.actions) : t = - Sat_solver.Log.debug 5 "theory_combine.create"; + Sat_solver.Log.debug 5 "th_combine.create"; let rec self = { cdcl_acts; tst=Term.create ~size:1024 (); cc = lazy ( (* lazily tie the knot *) let actions = mk_cc_actions self in - Congruence_closure.create ~size:1024 ~actions self.tst; + C_clos.create ~size:1024 ~actions self.tst; ); theories = []; conflict = None; } in - ignore (Lazy.force @@ self.cc : Congruence_closure.t); + ignore (Lazy.force @@ self.cc : C_clos.t); self (** {2 Interface to individual theories} *) -let act_all_classes self = Congruence_closure.all_classes (cc self) +let act_all_classes self = C_clos.all_classes (cc self) let act_propagate_eq self t u guard = - Congruence_closure.assert_eq (cc self) t u guard + C_clos.assert_eq (cc self) t u guard let act_propagate_distinct self l ~neq guard = - Congruence_closure.assert_distinct (cc self) l ~neq guard + C_clos.assert_distinct (cc self) l ~neq guard let act_find self t = - Congruence_closure.add (cc self) t - |> Congruence_closure.find (cc self) + C_clos.add (cc self) t + |> C_clos.find (cc self) let act_add_local_axiom self c : unit = Sat_solver.Log.debugf 5 (fun k->k "(@[<2>th_combine.push_local_lemma@ %a@])" Theory.Clause.pp c); @@ -208,7 +212,7 @@ let mk_theory_actions (self:t) : Theory.actions = let add_theory (self:t) (th:Theory.t) : unit = Sat_solver.Log.debugf 2 - (fun k->k "(@[theory_combine.add_th@ :name %S@])" th.Theory.name); + (fun k->k "(@[th_combine.add_th@ :name %S@])" th.Theory.name); let th_s = th.Theory.make self.tst (mk_theory_actions self) in self.theories <- th_s :: self.theories