[sledge] Omit true from conjunction and false from disjunction

Summary:
It is redundant to include the unit of conjunction in conjunction
formulas (resp., disjunction).

Reviewed By: jvillard

Differential Revision: D24371084

fbshipit-source-id: 6edc151e5

sledge/src/propositional.ml

@@ -111,6 +111,7 @@ module Make (Trm : TERM) = struct
       join _And ff
         (function
           | And {pos; neg} -> (pos, neg)
+          | Tt -> (Fmls.empty, Fmls.empty)
           | Not p -> (Fmls.empty, Fmls.of_ p)
           | p -> (Fmls.of_ p, Fmls.empty) )
         p q
@@ -119,6 +120,7 @@ module Make (Trm : TERM) = struct
       join _Or tt
         (function
           | Or {pos; neg} -> (pos, neg)
+          | Not Tt -> (Fmls.empty, Fmls.empty)
           | Not p -> (Fmls.empty, Fmls.of_ p)
           | p -> (Fmls.of_ p, Fmls.empty) )
         p q

sledge/src/test/fol_test.ml

@@ -515,10 +515,10 @@ let%test_module _ =
         ((%x_5 = %y_6) ∧ ((%w_4 = 4) ∨ (%w_4 = 5))
           ∧ ((0 = %x_5) ? (%z_7 = 2) : (%z_7 = 3)))
 
-        ((tt ∧ (%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5))
-          ∨ (tt ∧ (%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))
-          ∨ (tt ∧ (%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5))
-          ∨ (tt ∧ (%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))) |}]
+        (((%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5))
+          ∨ ((%w_4 = 4) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))
+          ∨ ((%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 2) ∧ (0 = %x_5))
+          ∨ ((%w_4 = 5) ∧ (%x_5 = %y_6) ∧ (%z_7 = 3) ∧ (0 ≠ %x_5))) |}]
 
     let%test "unsigned boolean overflow" =
       Formula.equal Formula.tt

sledge/src/test/sh_test.ml

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