From 09317474044b64ce50aa115b96bfa21e64984d04 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 22 Jun 2018 21:02:07 -0500 Subject: [PATCH] refactor(cc): better handling of terms that should be ignored by CC --- src/smt/Congruence_closure.ml | 13 ++++++------- src/smt/Cst.ml | 4 ++++ src/smt/Cst.mli | 1 + src/smt/Solver_types.ml | 2 +- src/smt/Theory_combine.ml | 1 + 5 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/smt/Congruence_closure.ml b/src/smt/Congruence_closure.ml index dab6b42a..d6044e50 100644 --- a/src/smt/Congruence_closure.ml +++ b/src/smt/Congruence_closure.ml @@ -76,9 +76,8 @@ let[@inline] size_ (r:repr) = Bag.size r.n_parents (* check if [t] is in the congruence closure. - Invariant: [in_cc t => in_cc u, forall u subterm t] *) -let[@inline] mem (cc:t) (t:term): bool = - Term.Tbl.mem cc.tbl t + Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) +let[@inline] mem (cc:t) (t:term): bool = Term.Tbl.mem cc.tbl t (* TODO: remove path compression, point to new root explicitely during `union` *) @@ -125,7 +124,7 @@ let signature cc (t:term): node Term.view option = let find = find_tn cc in begin match Term.view t with | App_cst (_, a) when IArray.is_empty a -> None - | App_cst ({cst_view=Cst_def {do_cc=false;_}; _}, _) -> None (* no CC *) + | App_cst (c, _) when not @@ Cst.do_cc c -> None (* no CC *) | App_cst (f, a) -> App_cst (f, IArray.map find a) |> CCOpt.return (* FIXME: relevance *) | Bool _ | If _ -> None (* no congruence for these *) @@ -452,8 +451,8 @@ and add_new_term cc (t:term) : node = in (* register sub-terms, add [t] to their parent list *) begin match t.term_view with - | Bool _-> () - | App_cst (_, a) -> IArray.iter add_sub_t a + | App_cst (c, a) when Cst.do_cc c -> IArray.iter add_sub_t a + | Bool _ | App_cst _ -> () | If (a,b,c) -> (* TODO: relevancy? only [a] needs be decided for now *) add_sub_t a; @@ -463,7 +462,7 @@ and add_new_term cc (t:term) : node = (* remove term when we backtrack *) on_backtrack cc (fun () -> - Log.debugf 20 (fun k->k "(@[cc.remove_term@ %a@])" Term.pp t); + 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; diff --git a/src/smt/Cst.ml b/src/smt/Cst.ml index ddd7fe71..d0cd406d 100644 --- a/src/smt/Cst.ml +++ b/src/smt/Cst.ml @@ -21,6 +21,10 @@ let as_undefined_exn (c:t) = match as_undefined c with let[@inline] mk_undef id ty = make id (Cst_undef ty) let[@inline] mk_undef_const id ty = mk_undef id (Ty.Fun.mk [] ty) +let[@inline] do_cc (c:t) : bool = match view c with +| Cst_undef _ -> true +| Cst_def {do_cc;_} -> do_cc + let equal a b = ID.equal a.cst_id b.cst_id let compare a b = ID.compare a.cst_id b.cst_id let hash t = ID.hash t.cst_id diff --git a/src/smt/Cst.mli b/src/smt/Cst.mli index b6d98dc8..3596e250 100644 --- a/src/smt/Cst.mli +++ b/src/smt/Cst.mli @@ -13,6 +13,7 @@ val as_undefined : t -> (t * Ty.Fun.t) option val as_undefined_exn : t -> t * Ty.Fun.t val is_undefined : t -> bool +val do_cc : t -> bool val mk_undef : ID.t -> Ty.Fun.t -> t val mk_undef_const : ID.t -> Ty.t -> t diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml index ec311bdb..0afa1614 100644 --- a/src/smt/Solver_types.ml +++ b/src/smt/Solver_types.ml @@ -149,7 +149,7 @@ let hash_lit a = let cmp_cc_node a b = term_cmp_ a.n_term b.n_term -let rec cmp_exp a b = +let cmp_exp a b = let toint = function | E_merges _ -> 0 | E_lit _ -> 1 | E_reduction -> 2 | E_lits _ -> 3 diff --git a/src/smt/Theory_combine.ml b/src/smt/Theory_combine.ml index 54b18f5d..08304b9c 100644 --- a/src/smt/Theory_combine.ml +++ b/src/smt/Theory_combine.ml @@ -53,6 +53,7 @@ let assume_lit (self:t) (lit:Lit.t) : unit = | _ -> (* transmit to theories. *) C_clos.assert_lit (cc self) lit; + C_clos.check (cc self); theories self (fun (module Th) -> Th.on_assert Th.state lit); end