refactor(cc): better handling of terms that should be ignored by CC

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;

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

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
 

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

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