wip: fix CC for theory terms

src/smt/Congruence_closure.ml

@@ -123,7 +123,8 @@ 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 (f, a) -> App_cst (f, IArray.map find a) |> CCOpt.return
+    | App_cst ({cst_view=Cst_def {do_cc=false;_}; _}, _) -> 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 *)
    end
@@ -142,8 +143,6 @@ let remove_signature cc (t:term): unit = match signature cc t with
 let add_signature cc (t:term) (r:repr): unit = match signature cc t with
   | None -> ()
   | Some s ->
-    assert (CCOpt.map_or ~default:false (Signature.equal s)
-        (signature cc r.n_term));
     (* add, but only if not present already *)
     begin match Sig_tbl.get cc.signatures_tbl s with
       | None ->
@@ -344,7 +343,9 @@ let rec update_pending (cc:t): unit =
         add_signature cc n.n_term (find cc n)
       | Some u ->
         (* must combine [t] with [r] *)
-        push_combine cc n u (Explanation.mk_congruence n u)
+        if not @@ Equiv_class.equal n u then (
+          push_combine cc n u (Explanation.mk_congruence n u)
+        )
     end;
     (* FIXME: when to actually evaluate?
     eval_pending cc;

src/smt/Solver_types.ml

@@ -74,8 +74,9 @@ and cst_view =
   | Cst_def of {
       pp : 'a. ('a Fmt.printer -> 'a IArray.t Fmt.printer) option;
       abs : self:term -> term IArray.t -> term * bool; (* remove the sign? *)
-      relevant : 'a. 'a IArray.t -> 'a Sequence.t; (* iter on relevant immediate subterms *)
-      ty : term IArray.t -> ty; (* compute type *)
+      do_cc: bool; (* participate in congruence closure? *)
+      relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
+      ty : ID.t -> term IArray.t -> ty; (* compute type *)
     }
 (** Methods on the custom term view whose arguments are ['a].
     Terms must be printable, and provide some additional theory handles.

src/smt/Term_cell.ml

@@ -78,7 +78,7 @@ let ty (t:t): Ty.t = match t with
              ))
           ty_args;
         ty_ret
-      | Cst_def def -> def.ty args
+      | Cst_def def -> def.ty f.cst_id args
     end
   | If (_,b,_) -> b.term_ty
 

src/smt/th_bool/Sidekick_th_bool.ml

@@ -25,8 +25,10 @@ let id_distinct = ID.make "distinct"
 
 module C = struct
 
-  let get_ty _ = Ty.prop
-  let relevant _ = Sequence.empty (* no congruence closure *)
+  let get_ty _ _ = Ty.prop
+
+  (* no congruence closure, except for `=` *)
+  let relevant id _ _ = ID.equal id_eq id
 
   let abs ~self _a =
     match Term.view self with
@@ -35,14 +37,14 @@ module C = struct
       IArray.get args 0, false
     | _ -> self, true
 
-  let mk_cst id : Cst.t =
-    {cst_id=id; cst_view=Cst_def { pp=None; abs; ty=get_ty; relevant; }; }
+  let mk_cst ?(do_cc=false) id : Cst.t =
+    {cst_id=id; cst_view=Cst_def { pp=None; abs; ty=get_ty; relevant; do_cc; }; }
 
   let not = mk_cst id_not
   let and_ = mk_cst id_and
   let or_ = mk_cst id_or
   let imply = mk_cst id_imply
-  let eq = mk_cst id_eq
+  let eq = mk_cst ~do_cc:true id_eq
   let distinct = mk_cst id_distinct
 end