From bbef19b9e574e04f944c6676037aa1f45bdce6f2 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 21 Nov 2023 15:17:55 +0100 Subject: [PATCH] Remove unused symbols `Reach` and `Fixed` These symboles are never produced by both legacy and Dolmen parsers. This commit removes them completely. --- src/lib/reasoners/arith.ml | 6 +----- src/lib/structures/modelMap.ml | 2 +- src/lib/structures/symbols.ml | 7 ++----- src/lib/structures/symbols.mli | 3 +-- 4 files changed, 5 insertions(+), 13 deletions(-) diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 696706c70..9fa3a8a2f 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -116,7 +116,7 @@ module Shostak match sy with | Int _ | Real _ -> true | Op (Plus | Minus | Mult | Div | Modulo - | Float | Fixed | Abs_int | Abs_real | Sqrt_real + | Float | Abs_int | Abs_real | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Real_of_int | Int_floor | Int_ceil | Max_int | Max_real | Min_int | Min_real @@ -354,10 +354,6 @@ module Shostak mk_partial_interpretation_2 (fun x y -> calc_power x y ty) coef p ty t x y, ctx - | Sy.Op Sy.Fixed, _ -> - (* Fixed-Point arithmetic currently not implemented *) - assert false - (*** : partial handling of some arith/FPA operators **) | _ -> diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index ff06afff0..965270b07 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -94,7 +94,7 @@ let is_suspicious_name hs = (* The model generation is known to be imcomplete for FPA and Bitvector theories. *) let is_suspicious_symbol = function - | Sy.Op (Float | Fixed | Abs_int | Abs_real | Sqrt_real + | Sy.Op (Float | Abs_int | Abs_real | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Real_of_int | Int_floor | Int_ceil | Max_int | Max_real | Min_int | Min_real diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 2f443c8c5..03babc9c0 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -36,7 +36,6 @@ type operator = | Tite (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow - | Reach (* ADTs *) | Access of Hstring.t | Record | Constr of Hstring.t (* enums, adts *) @@ -49,7 +48,7 @@ type operator = | BVnot | BVand | BVor | Int2BV of int | BV2Nat (* FP *) | Float - | Integer_round | Fixed + | Integer_round | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Abs_int | Abs_real | Real_of_int | Real_is_int | Int_floor | Int_ceil | Integer_log2 @@ -165,7 +164,7 @@ let compare_operators op1 op2 = if c <> 0 then c else Stdlib.compare b1 b2 | _ , (Plus | Minus | Mult | Div | Modulo | Real_is_int - | Concat | Extract _ | Get | Set | Fixed | Float | Reach + | Concat | Extract _ | Get | Set | Float | Access _ | Record | Sqrt_real | Abs_int | Abs_real | Real_of_int | Int_floor | Int_ceil | Sqrt_real_default | Sqrt_real_excess | Min_real | Min_int | Max_real | Max_int @@ -344,7 +343,6 @@ let to_string ?(show_vars=true) x = match x with | Op Get -> "get" | Op Set -> "set" | Op Float -> "float" - | Op Fixed -> "fixed" | Op Abs_int -> "abs_int" | Op Abs_real -> "abs_real" | Op Sqrt_real -> "sqrt_real" @@ -372,7 +370,6 @@ let to_string ?(show_vars=true) x = match x with | Op Int2BV n -> Format.sprintf "int2bv[%d]" n | Op BV2Nat -> "bv2nat" | Op Tite -> "ite" - | Op Reach -> assert false | True -> "true" | False -> "false" | Void -> "void" diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 59078b83f..0114e616f 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -36,7 +36,6 @@ type operator = | Tite (* Arithmetic *) | Plus | Minus | Mult | Div | Modulo | Pow - | Reach (* ADTs *) | Access of Hstring.t | Record | Constr of Hstring.t (* enums, adts *) @@ -49,7 +48,7 @@ type operator = | BVnot | BVand | BVor | Int2BV of int | BV2Nat (* FP *) | Float - | Integer_round | Fixed + | Integer_round | Sqrt_real | Sqrt_real_default | Sqrt_real_excess | Abs_int | Abs_real | Real_of_int | Real_is_int | Int_floor | Int_ceil | Integer_log2