feat(const): add opaque_to_cc property, to control CC

examples/sudoku/sudoku_solve.ml

@@ -165,6 +165,8 @@ end = struct
         | Cell_is a, Cell_is b ->
           a.x = b.x && a.y = b.y && Cell.equal a.value b.value
         | _ -> false
+
+      let opaque_to_cc _ = false
     end : Const.DYN_OPS)
 
   module Sat = Sidekick_sat

src/base/Data_ty.ml

@@ -103,6 +103,8 @@ let ops =
       | Select s -> Hash.combine2 594 (Select.hash s)
       | Is_a c -> Hash.combine2 595 (Cstor.hash c)
       | _ -> assert false
+
+    let opaque_to_cc _ = false
   end : Const.DYN_OPS)
 
 let data tst d : Term.t =

src/base/Form.ml

@@ -36,6 +36,8 @@ let ops : Const.ops =
       | C_or -> Hash.int 426
       | C_imply -> Hash.int 427
       | _ -> assert false
+
+    let opaque_to_cc _ = true
   end)
 
 (* ### view *)

src/base/LRA_term.ml

@@ -113,6 +113,8 @@ let ops : Const.ops =
       | Op o -> Op.hash o
       | Mult_by q -> Hash.(combine2 135 (Sidekick_zarith.Rational.hash q))
       | _ -> assert false
+
+    let opaque_to_cc _ = true
   end)
 
 let real tst = Ty.real tst

src/base/Ty.ml

@@ -34,6 +34,8 @@ let ops_ty : Const.ops =
         | Ty_int -> Hash.int 3
         | Ty_uninterpreted u -> Hash.combine2 10 (ID.hash u.id))
       | _ -> assert false
+
+    let opaque_to_cc _ = true
   end)
 
 open struct

src/base/Uconst.ml

@@ -26,6 +26,8 @@ let ops =
     let hash = function
       | Uconst c -> Hash.combine2 522660 (hash c)
       | _ -> assert false
+
+    let opaque_to_cc _ = false
   end : Const.DYN_OPS)
 
 let[@inline] make uc_id uc_ty : t = { uc_id; uc_ty }

src/core-logic/const.ml

@@ -6,6 +6,7 @@ module type DYN_OPS = sig
   val pp : view Fmt.printer
   val equal : view -> view -> bool
   val hash : view -> int
+  val opaque_to_cc : view -> bool
 end
 
 type ops = (module DYN_OPS)

src/core-logic/const.mli

@@ -10,6 +10,7 @@ module type DYN_OPS = sig
   val pp : view Fmt.printer
   val equal : view -> view -> bool
   val hash : view -> int
+  val opaque_to_cc : view -> bool
 end
 
 type ops = (module DYN_OPS)

src/core-logic/str_const.ml

@@ -16,6 +16,8 @@ let ops : Const.ops =
     let hash = function
       | Str s -> CCHash.string s
       | _ -> assert false
+
+    let opaque_to_cc _ = false
   end)
 
 let make name ~ty : Const.t = Const.make (Str name) ops ~ty

src/core-logic/t_builtins.ml

@@ -33,6 +33,8 @@ let ops : const_ops =
       | C_true -> Fmt.string out "true"
       | C_false -> Fmt.string out "false"
       | _ -> assert false
+
+    let opaque_to_cc _ = false
   end)
 
 let bool store = const store @@ Const.make C_bool ops ~ty:(type_ store)

src/core-logic/types_.ml

@@ -4,8 +4,15 @@ type const_view = ..
 
 module type DYN_CONST_OPS = sig
   val pp : const_view Fmt.printer
+  (** Pretty-print constant *)
   val equal : const_view -> const_view -> bool
+  (** Equality of constant with any other constant *)
   val hash : const_view -> int
+  (** Hash constant *)
+  val opaque_to_cc : const_view -> bool
+  (** If true, congruence closure will not apply for applications of this
+      constant. In other words, [c t1…tn] will appear to the congruence
+      closure as a single opaque term with no subterms. *)
 end
 
 type const_ops = (module DYN_CONST_OPS)

src/core/default_cc_view.ml

@@ -9,9 +9,14 @@ let view_as_cc (t : Term.t) : _ CC_view.t =
   | Term.E_const { Const.c_view = T_builtins.C_ite; _ }, [ _ty; a; b; c ] ->
     View.If (a, b, c)
   | Term.E_const { Const.c_view = T_builtins.C_not; _ }, [ a ] -> View.Not a
+  | Term.E_const { Const.c_ops = (module OP); c_view; _ }, _
+    when OP.opaque_to_cc c_view ->
+    (* this constant hides its arguments *)
+    View.Opaque t
   | _ ->
     (match Term.view t with
     | Term.E_app (f, a) -> View.App_ho (f, a)
     | Term.E_const { Const.c_view = T_builtins.C_true; _ } -> View.Bool true
     | Term.E_const { Const.c_view = T_builtins.C_false; _ } -> View.Bool false
+    | Term.E_app_fold _ -> View.Opaque t
     | _ -> View.Opaque t)

src/core/gensym.ml

@@ -9,6 +9,7 @@ type Const.view +=
       gensym_id: int;  (** Id of the gensym *)
       pre: string;  (** Printing prefix *)
       ty: ty;
+      opaque_to_cc: bool;
     }
 
 let ops =
@@ -26,6 +27,10 @@ let ops =
     let pp out = function
       | Fresh { id; pre; _ } -> Fmt.fprintf out "$%s[%d]" pre id
       | _ -> assert false
+
+    let opaque_to_cc = function
+      | Fresh f -> f.opaque_to_cc
+      | _ -> assert false
   end : Const.DYN_OPS)
 
 type t = { tst: Term.store; self_id: int; mutable fresh: int }
@@ -38,11 +43,13 @@ let create tst : t =
   incr id_;
   { tst; self_id; fresh = 0 }
 
-let fresh_term (self : t) ~pre (ty : ty) : Term.t =
+let fresh_term ?(opaque_to_cc = false) (self : t) ~pre (ty : ty) : Term.t =
   let id = self.fresh in
   self.fresh <- 1 + self.fresh;
   let c =
     Term.const self.tst
-    @@ Const.make (Fresh { id; gensym_id = self.self_id; pre; ty }) ops ~ty
+    @@ Const.make
+         (Fresh { id; gensym_id = self.self_id; pre; ty; opaque_to_cc })
+         ops ~ty
   in
   c

src/core/gensym.mli

@@ -15,5 +15,5 @@ type t
 val create : Term.store -> t
 (** New (stateful) generator instance. *)
 
-val fresh_term : t -> pre:string -> ty -> term
+val fresh_term : ?opaque_to_cc:bool -> t -> pre:string -> ty -> term
 (** Make a fresh term of the given type *)

src/main/pure_sat_solver.ml

@@ -177,6 +177,9 @@ end = struct
       let pp out = function
         | I i -> Fmt.int out i
         | _ -> assert false
+
+      (* irrelevant *)
+      let opaque_to_cc _ = true
     end : Const.DYN_OPS)
 
   let make tst i : Lit.t =