Remove unused symbols Reach and Fixed (#960)

These symboles are never produced by both legacy and Dolmen parsers. This commit removes them completely.
OCamlPro · Nov 21, 2023 · 7ee15af · 7ee15af
1 parent cb9c90c
commit 7ee15af
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 13 deletions.
diff --git 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
-
     (*** <end>: partial handling of some arith/FPA operators **)
 
     | _ ->

diff --git 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
@@ -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
@@ -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