[sledge] Remove exclusive-or formula

Summary: It is redundant with `Not Iff`

Reviewed By: jvillard

Differential Revision: D24306098

fbshipit-source-id: be732d22c

sledge/src/fol.ml

@@ -267,7 +267,6 @@ module Fml : sig
     | And of fml * fml
     | Or of fml * fml
     | Iff of fml * fml
-    | Xor of fml * fml
     | Cond of {cnd: fml; pos: fml; neg: fml}
     (* uninterpreted literals *)
     | Lit of Predsym.t * trm array
@@ -281,7 +280,6 @@ module Fml : sig
   val _And : fml -> fml -> fml
   val _Or : fml -> fml -> fml
   val _Iff : fml -> fml -> fml
-  val _Xor : fml -> fml -> fml
   val _Cond : fml -> fml -> fml -> fml
   val _Lit : Predsym.t -> trm array -> fml
 end = struct
@@ -294,7 +292,6 @@ end = struct
     | And of fml * fml
     | Or of fml * fml
     | Iff of fml * fml
-    | Xor of fml * fml
     | Cond of {cnd: fml; pos: fml; neg: fml}
     | Lit of Predsym.t * trm array
   [@@deriving compare, equal, sexp]
@@ -349,7 +346,7 @@ end = struct
   let _Lit p xs = Lit (p, xs)
 
   let rec is_negative = function
-    | Not (Tt | Eq _ | Eq0 _ | Gt0 _ | Lit _) | Or _ | Xor _ -> true
+    | Not (Tt | Eq _ | Eq0 _ | Gt0 _ | Lit _ | Iff _) | Or _ -> true
     | Tt | Eq _ | Eq0 _ | Gt0 _ | And _ | Iff _ | Lit _ | Cond _ -> false
     | Not p -> not (is_negative p)
 
@@ -365,8 +362,6 @@ end = struct
         | Opposite -> Opposite
         | _ -> Unknown )
       | _ -> Unknown )
-    | Iff (p, q), Xor (p', q') | Xor (p, q), Iff (p', q') ->
-        if equal_fml p p' && equal_fml q q' then Opposite else Unknown
     | Cond {cnd= c; pos= p; neg= n}, Cond {cnd= c'; pos= p'; neg= n'} ->
         if equal_fml c c' then
           match equal_or_opposite p p' with
@@ -415,26 +410,12 @@ end = struct
           let p, q = sort_fml p q in
           Iff (p, q) )
 
-  and _Xor p q =
-    match (p, q) with
-    | Tt, p | p, Tt -> _Not p
-    | Not Tt, p | p, Not Tt -> p
-    | _ -> (
-      match equal_or_opposite p q with
-      | Equal -> _Ff
-      | Opposite -> Tt
-      | Unknown ->
-          let p, q = sort_fml p q in
-          Xor (p, q) )
-
   and _Not = function
     | Not x -> x
     | And (x, y) -> _Or (_Not x) (_Not y)
     | Or (x, y) -> _And (_Not x) (_Not y)
-    | Iff (x, y) -> _Xor x y
-    | Xor (x, y) -> _Iff x y
     | Cond {cnd; pos; neg} -> _Cond cnd (_Not pos) (_Not neg)
-    | (Tt | Eq _ | Eq0 _ | Gt0 _ | Lit _) as x -> Not x
+    | (Tt | Eq _ | Eq0 _ | Gt0 _ | Lit _ | Iff _) as x -> Not x
 
   and _Cond cnd pos neg =
     match (cnd, pos, neg) with
@@ -510,7 +491,6 @@ let ppx_f strength fs fml =
     | And (x, y) -> pf "(%a@ @<2>∧ %a)" pp x pp y
     | Or (x, y) -> pf "(%a@ @<2>∨ %a)" pp x pp y
     | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
-    | Xor (x, y) -> pf "(%a@ xor %a)" pp x pp y
     | Cond {cnd; pos; neg} ->
         pf "@[<hv 1>(%a@ ? %a@ : %a)@]" pp cnd pp pos pp neg
     | Lit (p, xs) -> pf "%a(%a)" Predsym.pp p (Array.pp ",@ " pp_t) xs
@@ -561,7 +541,7 @@ let rec fold_vars_f ~init p ~f =
   | Eq (x, y) -> fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
   | Eq0 x | Gt0 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) ->
+  | And (x, y) | Or (x, y) | Iff (x, y) ->
       fold_vars_f ~f x ~init:(fold_vars_f ~f y ~init)
   | Cond {cnd; pos; neg} ->
       fold_vars_f ~f cnd
@@ -612,7 +592,6 @@ let rec map_trms_f ~f b =
   | And (x, y) -> map2 (map_trms_f ~f) b _And x y
   | Or (x, y) -> map2 (map_trms_f ~f) b _Or x y
   | Iff (x, y) -> map2 (map_trms_f ~f) b _Iff x y
-  | Xor (x, y) -> map2 (map_trms_f ~f) b _Xor x y
   | Cond {cnd; pos; neg} -> map3 (map_trms_f ~f) b _Cond cnd pos neg
   | Lit (p, xs) -> mapN f b (_Lit p) xs
 
@@ -944,7 +923,7 @@ module Formula = struct
   let or_ = _Or
   let orN = function [] -> ff | b :: bs -> List.fold ~init:b ~f:or_ bs
   let iff = _Iff
-  let xor = _Xor
+  let xor p q = _Not (_Iff p q)
   let cond ~cnd ~pos ~neg = _Cond cnd pos neg
   let not_ = _Not
 
@@ -982,7 +961,6 @@ module Formula = struct
     | And (x, y) -> map2 (map_terms ~f) b _And x y
     | Or (x, y) -> map2 (map_terms ~f) b _Or x y
     | Iff (x, y) -> map2 (map_terms ~f) b _Iff x y
-    | Xor (x, y) -> map2 (map_terms ~f) b _Xor x y
     | Cond {cnd; pos; neg} -> map3 (map_terms ~f) b _Cond cnd pos neg
     | Lit (p, xs) -> lift_mapN f b (_Lit p) xs
 
@@ -1008,7 +986,7 @@ module Formula = struct
    fun ~meet1 ~join1 ~top ~bot fml ->
     let rec add_conjunct (cjn, splits) fml =
       match fml with
-      | Tt | Eq _ | Eq0 _ | Gt0 _ | Iff _ | Xor _ | Lit _ | Not _ ->
+      | Tt | Eq _ | Eq0 _ | Gt0 _ | Iff _ | Lit _ | Not _ ->
           (meet1 fml cjn, splits)
       | And (p, q) -> add_conjunct (add_conjunct (cjn, splits) p) q
       | Or (p, q) -> (cjn, [p; q] :: splits)
@@ -1088,7 +1066,6 @@ let rec f_to_ses : fml -> Ses.Term.t = function
   | And (p, q) -> Ses.Term.and_ (f_to_ses p) (f_to_ses q)
   | Or (p, q) -> Ses.Term.or_ (f_to_ses p) (f_to_ses q)
   | Iff (p, q) -> Ses.Term.eq (f_to_ses p) (f_to_ses q)
-  | Xor (p, q) -> Ses.Term.dq (f_to_ses p) (f_to_ses q)
   | Cond {cnd; pos; neg} ->
       Ses.Term.conditional ~cnd:(f_to_ses cnd) ~thn:(f_to_ses pos)
         ~els:(f_to_ses neg)