From 2ca94c2f3e87b9fe55a9046507c604d57872864a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Sun, 19 May 2024 16:19:20 +0200 Subject: [PATCH] Remove the useless `ty` argument of `is_mine_symb` The argument `ty` of `is_mine_symbol` was only used by `Enum` and `Adt` theories because they shared the `Construct` symbol. As we merged these theories, we can remove this argument now. --- src/lib/reasoners/ac.ml | 6 ++--- src/lib/reasoners/ac.mli | 4 ++-- src/lib/reasoners/adt.ml | 8 +++---- src/lib/reasoners/arith.ml | 6 ++--- src/lib/reasoners/bitv.ml | 2 +- src/lib/reasoners/ccx.ml | 2 +- src/lib/reasoners/records.ml | 7 +++--- src/lib/reasoners/shostak.ml | 45 ++++++++++++++++++------------------ src/lib/reasoners/sig.mli | 8 +++---- src/lib/reasoners/uf.ml | 2 +- 10 files changed, 44 insertions(+), 46 deletions(-) diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index 2a3edb449..df9eeea71 100644 --- a/src/lib/reasoners/ac.ml +++ b/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 diff --git a/src/lib/reasoners/ac.mli b/src/lib/reasoners/ac.mli index e1a1f7dca..1219fb9f6 100644 --- a/src/lib/reasoners/ac.mli +++ b/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 diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 5fab09d5e..612d8376e 100644 --- a/src/lib/reasoners/adt.ml +++ b/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 diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 9a532a33b..b278ca920 100644 --- a/src/lib/reasoners/arith.ml +++ b/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 diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 39080aad2..fc63dcaba 100644 --- a/src/lib/reasoners/bitv.ml +++ b/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) diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index 66149abdb..ac732db92 100644 --- a/src/lib/reasoners/ccx.ml +++ b/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 = diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index 56e62fa84..e5d354e2a 100644 --- a/src/lib/reasoners/records.ml +++ b/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 diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 0c38e426d..c7a0273ff 100644 --- a/src/lib/reasoners/shostak.ml +++ b/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 diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index 535b76a84..3e05ceb83 100644 --- a/src/lib/reasoners/sig.mli +++ b/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,7 +186,7 @@ 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 @@ -194,7 +194,7 @@ module type X = sig 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 diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 9b2b6f2a3..aeff9649d 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1183,7 +1183,7 @@ let compute_concrete_model_of_val cache = and get_abstract_for = Cache.get_abstract_for cache.abstracts in fun env t ((mdl, mrepr) as acc) -> let { E.f; xs; ty; _ } = E.term_view t in - 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