[sledge] Revise Sh.dnf to handle nested existentials

Summary:
The dnf implementation dates to before nested existentials were
added. Updating it was overlooked, and it is just wrong.

Reviewed By: ngorogiannis

Differential Revision: D14481988

fbshipit-source-id: 9bba570f0

sledge/src/llair/exp_test.mli

@@ -0,0 +1,6 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)

sledge/src/symbheap/equality_test.mli

@@ -0,0 +1,6 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)

sledge/src/symbheap/sh.ml

@@ -311,6 +311,11 @@ let star q1 q2 =
     invariant q ;
     assert (Set.equal q.us (Set.union q1.us q2.us))]
 
+let stars = function
+  | [] -> emp
+  | [q] -> q
+  | q :: qs -> List.fold ~f:star ~init:q qs
+
 let or_ q1 q2 =
   [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2]
   ;
@@ -394,36 +399,32 @@ let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   if heap == q.heap && djns == q.djns then q
   else {us; xs; cong; pure; heap; djns} |> check invariant
 
-let fold_disjunctions sjn ~init ~f = List.fold sjn.djns ~init ~f
+let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
-let fold_disjuncts djn ~init ~f = List.fold djn ~init ~f
+  let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
-
+    let ys, sjn = bind_exists sjn ~wrt:xs in
-let fold_dnf ~conj ~disj sjn conjuncts disjuncts =
+    let xs = Set.union ys xs in
-  let rec add_disjunct pending_splits sjn (conjuncts, disjuncts) =
+    let djns = sjn.djns in
+    let sjn = {sjn with djns= []} in
     split_case
-      (fold_disjunctions sjn ~init:pending_splits
+      (List.rev_append djns pending_splits)
-         ~f:(fun pending_splits split -> split :: pending_splits ))
+      (xs, conj sjn conjuncts)
-      (conj {sjn with djns= []} conjuncts, disjuncts)
+      disjuncts
-  and split_case pending_splits (conjuncts, disjuncts) =
+  and split_case pending_splits (xs, conjuncts) disjuncts =
     match pending_splits with
     | split :: pending_splits ->
-        fold_disjuncts split ~init:disjuncts ~f:(fun disjuncts sjn ->
+        List.fold split ~init:disjuncts ~f:(fun disjuncts sjn ->
-            add_disjunct pending_splits sjn (conjuncts, disjuncts) )
+            add_disjunct pending_splits sjn (xs, conjuncts) disjuncts )
-    | [] -> disj conjuncts disjuncts
+    | [] -> disj (xs, conjuncts) disjuncts
   in
-  add_disjunct [] sjn (conjuncts, disjuncts)
+  add_disjunct [] sjn (xs, conjuncts) disjuncts
 
 let dnf q =
   [%Trace.call fun {pf} -> pf "%a" pp q]
   ;
-  let conj sjn conjuncts =
+  let conj sjn conjuncts = sjn :: conjuncts in
-    assert (List.is_empty sjn.djns) ;
+  let disj (xs, conjuncts) disjuncts =
-    assert (List.is_empty conjuncts.djns) ;
+    exists xs (stars conjuncts) :: disjuncts
-    star conjuncts sjn
-  in
-  let disj conjuncts disjuncts =
-    assert (match conjuncts.djns with [] | [[]] -> true | _ -> false) ;
-    conjuncts :: disjuncts
   in
-  fold_dnf ~conj ~disj q emp []
+  fold_dnf ~conj ~disj q (Var.Set.empty, []) []
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp_djn]

sledge/src/symbheap/sh.mli

@@ -112,9 +112,9 @@ val pure_approx : t -> t
 
 val fold_dnf :
      conj:(starjunction -> 'conjuncts -> 'conjuncts)
-  -> disj:('conjuncts -> 'disjuncts -> 'disjuncts)
+  -> disj:(Var.Set.t * 'conjuncts -> 'disjuncts -> 'disjuncts)
   -> t
-  -> 'conjuncts
+  -> Var.Set.t * 'conjuncts
   -> 'disjuncts
   -> 'disjuncts
 (** Enumerate the cubes and clauses of a disjunctive-normal form expansion. *)

sledge/src/symbheap/sh_test.ml

@@ -0,0 +1,92 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+let%test_module _ =
+  ( module struct
+    (* let () = Trace.init ~margin:68 ~config:all () *)
+
+    let () = Trace.init ~margin:68 ~config:none ()
+    let pp = Format.printf "@\n%a@." Sh.pp
+    let pp_djn = Format.printf "@\n%a@." Sh.pp_djn
+    let ( ~$ ) = Var.Set.of_list
+    let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz
+    let ( = ) = Exp.eq
+    let wrt = Var.Set.empty
+    let x_, wrt = Var.fresh "x" ~wrt
+    let y_, _ = Var.fresh "y" ~wrt
+    let x = Exp.var x_
+    let y = Exp.var y_
+
+    let%expect_test _ =
+      let p = Sh.(exists ~$[x_] (extend_us ~$[x_] emp)) in
+      let q = Sh.(pure (x = !0)) in
+      pp p ;
+      pp q ;
+      pp (Sh.star p q) ;
+      [%expect
+        {|
+        ∃ %x_1 . emp
+
+          0 = %x_1 ∧ emp
+
+          0 = %x_1 ∧ emp |}]
+
+    let%expect_test _ =
+      let q =
+        Sh.(
+          or_
+            (pure (x = !0))
+            (exists
+               ~$[x_]
+               (or_
+                  (and_ (x = !1) (pure (y = !1)))
+                  (exists ~$[x_] (pure (x = !2))))))
+      in
+      pp q ;
+      pp_djn (Sh.dnf q) ;
+      [%expect
+        {|
+        emp
+        * ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .emp
+             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          )
+
+        ( (∃ %x_1, %x_2 .   2 = %x_2 ∧ emp)
+        ∨ (∃ %x_1 .   1 = %x_1 = %y_2 ∧ emp)
+        ∨ (  0 = %x_1 ∧ emp)
+        ) |}]
+
+    let%expect_test _ =
+      let q =
+        Sh.(
+          exists
+            ~$[x_]
+            (or_
+               (pure (x = !0))
+               (exists
+                  ~$[x_]
+                  (or_
+                     (and_ (x = !1) (pure (y = !1)))
+                     (exists ~$[x_] (pure (x = !2)))))))
+      in
+      pp q ;
+      pp_djn (Sh.dnf q) ;
+      [%expect
+        {|
+        ∃ %x_1 .
+        emp
+        * ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .emp
+             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          )
+
+        ( (∃ %x_1, %x_3, %x_4 .   2 = %x_4 ∧ emp)
+        ∨ (∃ %x_1, %x_3 .   1 = %y_2 = %x_3 ∧ emp)
+        ∨ (∃ %x_1 .   0 = %x_1 ∧ emp)
+        ) |}]
+  end )

sledge/src/symbheap/sh_test.mli

@@ -0,0 +1,6 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)

sledge/src/symbheap/solver_test.mli

@@ -0,0 +1,6 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)