[sledge] Add: Normalization of constant, equal and negated subterms/formulas

Summary:
Strengthen normalization performed by Term and Formula constructors to
eliminate literal 0 subterms and true or false subformulas, as well as
cases where subterms or subformulas are either equal or opposite.

This strengthens the ability of Context.implies to prove formulas that
involve embedding or projecting between terms and formulas, as the
added normalization sometimes reduces if-then-else formulas to
literals that are then directly provable.

Reviewed By: ngorogiannis

Differential Revision: D23459512

fbshipit-source-id: 6d4d90399

sledge/src/fol.ml

@@ -95,10 +95,21 @@ let equal_trm x y =
       Int.equal i j
   | _ -> equal_trm x y
 
+let zero = Z Z.zero
+let one = Z Z.one
 let _Neg x = Neg x
-let _Add x y = Add (x, y)
+
+let _Add x y =
+  match (x, y) with
+  | _, Q q when Q.sign q = 0 -> x
+  | Q q, _ when Q.sign q = 0 -> y
+  | _ -> Add (x, y)
+
 let _Sub x y = Sub (x, y)
-let _Mulq q x = Mulq (q, x)
+
+let _Mulq q x =
+  if Q.equal Q.one q then x else if Q.sign q = 0 then zero else Mulq (q, x)
+
 let _Splat x = Splat x
 let _Sized seq siz = Sized {seq; siz}
 let _Extract seq off len = Extract {seq; off; len}
@@ -108,8 +119,6 @@ let _Update rcd idx elt = Update {rcd; idx; elt}
 let _Tuple es = Tuple es
 let _Project ary idx tup = Project {ary; idx; tup}
 let _Apply f a = Apply (f, a)
-let zero = Z Z.zero
-let one = Z Z.one
 
 (*
  * (Uninterpreted) Predicate Symbols
@@ -161,6 +170,7 @@ module Fml : sig
   val _Ge0 : trm -> fml
   val _Lt0 : trm -> fml
   val _Le0 : trm -> fml
+  val _Not : fml -> fml
   val _And : fml -> fml -> fml
   val _Or : fml -> fml -> fml
   val _Iff : fml -> fml -> fml
@@ -197,34 +207,165 @@ end = struct
 
   let _Tt = Tt
   let _Ff = Ff
-  let _Eq x y = if equal_trm x y then Tt else Eq (x, y)
-  let _Dq x y = Dq (x, y)
-  let _Eq0 x = Eq0 x
 
-  let _Dq0 = function
+  type equal_or_separate = Equal | Separate | Unknown
+
+  let equal_or_separate d e : equal_or_separate =
+    match (d, e) with
+    | Z y, Z z -> if Z.equal y z then Equal else Separate
+    | Q q, Q r -> if Q.equal q r then Equal else Separate
+    | Z z, Q q | Q q, Z z ->
+        if Q.equal (Q.of_z z) q then Equal else Separate
+    | _ -> if equal_trm d e then Equal else Unknown
+
+  let _Eq0 x =
+    match equal_or_separate zero x with
+    (* 0 = 0 ==> tt *)
+    | Equal -> Tt
+    (* 0 = N ==> ff for N ≢ 0 *)
+    | Separate -> Ff
+    | Unknown -> Eq0 x
+
+  let _Dq0 x =
+    match equal_or_separate zero x with
     (* 0 ≠ 0 ==> ff *)
-    | Z _ as z when z == zero -> Ff
+    | Equal -> Ff
     (* 0 ≠ N ==> tt for N ≢ 0 *)
-    | Z _ -> Tt
+    | Separate -> Tt
-    | t -> Dq0 t
+    | Unknown -> Dq0 x
-
+
-  let _Gt0 x = Gt0 x
+  let _Eq x y =
-  let _Ge0 x = Ge0 x
+    if x == zero then _Eq0 y
-  let _Lt0 x = Lt0 x
+    else if y == zero then _Eq0 x
-  let _Le0 x = Le0 x
+    else
-  let _And p q = And (p, q)
+      match equal_or_separate x y with
-  let _Or p q = Or (p, q)
+      | Equal -> Tt
-  let _Iff p q = Iff (p, q)
+      | Separate -> Ff
-  let _Xor p q = Xor (p, q)
+      | Unknown -> Eq (x, y)
-
+
-  let _Cond cnd pos neg =
+  let _Dq x y =
-    match (pos, neg) with
+    if x == zero then _Dq0 y
-    (* (p ? tt : ff) ==> p *)
+    else if y == zero then _Dq0 x
-    | Tt, Ff -> cnd
+    else
-    | _ -> Cond {cnd; pos; neg}
+      match equal_or_separate x y with
+      | Equal -> Ff
+      | Separate -> Tt
+      | Unknown -> Dq (x, y)
+
+  let _Gt0 = function
+    | Z z -> if Z.gt z Z.zero then Tt else Ff
+    | Q q -> if Q.gt q Q.zero then Tt else Ff
+    | x -> Gt0 x
+
+  let _Ge0 = function
+    | Z z -> if Z.geq z Z.zero then Tt else Ff
+    | Q q -> if Q.geq q Q.zero then Tt else Ff
+    | x -> Ge0 x
+
+  let _Lt0 = function
+    | Z z -> if Z.lt z Z.zero then Tt else Ff
+    | Q q -> if Q.lt q Q.zero then Tt else Ff
+    | x -> Lt0 x
+
+  let _Le0 = function
+    | Z z -> if Z.leq z Z.zero then Tt else Ff
+    | Q q -> if Q.leq q Q.zero then Tt else Ff
+    | x -> Le0 x
 
   let _UPosLit p x = UPosLit (p, x)
   let _UNegLit p x = UNegLit (p, x)
+
+  type equal_or_opposite = Equal | Opposite | Unknown
+
+  let rec equal_or_opposite p q : equal_or_opposite =
+    if equal_fml p q then Equal
+    else if equal_fml p (_Not q) then Opposite
+    else Unknown
+
+  and _And p q =
+    match (p, q) with
+    | Tt, p | p, Tt -> p
+    | Ff, _ | _, Ff -> Ff
+    | _ -> (
+      match equal_or_opposite p q with
+      | Equal -> p
+      | Opposite -> Ff
+      | Unknown -> And (p, q) )
+
+  and _Or p q =
+    match (p, q) with
+    | Ff, p | p, Ff -> p
+    | Tt, _ | _, Tt -> Tt
+    | _ -> (
+      match equal_or_opposite p q with
+      | Equal -> p
+      | Opposite -> Tt
+      | Unknown -> Or (p, q) )
+
+  and _Iff p q =
+    match (p, q) with
+    | Tt, p | p, Tt -> p
+    | Ff, p | p, Ff -> _Not p
+    | _ -> (
+      match equal_or_opposite p q with
+      | Equal -> Tt
+      | Opposite -> Ff
+      | Unknown -> Iff (p, q) )
+
+  and _Xor p q =
+    match (p, q) with
+    | Tt, p | p, Tt -> _Not p
+    | Ff, p | p, Ff -> p
+    | _ -> (
+      match equal_or_opposite p q with
+      | Equal -> Ff
+      | Opposite -> Tt
+      | Unknown -> Xor (p, q) )
+
+  and _Not = function
+    | Tt -> _Ff
+    | Ff -> _Tt
+    | Eq (x, y) -> _Dq x y
+    | Dq (x, y) -> _Eq x y
+    | Eq0 x -> _Dq0 x
+    | Dq0 x -> _Eq0 x
+    | Gt0 x -> _Le0 x
+    | Ge0 x -> _Lt0 x
+    | Lt0 x -> _Ge0 x
+    | Le0 x -> _Gt0 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)
+    | UPosLit (p, x) -> _UNegLit p x
+    | UNegLit (p, x) -> _UPosLit p x
+
+  and _Cond cnd pos neg =
+    match (cnd, pos, neg) with
+    (* (tt ? p : n) ==> p *)
+    | Tt, _, _ -> pos
+    (* (ff ? p : n) ==> n *)
+    | Ff, _, _ -> neg
+    (* (c ? tt : ff) ==> c *)
+    | _, Tt, Ff -> cnd
+    (* (c ? ff : tt) ==> ¬c *)
+    | _, Ff, Tt -> _Not cnd
+    (* (c ? p : ff) ==> c ∧ p *)
+    | _, _, Ff -> _And cnd pos
+    (* (c ? ff : n) ==> ¬c ∧ n *)
+    | _, Ff, _ -> _And (_Not cnd) neg
+    (* (c ? tt : n) ==> c ∨ n *)
+    | _, Tt, _ -> _Or cnd neg
+    (* (c ? p : tt) ==> ¬c ∨ p *)
+    | _, _, Tt -> _Or (_Not cnd) pos
+    | _ -> (
+      match equal_or_opposite pos neg with
+      (* (c ? p : p) ==> c *)
+      | Equal -> cnd
+      (* (c : p : ¬p) ==> c <=> p *)
+      | Opposite -> _Iff cnd pos
+      | Unknown -> Cond {cnd; pos; neg} )
 end
 
 open Fml
@@ -1005,25 +1146,7 @@ module Formula = struct
   let iff = _Iff
   let xor = _Xor
   let cond ~cnd ~pos ~neg = _Cond cnd pos neg
-
+  let not_ = _Not
-  let rec not_ = function
-    | Tt -> _Ff
-    | Ff -> _Tt
-    | Eq (x, y) -> _Dq x y
-    | Dq (x, y) -> _Eq x y
-    | Eq0 x -> _Dq0 x
-    | Dq0 x -> _Eq0 x
-    | Gt0 x -> _Le0 x
-    | Ge0 x -> _Lt0 x
-    | Lt0 x -> _Ge0 x
-    | Le0 x -> _Gt0 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)
-    | UPosLit (p, x) -> _UNegLit p x
-    | UNegLit (p, x) -> _UPosLit p x
 
   (** Query *)
 

sledge/src/sh_test.ml

@@ -86,7 +86,7 @@ let%test_module _ =
     
         ( (∃ %x_6, %x_7 .   (%x_7 = 2) ∧ emp)
         ∨ (∃ %x_6 .   ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
-        ∨ (  (%x_6 = 0) ∧ emp)
+        ∨ (  (0 = %x_6) ∧ emp)
         ) |}]
 
     let%expect_test _ =
@@ -111,7 +111,7 @@ let%test_module _ =
     
         ( (∃ %x_6, %x_8, %x_9 .   (%x_9 = 2) ∧ emp)
         ∨ (∃ %x_6, %x_8 .   ((%x_8 = 1) ∧ (%y_7 = 1)) ∧ emp)
-        ∨ (∃ %x_6 .   (%x_6 = 0) ∧ emp)
+        ∨ (∃ %x_6 .   (0 = %x_6) ∧ emp)
         ) |}]
 
     let%expect_test _ =
@@ -146,7 +146,7 @@ let%test_module _ =
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp
     
-          ((%y_7^ = (-1 + %y_7)) ∧ tt) ∧ emp
+          (%y_7^ = (-1 + %y_7)) ∧ emp
 
           (-1 + %y_7) = %y_7^ ∧ emp |}]
 
@@ -169,15 +169,13 @@ let%test_module _ =
       [%expect
         {|
         ∃ %a_1, %c_3, %d_4, %e_5 .
-          ((⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ tt)
+          (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
         ∧ emp
-        * ( (  (%x_6 ≠ 0) ∧ emp)
+        * ( (  (0 ≠ %x_6) ∧ emp)
           ∨ (∃ %b_2 .   (⟨8,%a_1⟩ = (⟨4,%c_3⟩^⟨4,%b_2⟩)) ∧ emp)
           )
 
-          ((tt ∧ (tt ∧ tt)) ∧ tt)
+          tt ∧ emp * ( (  tt ∧ emp) ∨ (  (0 ≠ %x_6) ∧ emp) )
-        ∧ emp
-        * ( (  tt ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
 
-          ( (  emp) ∨ (  (%x_6 ≠ 0) ∧ emp) ) |}]
+          ( (  emp) ∨ (  (0 ≠ %x_6) ∧ emp) ) |}]
   end )

sledge/src/solver_test.ml

@@ -287,6 +287,6 @@ let%test_module _ =
       infer_frame minuend [m_] subtrahend ;
       [%expect
         {|
-        ( infer_frame:   emp \- ∃ %m_8 .   %a_1 = %m_8 ∧ (%a_1 ≠ 0) ∧ emp
+        ( infer_frame:   emp \- ∃ %m_8 .   %a_1 = %m_8 ∧ (0 ≠ %a_1) ∧ emp
         ) infer_frame: |}]
   end )