From 5ea779671a5084cc78c4d5aa59c6202225270ed2 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 20 Oct 2020 11:40:05 -0700
Subject: [PATCH] [sledge] Remove non-zero formula

Summary: It is redundant with `Not Eq0`

Reviewed By: ngorogiannis

Differential Revision: D24306058

fbshipit-source-id: 75ca55016
---
 sledge/src/fol.ml | 34 +++++++++-------------------------
 1 file changed, 9 insertions(+), 25 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index f9ba0169a..c3870cbd6 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -261,7 +261,6 @@ module Fml : sig
     | Eq of trm * trm
     (* arithmetic *)
     | Eq0 of trm  (** [Eq0(x)] iff x = 0 *)
-    | Dq0 of trm  (** [Dq0(x)] iff x ≠ 0 *)
     | Gt0 of trm  (** [Gt0(x)] iff x > 0 *)
     | Le0 of trm  (** [Le0(x)] iff x ≤ 0 *)
     (* propositional connectives *)
@@ -279,7 +278,6 @@ module Fml : sig
   val _Tt : fml
   val _Eq : trm -> trm -> fml
   val _Eq0 : trm -> fml
-  val _Dq0 : trm -> fml
   val _Gt0 : trm -> fml
   val _Le0 : trm -> fml
   val _Not : fml -> fml
@@ -295,7 +293,6 @@ end = struct
     | Tt
     | Eq of trm * trm
     | Eq0 of trm
-    | Dq0 of trm
     | Gt0 of trm
     | Le0 of trm
     | Not of fml
@@ -340,14 +337,6 @@ end = struct
     | SemDq -> _Ff
     | SynLt | SynGt -> Eq0 x
 
-  let _Dq0 x =
-    match compare_semantic_syntactic zero x with
-    (* 0 ≠ 0 ==> ff *)
-    | SemEq -> _Ff
-    (* 0 ≠ N ==> tt for N ≢ 0 *)
-    | SemDq -> Tt
-    | SynLt | SynGt -> Dq0 x
-
   let _Eq x y =
     if x == zero then _Eq0 y
     else if y == zero then _Eq0 x
@@ -372,7 +361,7 @@ end = struct
   let _UNegLit p xs = UNegLit (p, xs)
 
   let rec is_negative = function
-    | Not (Tt | Eq _) | Dq0 _ | Le0 _ | Or _ | Xor _ | UNegLit _ -> true
+    | Not (Tt | Eq _ | Eq0 _) | Le0 _ | Or _ | Xor _ | UNegLit _ -> true
     | Tt | Eq _ | Eq0 _ | Gt0 _ | And _ | Iff _ | UPosLit _ | Cond _ ->
         false
     | Not p -> not (is_negative p)
@@ -382,7 +371,7 @@ end = struct
   let rec equal_or_opposite p q =
     match (p, q) with
     | p, Not p' | Not p', p -> if equal_fml p p' then Opposite else Unknown
-    | Eq0 a, Dq0 a' | Dq0 a, Eq0 a' | Gt0 a, Le0 a' | Le0 a, Gt0 a' ->
+    | Gt0 a, Le0 a' | Le0 a, Gt0 a' ->
         if equal_trm a a' then Opposite else Unknown
     | And (a, b), Or (a', b') | Or (a', b'), And (a, b) -> (
       match equal_or_opposite a a' with
@@ -458,8 +447,6 @@ end = struct
           Xor (p, q) )
 
   and _Not = function
-    | Eq0 x -> _Dq0 x
-    | Dq0 x -> _Eq0 x
     | Gt0 x -> _Le0 x
     | Le0 x -> _Gt0 x
     | Not x -> x
@@ -470,7 +457,7 @@ end = struct
     | Cond {cnd; pos; neg} -> _Cond cnd (_Not pos) (_Not neg)
     | UPosLit (p, xs) -> _UNegLit p xs
     | UNegLit (p, xs) -> _UPosLit p xs
-    | (Tt | Eq _) as x -> Not x
+    | (Tt | Eq _ | Eq0 _) as x -> Not x
 
   and _Cond cnd pos neg =
     match (cnd, pos, neg) with
@@ -539,7 +526,7 @@ let ppx_f strength fs fml =
     | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
     | Not (Eq (x, y)) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
     | Eq0 x -> pf "(0 = %a)" pp_t x
-    | Dq0 x -> pf "(0 @<2>≠ %a)" pp_t x
+    | Not (Eq0 x) -> pf "(0 @<2>≠ %a)" pp_t x
     | Gt0 x -> pf "(0 < %a)" pp_t x
     | Le0 x -> pf "(0 @<2>≥ %a)" pp_t x
     | Not x -> pf "@<1>¬%a" pp x
@@ -597,7 +584,7 @@ let rec fold_vars_f ~init p ~f =
   match (p : fml) with
   | Tt -> init
   | Eq (x, y) -> fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
-  | Eq0 x | Dq0 x | Gt0 x | Le0 x -> fold_vars_t ~f x ~init
+  | Eq0 x | Gt0 x | Le0 x -> fold_vars_t ~f x ~init
   | Not x -> fold_vars_f ~f x ~init
   | And (x, y) | Or (x, y) | Iff (x, y) | Xor (x, y) ->
       fold_vars_f ~f x ~init:(fold_vars_f ~f y ~init)
@@ -646,7 +633,6 @@ let rec map_trms_f ~f b =
   | Tt -> b
   | Eq (x, y) -> map2 f b _Eq x y
   | Eq0 x -> map1 f b _Eq0 x
-  | Dq0 x -> map1 f b _Dq0 x
   | Gt0 x -> map1 f b _Gt0 x
   | Le0 x -> map1 f b _Le0 x
   | Not x -> map1 (map_trms_f ~f) b _Not x
@@ -747,7 +733,7 @@ let project_out_fml : cnd -> fml option = function
       [0 ≠ x] holds. *)
 let embed_into_fml : exp -> fml = function
   | `Fml fml -> fml
-  | #cnd as c -> map_cnd _Cond _Dq0 c
+  | #cnd as c -> map_cnd _Cond (fun e -> _Not (_Eq0 e)) c
 
 (** Construct a conditional term, or formula if possible precisely. *)
 let ite : fml -> exp -> exp -> exp =
@@ -956,7 +942,7 @@ module Formula = struct
   let eq = ap2f _Eq
   let dq a b = _Not (eq a b)
   let eq0 = ap1f _Eq0
-  let dq0 = ap1f _Dq0
+  let dq0 a = _Not (eq0 a)
   let gt0 = ap1f _Gt0
   let le0 = ap1f _Le0
   let ge0 a = le0 (Term.neg a)
@@ -1020,7 +1006,6 @@ module Formula = struct
     | Tt -> b
     | Eq (x, y) -> lift_map2 f b _Eq x y
     | Eq0 x -> lift_map1 f b _Eq0 x
-    | Dq0 x -> lift_map1 f b _Dq0 x
     | Gt0 x -> lift_map1 f b _Gt0 x
     | Le0 x -> lift_map1 f b _Le0 x
     | Not x -> map1 (map_terms ~f) b _Not x
@@ -1054,8 +1039,8 @@ module Formula = struct
    fun ~meet1 ~join1 ~top ~bot fml ->
     let rec add_conjunct (cjn, splits) fml =
       match fml with
-      | Tt | Eq _ | Eq0 _ | Dq0 _ | Gt0 _ | Le0 _ | Iff _ | Xor _
-       |UPosLit _ | UNegLit _ | Not _ ->
+      | Tt | Eq _ | Eq0 _ | Gt0 _ | Le0 _ | Iff _ | Xor _ | UPosLit _
+       |UNegLit _ | Not _ ->
           (meet1 fml cjn, splits)
       | And (p, q) -> add_conjunct (add_conjunct (cjn, splits) p) q
       | Or (p, q) -> (cjn, [p; q] :: splits)
@@ -1130,7 +1115,6 @@ let rec f_to_ses : fml -> Ses.Term.t = function
   | Not Tt -> Ses.Term.false_
   | Eq (x, y) -> Ses.Term.eq (t_to_ses x) (t_to_ses y)
   | Eq0 x -> Ses.Term.eq Ses.Term.zero (t_to_ses x)
-  | Dq0 x -> Ses.Term.dq Ses.Term.zero (t_to_ses x)
   | Gt0 x -> Ses.Term.lt Ses.Term.zero (t_to_ses x)
   | Le0 x -> Ses.Term.le (t_to_ses x) Ses.Term.zero
   | Not p -> Ses.Term.not_ (f_to_ses p)