Simplify is_mine_symb

src/lib/reasoners/ac.ml

@@ -39,8 +39,8 @@ module type S = sig
   (* builds an embeded semantic value from an AC term *)
   val make : Expr.t -> r * Expr.t list
 
-  (* tells whether the given term is AC*)
-  val is_mine_symb : Sy.t -> Ty.t -> bool
+  (* Tells whether the given symbol is AC. *)
+  val is_mine_symb : Sy.t -> bool
 
   (* compares two AC semantic values *)
   val compare : t -> t -> int
@@ -238,7 +238,7 @@ module Make (X : Sig.X) = struct
          got %i (%a)." (List.length xs) Expr.print_list xs;
       assert false
 
-  let is_mine_symb sy _ = (not @@ Options.get_no_ac ()) && Sy.is_ac sy
+  let is_mine_symb sy = (not @@ Options.get_no_ac ()) && Sy.is_ac sy
 
   let type_info { t = ty; _ } = ty
 

src/lib/reasoners/ac.mli

@@ -36,8 +36,8 @@ module type S = sig
   (* builds an embeded semantic value from an AC term *)
   val make : Expr.t -> r * Expr.t list
 
-  (* tells whether the given term is AC*)
-  val is_mine_symb : Symbols.t -> Ty.t -> bool
+  (** Tells whether the given symbol is AC. *)
+  val is_mine_symb : Symbols.t -> bool
 
   (* compares two AC semantic values *)
   val compare : t -> t -> int

src/lib/reasoners/adt.ml

@@ -80,11 +80,11 @@ module Shostak (X : ALIEN) = struct
 
   [@@ocaml.ppwarning "XXX: IsConstr not interpreted currently. Maybe \
                       it's OK"]
-  let is_mine_symb sy ty =
+  let is_mine_symb sy =
     not (Options.get_disable_adts ()) &&
-    match sy, ty with
-    | Sy.Op (Sy.Constr _), Ty.Tadt _ -> true
-    | Sy.Op Sy.Destruct _, Ty.Tadt _ ->
+    match sy with
+    | Sy.Op Sy.Constr _ -> true
+    | Sy.Op Sy.Destruct _ ->
       (* A destructor is partially interpreted by the ADT theory.
          If we assume the tester of the constructor associated with
          this destructor, we propagate the non-guarded version of the

src/lib/reasoners/arith.ml

@@ -110,7 +110,7 @@ module Shostak
   end
   (*BISECT-IGNORE-END*)
 
-  let is_mine_symb sy _ty =
+  let is_mine_symb sy =
     let open Sy in
     match sy with
     | Int _ | Real _ -> true
@@ -773,8 +773,8 @@ module Shostak
       else
       if List.exists
           (fun (t,x) ->
-             let E.{f; ty; _} = E.term_view t in
-             is_mine_symb f ty && X.leaves x == []
+             let E.{f; _} = E.term_view t in
+             is_mine_symb f && X.leaves x == []
           ) eq
       then None
       else

src/lib/reasoners/bitv.ml

@@ -344,7 +344,7 @@ module Shostak(X : ALIEN) = struct
 
   let timer = Timers.M_Bitv
 
-  let is_mine_symb sy _ =
+  let is_mine_symb sy =
     match sy with
     | Sy.Bitv _
     | Op (Concat | Extract _ | BV2Nat | BVnot | BVand | BVor | BVxor)

src/lib/reasoners/ccx.ml

@@ -280,7 +280,7 @@ module Main : S = struct
   let congruents env (facts: r Sig_rel.facts) t1 s =
     match E.term_view t1 with
     | { E.xs = []; _ } -> ()
-    | { E.f; ty; _ } when X.fully_interpreted f ty -> ()
+    | { E.f; _ } when X.fully_interpreted f -> ()
     |  _ -> SE.iter (equal_only_by_congruence env facts t1) s
 
   let fold_find_with_explanation find ex l =

src/lib/reasoners/records.ml

@@ -244,12 +244,11 @@ module Shostak (X : ALIEN) = struct
 
   let subst p v r = is_mine (subst_rec p v r)
 
-  let is_mine_symb_aux sy = match sy with
+  let is_mine_symb sy =
+    match sy with
     | Symbols.Op (Symbols.Record | Symbols.Access _) -> true
     | _ -> false
 
-  let is_mine_symb sy _ty = is_mine_symb_aux sy
-
   let abstract_access field e ty acc =
     let xe = is_mine e in
     let abs_right_xe, acc =
@@ -328,7 +327,7 @@ module Shostak (X : ALIEN) = struct
      | Other _ -> e
   *)
 
-  let fully_interpreted = is_mine_symb_aux
+  let fully_interpreted = is_mine_symb
 
   let rec term_extract r =
     match X.extract r with

src/lib/reasoners/shostak.ml

@@ -351,14 +351,14 @@ struct
       | Term _ -> if equal p r then v else r
 
   let make t =
-    let { Expr.f = sb; ty; _ } = Expr.term_view t in
+    let { Expr.f = sb; _ } = Expr.term_view t in
     let not_restricted = not @@ Options.get_restricted () in
     match
-      ARITH.is_mine_symb sb ty,
-      not_restricted && RECORDS.is_mine_symb sb ty,
-      not_restricted && BITV.is_mine_symb sb ty,
-      not_restricted && ADT.is_mine_symb sb ty,
-      AC.is_mine_symb sb ty
+      ARITH.is_mine_symb sb,
+      not_restricted && RECORDS.is_mine_symb sb,
+      not_restricted && BITV.is_mine_symb sb,
+      not_restricted && ADT.is_mine_symb sb,
+      AC.is_mine_symb sb
     with
     | true, false, false, false, false ->
       Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () ->
@@ -385,14 +385,14 @@ struct
 
     | _ -> assert false
 
-  let fully_interpreted sb ty =
+  let fully_interpreted sb =
     let not_restricted = not @@ Options.get_restricted () in
     match
-      ARITH.is_mine_symb sb ty,
-      not_restricted && RECORDS.is_mine_symb sb ty,
-      not_restricted && BITV.is_mine_symb sb ty,
-      not_restricted && ADT.is_mine_symb sb ty,
-      AC.is_mine_symb sb ty
+      ARITH.is_mine_symb sb,
+      not_restricted && RECORDS.is_mine_symb sb,
+      not_restricted && BITV.is_mine_symb sb,
+      not_restricted && ADT.is_mine_symb sb,
+      AC.is_mine_symb sb
     with
     | true, false, false, false, false ->
       ARITH.fully_interpreted sb
@@ -408,12 +408,12 @@ struct
       false
     | _ -> assert false
 
-  let is_solvable_theory_symbol sb ty =
-    ARITH.is_mine_symb sb ty ||
+  let is_solvable_theory_symbol sb =
+    ARITH.is_mine_symb sb ||
     not (Options.get_restricted ()) &&
-    (RECORDS.is_mine_symb sb ty ||
-     BITV.is_mine_symb sb ty ||
-     ADT.is_mine_symb sb ty)
+    (RECORDS.is_mine_symb sb ||
+     BITV.is_mine_symb sb ||
+     ADT.is_mine_symb sb)
 
   let is_a_leaf r = match r.v with
     | Term _ | Ac _ -> true
@@ -424,13 +424,12 @@ struct
     | [] -> assert false
     | [r,1] -> r
     | _ ->
-      let ty = ac.Sig.t in
       match
-        ARITH.is_mine_symb ac.Sig.h ty,
-        RECORDS.is_mine_symb ac.Sig.h ty,
-        BITV.is_mine_symb ac.Sig.h ty,
-        ADT.is_mine_symb ac.Sig.h ty,
-        AC.is_mine_symb ac.Sig.h ty with
+        ARITH.is_mine_symb ac.Sig.h,
+        RECORDS.is_mine_symb ac.Sig.h,
+        BITV.is_mine_symb ac.Sig.h,
+        ADT.is_mine_symb ac.Sig.h,
+        AC.is_mine_symb ac.Sig.h with
       (*AC.is_mine may say F if Options.get_no_ac is set to F dynamically *)
       | true, false, false, false, false ->
         ARITH.color ac

src/lib/reasoners/sig.mli

@@ -43,8 +43,8 @@ module type SHOSTAK = sig
 
   val timer : Timers.ty_module
 
-  (** return true if the symbol and the type are owned by the theory*)
-  val is_mine_symb : Symbols.t -> Ty.t -> bool
+  val is_mine_symb : Symbols.t -> bool
+  (** Return [true] if the symbol is owned by the theory. *)
 
   (** Give a representant of a term of the theory*)
   val make : Expr.t -> r * Expr.t list
@@ -186,15 +186,15 @@ module type X = sig
 
   val color : (r ac) -> r
 
-  val fully_interpreted : Symbols.t -> Ty.t -> bool
+  val fully_interpreted : Symbols.t -> bool
 
   val is_a_leaf : r -> bool
 
   val print : Format.formatter -> r -> unit
 
   val abstract_selectors : r -> (r * r) list -> r * (r * r) list
 
-  val is_solvable_theory_symbol : Symbols.t -> Ty.t -> bool
+  val is_solvable_theory_symbol : Symbols.t -> bool
 
   (* the returned bool is true when the returned term in a constant of the
      theory. Otherwise, the term contains aliens that should be assigned

src/lib/reasoners/uf.ml

@@ -1187,7 +1187,7 @@ let compute_concrete_model_of_val cache =
        pending destructors as solvable theory symbols of the ADT theory.
        We should check if these symbols can be defined as solvable to
        remove this particular case here. *)
-    if X.is_solvable_theory_symbol f ty || is_destructor f
+    if X.is_solvable_theory_symbol f || is_destructor f
        || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t
        || E.equal t E.vrai || E.equal t E.faux
     then