[sledge] Remove the redundancy of both < and >= terms

Summary: It is not necessary to have both < and >=, and similarly for <= and >.

Reviewed By: bennostein

Differential Revision: D17665232

fbshipit-source-id: 01b3511f5

sledge/src/symbheap/term.ml

@@ -35,8 +35,6 @@ module rec T : sig
     (* binary: comparison *)
     | Eq
     | Dq
-    | Gt
-    | Ge
     | Lt
     | Le
     | Ord
@@ -93,8 +91,6 @@ and T0 : sig
     | App of {op: t; arg: t}
     | Eq
     | Dq
-    | Gt
-    | Ge
     | Lt
     | Le
     | Ord
@@ -132,8 +128,6 @@ end = struct
     | App of {op: t; arg: t}
     | Eq
     | Dq
-    | Gt
-    | Ge
     | Lt
     | Le
     | Ord
@@ -214,8 +208,6 @@ let rec pp ?is_x fs term =
     | Float {data} -> pf "%s" data
     | Eq -> pf "="
     | Dq -> pf "@<1>≠"
-    | Gt -> pf ">"
-    | Ge -> pf "@<1>≥"
     | Lt -> pf "<"
     | Le -> pf "@<1>≤"
     | Ord -> pf "ord"
@@ -373,8 +365,7 @@ let invariant ?(partial = false) e =
       assert (Typ.convertible src dst)
   | Add _ -> assert_polynomial e |> Fn.id
   | Mul _ -> assert_monomial e |> Fn.id
-  | Eq | Dq | Gt | Ge | Lt | Le | Div | Rem | And | Or | Xor | Shl | Lshr
+  | Eq | Dq | Lt | Le | Div | Rem | And | Or | Xor | Shl | Lshr | Ashr ->
-   |Ashr ->
       assert_arity 2
   | Concat {args} -> assert (Vector.length args <> 1)
   | Splat {siz} -> (
@@ -558,16 +549,6 @@ let simp_convert ~unsigned dst src arg =
         integer (Z.extract ~unsigned (min m n) data)
     | _ -> App {op= Convert {unsigned; dst; src}; arg}
 
-let simp_gt x y =
-  match (x, y) with
-  | Integer {data= i}, Integer {data= j} -> bool (Z.gt i j)
-  | _ -> App {op= App {op= Gt; arg= x}; arg= y}
-
-let simp_ge x y =
-  match (x, y) with
-  | Integer {data= i}, Integer {data= j} -> bool (Z.geq i j)
-  | _ -> App {op= App {op= Ge; arg= x}; arg= y}
-
 let simp_lt x y =
   match (x, y) with
   | Integer {data= i}, Integer {data= j} -> bool (Z.lt i j)
@@ -776,7 +757,7 @@ let rec simp_or x y =
   | _ -> App {op= App {op= Or; arg= x}; arg= y}
 
 let rec is_boolean = function
-  | App {op= App {op= Eq | Dq | Gt | Ge | Lt | Le}}
+  | App {op= App {op= Eq | Dq | Lt | Le}}
    |App {op= Convert {dst= Integer {bits= 1}}} ->
       true
   | App
@@ -792,14 +773,10 @@ let rec simp_not term =
   | App {op= App {op= Eq; arg= x}; arg= y} -> simp_dq x y
   (* ¬(x ≠ y) ==> x = y *)
   | App {op= App {op= Dq; arg= x}; arg= y} -> simp_eq x y
-  (* ¬(x > y) ==> x <= y *)
+  (* ¬(x < y) ==> y <= x *)
-  | App {op= App {op= Gt; arg= x}; arg= y} -> simp_le x y
+  | App {op= App {op= Lt; arg= x}; arg= y} -> simp_le y x
-  (* ¬(x >= y) ==> x < y *)
+  (* ¬(x <= y) ==> y < x *)
-  | App {op= App {op= Ge; arg= x}; arg= y} -> simp_lt x y
+  | App {op= App {op= Le; arg= x}; arg= y} -> simp_lt y x
-  (* ¬(x < y) ==> x >= y *)
-  | App {op= App {op= Lt; arg= x}; arg= y} -> simp_ge x y
-  (* ¬(x <= y) ==> x > y *)
-  | App {op= App {op= Le; arg= x}; arg= y} -> simp_gt x y
   (* ¬(x ≠ nan ∧ y ≠ nan) ==> x = nan ∨ y = nan *)
   | App {op= App {op= Ord; arg= x}; arg= y} -> simp_uno x y
   (* ¬(x = nan ∨ y = nan) ==> x ≠ nan ∧ y ≠ nan *)
@@ -917,8 +894,6 @@ let app1 ?(partial = false) op arg =
   ( match (op, arg) with
   | App {op= Eq; arg= x}, y -> simp_eq x y
   | App {op= Dq; arg= x}, y -> simp_dq x y
-  | App {op= Gt; arg= x}, y -> simp_gt x y
-  | App {op= Ge; arg= x}, y -> simp_ge x y
   | App {op= Lt; arg= x}, y -> simp_lt x y
   | App {op= Le; arg= x}, y -> simp_le x y
   | App {op= Ord; arg= x}, y -> simp_ord x y
@@ -988,8 +963,6 @@ let simp_splat byt siz =
 let splat ~byt ~siz = simp_splat byt siz |> check invariant
 let eq = app2 Eq
 let dq = app2 Dq
-let gt = app2 Gt
-let ge = app2 Ge
 let lt = app2 Lt
 let le = app2 Le
 let ord = app2 Ord
@@ -1065,14 +1038,10 @@ let rec of_exp (e : Exp.t) =
       select ~rcd:(of_exp arg) ~idx:(integer (Z.of_int idx))
   | Ap2 (Eq, _, x, y) -> eq (of_exp x) (of_exp y)
   | Ap2 (Dq, _, x, y) -> dq (of_exp x) (of_exp y)
-  | Ap2 (Gt, _, x, y) -> gt (of_exp x) (of_exp y)
+  | Ap2 (Lt, _, x, y) | Ap2 (Gt, _, y, x) -> lt (of_exp x) (of_exp y)
-  | Ap2 (Ge, _, x, y) -> ge (of_exp x) (of_exp y)
+  | Ap2 (Le, _, x, y) | Ap2 (Ge, _, y, x) -> le (of_exp x) (of_exp y)
-  | Ap2 (Lt, _, x, y) -> lt (of_exp x) (of_exp y)
+  | Ap2 (Ult, typ, x, y) | Ap2 (Ugt, typ, y, x) -> unsigned lt typ x y
-  | Ap2 (Le, _, x, y) -> le (of_exp x) (of_exp y)
+  | Ap2 (Ule, typ, x, y) | Ap2 (Uge, typ, y, x) -> unsigned le typ x y
-  | Ap2 (Ugt, typ, x, y) -> unsigned gt typ x y
-  | Ap2 (Uge, typ, x, y) -> unsigned ge typ x y
-  | Ap2 (Ult, typ, x, y) -> unsigned lt typ x y
-  | Ap2 (Ule, typ, x, y) -> unsigned le typ x y
   | Ap2 (Ord, _, x, y) -> ord (of_exp x) (of_exp y)
   | Ap2 (Uno, _, x, y) -> uno (of_exp x) (of_exp y)
   | Ap2 (Add, _, x, y) -> add (of_exp x) (of_exp y)

sledge/src/symbheap/term.mli

@@ -37,8 +37,6 @@ and t = private
       (** Application of function symbol to argument, curried *)
   | Eq  (** Equal test *)
   | Dq  (** Disequal test *)
-  | Gt  (** Greater-than test *)
-  | Ge  (** Greater-than-or-equal test *)
   | Lt  (** Less-than test *)
   | Le  (** Less-than-or-equal test *)
   | Ord  (** Ordered test (neither arg is nan) *)
@@ -145,8 +143,6 @@ val rational : Q.t -> t
 val float : string -> t
 val eq : t -> t -> t
 val dq : t -> t -> t
-val gt : t -> t -> t
-val ge : t -> t -> t
 val lt : t -> t -> t
 val le : t -> t -> t
 val ord : t -> t -> t

sledge/src/symbheap/term_test.ml

@@ -16,8 +16,6 @@ let%test_module _ =
     let ( * ) = Term.mul
     let ( = ) = Term.eq
     let ( != ) = Term.dq
-    let ( > ) = Term.gt
-    let ( >= ) = Term.ge
     let ( < ) = Term.lt
     let ( <= ) = Term.le
     let ( && ) = Term.and_
@@ -235,12 +233,12 @@ let%test_module _ =
       [%expect {| ((13 × %z_2 + -42) = (3 × %y_1 + 13 × %z_2)) |}]
 
     let%expect_test _ =
-      pp ~~(y > !2 && z <= !3) ;
+      pp ~~(!2 < y && z <= !3) ;
-      [%expect {| ((%y_1 ≤ 2) || (%z_2 > 3)) |}]
+      [%expect {| ((%y_1 ≤ 2) || (3 < %z_2)) |}]
 
     let%expect_test _ =
-      pp ~~(y >= !2 || z < !3) ;
+      pp ~~(!2 <= y || z < !3) ;
-      [%expect {| ((%y_1 < 2) && (%z_2 ≥ 3)) |}]
+      [%expect {| ((%y_1 < 2) && (3 ≤ %z_2)) |}]
 
     let%expect_test _ =
       pp Term.(eq z null) ;