refactor(term): notion of is_value, which are kept as representatives

src/smt/Solver_types.ml

@@ -72,6 +72,7 @@ and cst_view =
       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 *)
+      is_value: bool; (* value constructor *)
       eval: value IArray.t -> value; (* evaluate term *)
     }
 (** Methods on the custom term view whose arguments are ['a].

src/smt/Term.ml

@@ -60,6 +60,7 @@ let create ?(size=1024) () : state =
   st
 
 let[@inline] all_terms st = Term_cell.Tbl.values st.tbl
+let[@inline] is_value t = Term_cell.is_value t.term_view
 
 let app_cst st f a =
   let cell = Term_cell.app_cst f a in

src/smt/Term.mli

@@ -40,6 +40,9 @@ val all_terms : state -> t Sequence.t
 
 val pp : t Fmt.printer
 
+val is_value : t -> bool
+(** Values are special terms that behave specially wrt congruence/equality *)
+
 (** {6 Views} *)
 
 val is_true : t -> bool

src/smt/Term_cell.ml

@@ -50,6 +50,11 @@ include Make_eq(struct
 let true_ = Bool true
 let false_ = Bool false
 
+let is_value = function
+  | Bool _ -> true
+  | App_cst ({cst_view=Cst_def r;_}, _) -> r.is_value
+  | If _ | App_cst _ -> false
+
 let app_cst f a = App_cst (f, a)
 let const c = App_cst (c, IArray.empty)
 

src/smt/Term_cell.mli

@@ -17,6 +17,8 @@ val const : cst -> t
 val app_cst : cst -> term IArray.t -> t
 val if_ : term -> term -> term -> t
 
+val is_value : t -> bool
+
 val ty : t -> Ty.t
 (** Compute the type of this term cell. Not totally free *)
 

src/smt/th_bool/Sidekick_th_bool.ml

@@ -93,7 +93,8 @@ module C = struct
 
   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; eval=eval id; }; }
+     cst_view=Cst_def {
+         pp=None; abs; ty=get_ty; relevant; is_value=false; do_cc; eval=eval id; }; }
 
   let not = mk_cst id_not
   let and_ = mk_cst id_and