[sledge] Fix: Replace Formula.disjuncts with DNF in Sh.pure

Summary: Formula.disjuncts was a quickly written approximation of DNF.

Reviewed By: ngorogiannis

Differential Revision: D23459513

fbshipit-source-id: 79fd60a7b

sledge/src/fol.ml

@@ -1198,15 +1198,32 @@ module Formula = struct
 
   let rename s e = map_vars ~f:(Var.Subst.apply s) e
 
-  let disjuncts p =
-    let rec disjuncts_ p ds =
-      match p with
-      | Or (a, b) -> disjuncts_ a (disjuncts_ b ds)
+  let fold_dnf :
+         meet1:('literal -> 'conjunction -> 'conjunction)
+      -> join1:('conjunction -> 'disjunction -> 'disjunction)
+      -> top:'conjunction
+      -> bot:'disjunction
+      -> 'formula
+      -> 'disjunction =
+   fun ~meet1 ~join1 ~top ~bot fml ->
+    let rec add_conjunct (cjn, splits) fml =
+      match fml with
+      | Tt | Ff | Eq _ | Dq _ | Eq0 _ | Dq0 _ | Gt0 _ | Ge0 _ | Lt0 _
+       |Le0 _ | Iff _ | Xor _ | UPosLit _ | UNegLit _ ->
+          (meet1 fml cjn, splits)
+      | And (p, q) -> add_conjunct (add_conjunct (cjn, splits) p) q
+      | Or (p, q) -> (cjn, [p; q] :: splits)
       | Cond {cnd; pos; neg} ->
-          disjuncts_ (and_ cnd pos) (disjuncts_ (and_ (not_ cnd) neg) ds)
-      | d -> d :: ds
+          (cjn, [and_ cnd pos; and_ (not_ cnd) neg] :: splits)
     in
-    disjuncts_ p []
+    let rec add_disjunct (cjn, splits) djn fml =
+      let cjn, splits = add_conjunct (cjn, splits) fml in
+      match splits with
+      | split :: splits ->
+          List.fold ~f:(add_disjunct (cjn, splits)) ~init:djn split
+      | [] -> join1 cjn djn
+    in
+    add_disjunct (top, []) bot fml
 end
 
 (*
@@ -1541,6 +1558,16 @@ module Context = struct
     let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
     (vs_of_ses vs', z)
 
+  let dnf f =
+    let meet1 a (vs, p, x) =
+      let vs, x = add vs a x in
+      (vs, Formula.and_ p a, x)
+    in
+    let join1 = Iter.cons in
+    let top = (Var.Set.empty, Formula.tt, empty) in
+    let bot = Iter.empty in
+    Formula.fold_dnf ~meet1 ~join1 ~top ~bot f
+
   let rename x sub = Ses.Equality.rename x (v_map_ses (Var.Subst.apply sub))
 
   (* Substs *)

sledge/src/fol.mli

@@ -181,7 +181,6 @@ and Formula : sig
     init:'a -> t -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
 
   val rename : Var.Subst.t -> t -> t
-  val disjuncts : t -> t list
 end
 
 (** Sets of assumptions, interpreted as conjunction, plus reasoning about
@@ -212,6 +211,9 @@ module Context : sig
   (** Intersect contexts of assumptions. Possibly weaker than logical
       disjunction. *)
 
+  val dnf : Formula.t -> (Var.Set.t * Formula.t * t) iter
+  (** Disjunctive-normal form expansion. *)
+
   val rename : t -> Var.Subst.t -> t
   (** Apply a renaming substitution to the context. *)
 

sledge/src/sh.ml

@@ -522,12 +522,11 @@ let orN = function
 let pure (p : Formula.t) =
   [%Trace.call fun {pf} -> pf "%a" Formula.pp p]
   ;
-  List.fold (Formula.disjuncts p) ~init:(false_ Var.Set.empty)
-    ~f:(fun q p ->
-      let us = Formula.fv p in
-      let xs, ctx = Context.add us p Context.empty in
+  Iter.fold (Context.dnf p) ~init:(false_ Var.Set.empty)
+    ~f:(fun q (xs, pure, ctx) ->
+      let us = Formula.fv pure in
       if Context.is_unsat ctx then extend_us us q
-      else or_ q (exists_fresh xs {emp with us; ctx; pure= p}) )
+      else or_ q (exists_fresh xs {emp with us; ctx; pure}) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;

sledge/src/test/fol_test.ml

@@ -498,4 +498,25 @@ let%test_module _ =
            rep= [[%x_5 ↦ 0]; [%y_6 ↦ 0]; [%z_7 ↦ 0]; [-1 ↦ ]; [0 ↦ ]]} |}]
 
     let%test _ = implies_eq r19 z !0
+
+    let%expect_test _ =
+      let f =
+        Formula.(
+          andN
+            [ eq x y
+            ; cond ~cnd:(eq x !0) ~pos:(eq z !2) ~neg:(eq z !3)
+            ; or_ (eq w !4) (eq w !5) ])
+      in
+      printf Formula.pp f ;
+      printf Formula.pp
+        (Formula.orN (Iter.to_list (Iter.map ~f:snd3 (Context.dnf f)))) ;
+      [%expect
+        {|
+        (((%x_5 = %y_6) ∧ ((0 = %x_5) ? (%z_7 = 2) : (%z_7 = 3)))
+          ∧ ((%w_4 = 4) ∨ (%w_4 = 5)))
+
+        (((((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3))
+            ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 5)) ∧ (0 = %x_5)) ∧ (%z_7 = 2)))
+           ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 ≠ %x_5)) ∧ (%z_7 = 3)))
+          ∨ ((((%x_5 = %y_6) ∧ (%w_4 = 4)) ∧ (0 = %x_5)) ∧ (%z_7 = 2))) |}]
   end )

sledge/src/test/solver_test.ml

@@ -239,27 +239,27 @@ let%test_module _ =
         ( infer_frame:
             %l_6
               -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
-          * ( (  2 = %n_9 ∧ emp)
-            ∨ (  0 = %n_9 ∧ emp)
+          * ( (  0 = %n_9 ∧ emp)
+            ∨ (  2 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
             )
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame:
-            ( (  %a_1 = %a_2
-               ∧ 2 = %n_9
+            ( (  %a_3 = _
+               ∧ 0 = %n_9
                ∧ 16 = %m_8
-               ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
+               ∧ emp)
             ∨ (  %a_3 = _
                ∧ 1 = %n_9
                ∧ 16 = %m_8
                ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ emp)
-            ∨ (  %a_3 = _
-               ∧ 0 = %n_9
+            ∨ (  %a_1 = %a_2
+               ∧ 2 = %n_9
                ∧ 16 = %m_8
-               ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1
-               ∧ emp)
+               ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ) |}]
 
     (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)