refactor: introduce check_invariants in CC

costly, but helps find bugs

src/sat/Internal.ml

@@ -1426,7 +1426,7 @@ module Make (Th : Theory_intf.S) = struct
   (* remove some learnt clauses
      NOTE: so far we do not forget learnt clauses. We could, as long as
      lemmas from the theory itself are kept. *)
-  let reduce_db () = ()
+  let reduce_db (_:t) = ()
 
   (* Decide on a new literal, and enqueue it into the trail *)
   let rec pick_branch_aux st atom : unit =
@@ -1450,11 +1450,18 @@ module Make (Th : Theory_intf.S) = struct
         | exception Not_found -> raise Sat
       end
 
+  let[@inline] check_invariants (st:t) =
+    if Util._CHECK_INVARIANTS then (
+      Th.check_invariants @@ theory st;
+      (* TODO: also check internal invariants? *)
+    )
+
   (* do some amount of search, until the number of conflicts or clause learnt
      reaches the given parameters *)
   let search (st:t) n_of_conflicts n_of_learnts : unit =
     let conflictC = ref 0 in
     while true do
+      check_invariants st;
       match propagate st with
       | Some confl -> (* Conflict *)
         incr conflictC;
@@ -1472,8 +1479,9 @@ module Make (Th : Theory_intf.S) = struct
         (* if decision_level() = 0 then simplify (); *)
 
         if n_of_learnts >= 0 &&
-           Vec.size st.clauses - Vec.size st.trail >= n_of_learnts
+           Vec.size st.clauses - Vec.size st.trail >= n_of_learnts then (
-        then reduce_db();
+          reduce_db st;
+        );
 
         pick_branch_lit st
     done

src/sat/Theory_intf.ml

@@ -130,5 +130,9 @@ module type S = sig
   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. *)
+
+  (**/**)
+  val check_invariants : t -> unit
+  (**/**)
 end
 

src/smt/Congruence_closure.ml

@@ -373,6 +373,7 @@ and task_merge_ cc a b e_ab : unit =
         (fun parent -> push_pending cc parent)
     end;
     (* perform [union ra rb] *)
+    Log.debugf 15 (fun k->k "(@[cc.merge@ :from %a@ :into %a@])" Equiv_class.pp r_from Equiv_class.pp r_into);
     begin
       let r_into_old_parents = r_into.n_parents in
       let r_into_old_tags = r_into.n_tags in
@@ -606,3 +607,49 @@ let mk_model (cc:t) (m:Model.t) : Model.t =
       funs
   in
   Model.add_funs funs m
+
+let pp_full out (cc:t) : unit =
+  let pp_n out n =
+    let pp_next out n =
+      if n==n.n_root then () else Fmt.fprintf out "@ :next %a" Equiv_class.pp n.n_root in
+    let pp_root out n =
+      let u = find cc n in if n==u||n.n_root==u then () else Fmt.fprintf out "@ :root %a" Equiv_class.pp u in
+    Fmt.fprintf out "(@[%a%a%a@])" Term.pp n.n_term pp_next n pp_root n
+  and pp_sig_e out (s,n) =
+    Fmt.fprintf out "(@[<1>%a@ -> %a@])" Signature.pp s Equiv_class.pp n
+  in
+  Fmt.fprintf out
+    "(@[cc.state@ (@[<hv>:nodes@ %a@])@ (@[<hv>:sig@ %a@])@])"
+    (Util.pp_seq ~sep:" " pp_n) (Term.Tbl.values cc.tbl)
+    (Util.pp_seq ~sep:" " pp_sig_e) (Sig_tbl.to_seq cc.signatures_tbl)
+
+let check_invariants_ (cc:t) =
+  Log.debug 5 "(cc.check-invariants)";
+  Log.debugf 15 (fun k-> k "%a" pp_full cc);
+  assert (Term.equal (Term.true_ cc.tst) cc.true_.n_term);
+  assert (Term.equal (Term.false_ cc.tst) cc.false_.n_term);
+  assert (Vec.is_empty cc.tasks);
+  (* check that subterms are internalized *)
+  Term.Tbl.iter
+    (fun t n ->
+       assert (Term.equal t n.n_term);
+       assert (not @@ Equiv_class.get_field Equiv_class.field_is_pending n);
+       relevant_subterms t
+         (fun u -> assert (Term.Tbl.mem cc.tbl u));
+       (* check proper signature *)
+       begin match signature cc t with
+         | None -> ()
+         | Some s ->
+           Log.debugf 15 (fun k->k "(@[cc.check-sig@ %a@ :sig %a@])" Term.pp t Signature.pp s);
+           (* add, but only if not present already *)
+           begin match Sig_tbl.find cc.signatures_tbl s with
+             | exception Not_found -> assert false
+             | repr_s -> assert (same_class cc n repr_s)
+           end
+       end;
+    )
+    cc.tbl;
+  ()
+
+let[@inline] check_invariants (cc:t) : unit =
+  if Util._CHECK_INVARIANTS then check_invariants_ cc

src/smt/Congruence_closure.mli

@@ -68,3 +68,6 @@ val mk_model : t -> Model.t -> Model.t
 (** Enrich a model by mapping terms to their representative's value,
     if any. Otherwise map the representative to a fresh value *)
 
+(**/**)
+val check_invariants : t -> unit
+(**/**)

src/smt/Theory.ml

@@ -86,6 +86,7 @@ let make ~name ~make () : t = {name;make}
 
 let make_st
   (type st)
+    ?(check_invariants=fun _ -> ())
     ?(on_merge=fun _ _ _ _ -> ())
     ?(on_assert=fun _ _ -> ())
     ?(mk_model=fun _ _ -> Model.empty)
@@ -99,5 +100,6 @@ let make_st
     let on_assert = on_assert
     let final_check = final_check
     let mk_model = mk_model
+    let check_invariants = check_invariants
   end in
   (module A : STATE)

src/smt/Theory_combine.ml

@@ -193,6 +193,11 @@ let act_add_persistent_axiom self c : unit =
   let (module A) = self.cdcl_acts in
   A.push_persistent c Proof.default
 
+let check_invariants (self:t) =
+  if Util._CHECK_INVARIANTS then (
+    Congruence_closure.check_invariants (cc self);
+  )
+
 let mk_theory_actions (self:t) : Theory.actions =
   let (module A) = self.cdcl_acts in
   let module R = struct

src/util/Util.ml

@@ -37,3 +37,6 @@ let setup_gc () =
 module Int_set = CCSet.Make(CCInt)
 module Int_map = CCMap.Make(CCInt)
 module Int_tbl = CCHashtbl.Make(CCInt)
+
+(* NOTE: if true, can have a big impact on performance *)
+let _CHECK_INVARIANTS = true

src/util/Util.mli

@@ -23,3 +23,8 @@ val setup_gc : unit -> unit
 module Int_set : CCSet.S with type elt = int
 module Int_map : CCMap.S with type key = int
 module Int_tbl : CCHashtbl.S with type key = int
+
+(* compile time config for internal checking of invariants *)
+val _CHECK_INVARIANTS : bool
+
+