[sledge] Change: Use conjunction instead of list of terms for Sh.pure

Summary:
The list interpreted as a conjunction of individual terms in `Sh.pure`
is now redundant with `Term.And`. This patch removes the redundant
list.

Reviewed By: jvillard

Differential Revision: D22035852

fbshipit-source-id: 49c01a078

sledge/src/sh.ml

@@ -16,7 +16,7 @@ type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
   ; cong: Equality.t
-  ; pure: Term.t list
+  ; pure: Term.t
   ; heap: seg list
   ; djns: disjunction list }
 [@@deriving compare, equal, sexp]
@@ -31,7 +31,7 @@ let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
   ; cong= Equality.true_
-  ; pure= []
+  ; pure= Term.true_
   ; heap= []
   ; djns= [] }
 
@@ -55,22 +55,15 @@ let map_seg ~f h =
   else {loc; bas; len; siz; seq}
 
 let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
-  let exception Unsat in
+  let pure = f_trm pure in
-  try
+  if Term.is_false pure then false_ us
+  else
     let cong = f_cong cong in
-    let pure =
-      List.filter_map_endo pure ~f:(fun e ->
-          let e' = f_trm e in
-          if Term.is_false e' then raise Unsat
-          else if Term.is_true e' then None
-          else Some e' )
-    in
     let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in
     let djns = List.map_endo djns ~f:(List.map_endo ~f:f_sjn) in
     if cong == q.cong && pure == q.pure && heap == q.heap && djns == q.djns
     then q
     else {q with cong; pure; heap; djns}
-  with Unsat -> false_ us
 
 let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
   let f b s = f s b in
@@ -83,7 +76,7 @@ let fold_vars_stem ?ignore_cong {us= _; xs= _; cong; pure; heap; djns= _}
     ~init ~f =
   List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
   |> fun init ->
-  List.fold ~init pure ~f:(fun init -> Term.fold_vars ~f ~init)
+  Term.fold_vars ~f ~init pure
   |> fun init ->
   if Option.is_some ignore_cong then init
   else
@@ -227,17 +220,14 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
   if not first then Format.fprintf fs "  " ;
   Equality.ppx_classes_diff x fs (parent_cong, cong) ;
   let pure =
-    if Option.is_none var_strength then pure
+    if Option.is_none var_strength then [pure]
     else
-      List.filter_map pure ~f:(fun e ->
+      let pure' = Equality.normalize cong pure in
-          let e' = Equality.normalize cong e in
+      if Term.is_true pure' then [] else [pure']
-          if Term.is_true e' then None else Some e' )
   in
   List.pp
     ~pre:(if first then "@[  " else "@ @[@<2>∧ ")
-    "@ @<2>∧ " (Term.ppx x) fs
+    "@ @<2>∧ " (Term.ppx x) fs pure ~suf:"@]" ;
-    (List.dedup_and_sort ~compare:Term.compare pure)
-    ~suf:"@]" ;
   let first = first && List.is_empty pure in
   if List.is_empty heap then
     Format.fprintf fs
@@ -308,10 +298,10 @@ let rec invariant q =
     ( match djns with
     | [[]] ->
         assert (Equality.is_true cong) ;
-        assert (List.is_empty pure) ;
+        assert (Term.is_true pure) ;
         assert (List.is_empty heap)
     | _ -> assert (not (Equality.is_false cong)) ) ;
-    List.iter pure ~f:invariant_pure ;
+    invariant_pure pure ;
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
         List.iter djn ~f:(fun sjn ->
@@ -466,12 +456,12 @@ let star q1 q2 =
   ( match (q1, q2) with
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Var.Set.union q1.us q2.us)
-  | {us= _; xs= _; cong; pure= []; heap= []; djns= []}, _
+  | {us= _; xs= _; cong; pure; heap= []; djns= []}, _
-    when Equality.is_true cong ->
+    when Equality.is_true cong && Term.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
-  | _, {us= _; xs= _; cong; pure= []; heap= []; djns= []}
+  | _, {us= _; xs= _; cong; pure; heap= []; djns= []}
-    when Equality.is_true cong ->
+    when Equality.is_true cong && Term.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
@@ -490,7 +480,7 @@ let star q1 q2 =
           { us
           ; xs= Var.Set.union xs1 xs2
           ; cong
-          ; pure= List.append p1 p2
+          ; pure= Term.and_ p1 p2
           ; heap= List.append h1 h2
           ; djns= List.append d1 d2 } )
   |>
@@ -511,18 +501,18 @@ let or_ q1 q2 =
   | {djns= [[]]; _}, _ -> extend_us q1.us q2
   | _, {djns= [[]]; _} -> extend_us q2.us q1
   | ( ({djns= []; _} as q)
-    , ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d) )
+    , ({us= _; xs; cong= _; pure; heap= []; djns= [djn]} as d) )
-    when Var.Set.is_empty xs ->
+    when Var.Set.is_empty xs && Term.is_true pure ->
       {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
-  | ( ({us= _; xs; cong= _; pure= []; heap= []; djns= [djn]} as d)
+  | ( ({us= _; xs; cong= _; pure; heap= []; djns= [djn]} as d)
     , ({djns= []; _} as q) )
-    when Var.Set.is_empty xs ->
+    when Var.Set.is_empty xs && Term.is_true pure ->
       {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
   | _ ->
       { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
       ; cong= Equality.true_
-      ; pure= []
+      ; pure= Term.true_
       ; heap= []
       ; djns= [[q1; q2]] } )
   |>
@@ -543,7 +533,7 @@ let pure (e : Term.t) =
       let us = Term.fv b in
       let xs, cong = Equality.(and_term us b true_) in
       if Equality.is_false cong then false_ us
-      else or_ q (exists_fresh xs {emp with us; cong; pure= [b]}) )
+      else or_ q (exists_fresh xs {emp with us; cong; pure= b}) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
@@ -596,14 +586,13 @@ let filter_heap ~f q =
 (** Query *)
 
 let is_emp = function
-  | {us= _; xs= _; cong= _; pure= []; heap= []; djns= []} -> true
+  | {us= _; xs= _; cong= _; pure; heap= []; djns= []} -> Term.is_true pure
   | _ -> false
 
 let is_false = function
   | {djns= [[]]; _} -> true
   | {cong; pure; heap; _} ->
-      List.exists pure ~f:(fun b ->
+      Term.is_false (Equality.normalize cong pure)
-          Term.is_false (Equality.normalize cong b) )
       || List.exists heap ~f:(fun seg ->
              Equality.entails_eq cong seg.loc Term.zero )
 

sledge/src/sh.mli

@@ -16,7 +16,7 @@ type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
   ; xs: Var.Set.t  (** existentially-bound variables *)
   ; cong: Equality.t  (** congruence induced by rest of formula *)
-  ; pure: Term.t list  (** conjunction of pure boolean constraints *)
+  ; pure: Term.t  (** pure boolean constraints *)
   ; heap: seg list  (** star-conjunction of segment atomic formulas *)
   ; djns: disjunction list  (** star-conjunction of disjunctions *) }
 
@@ -69,7 +69,7 @@ val and_subst : Equality.Subst.t -> t -> t
 
 (** Update *)
 
-val with_pure : Term.t list -> t -> t
+val with_pure : Term.t -> t -> t
 (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
     [pure] are defined in the same vocabulary. Note that [cong] is not
     weakened, so if [pure] and [q.pure] do not induce the same congruence,

sledge/src/sh_test.ml

@@ -82,7 +82,7 @@ let%test_module _ =
           )
 
         ( (∃ %x_6, %x_7 .   2 = %x_7 ∧ (%x_7 = 2) ∧ emp)
-        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ (%x_6 = 1) ∧ (%y_7 = 1) ∧ emp)
+        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) && (%y_7 = 1)) ∧ emp)
         ∨ (  0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
 
@@ -107,7 +107,10 @@ let%test_module _ =
           )
 
         ( (∃ %x_6, %x_8, %x_9 .   2 = %x_9 ∧ (%x_9 = 2) ∧ emp)
-        ∨ (∃ %x_6, %x_8 .   1 = %y_7 = %x_8 ∧ (%y_7 = 1) ∧ (%x_8 = 1) ∧ emp)
+        ∨ (∃ %x_6, %x_8 .
+             1 = %y_7 = %x_8
+           ∧ ((%y_7 = 1) && (%x_8 = 1))
+           ∧ emp)
         ∨ (∃ %x_6 .   0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
 
@@ -176,7 +179,7 @@ let%test_module _ =
              ∧ emp)
           )
 
-          ( (  emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
+          -1 ∧ emp * ( (  -1 ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
 
           ( (  emp) ∨ (  (%x_6 ≠ 0) ∧ emp) ) |}]
   end )

sledge/src/solver.ml

@@ -154,7 +154,7 @@ let excise_exists goal =
     let solutions_for_xs =
       let xs =
         Var.Set.diff goal.xs
-          (Sh.fv ~ignore_cong:() (Sh.with_pure [] goal.sub))
+          (Sh.fv ~ignore_cong:() (Sh.with_pure Term.true_ goal.sub))
       in
       Equality.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong
     in
@@ -179,21 +179,11 @@ let excise_exists goal =
           let min = Sh.and_subst witnesses goal.min in
           goal |> with_ ~us ~min ~xs ~pgs:true )
 
-let excise_term ({min} as goal) pure term =
+let excise_pure ({min; sub} as goal) =
-  let term' = Equality.normalize min.cong term in
-  if Term.is_false term' then None
-  else if Term.is_true term' then (
-    excise (fun {pf} -> pf "excise_pure %a" Term.pp term) ;
-    Some (goal |> with_ ~pgs:true, pure) )
-  else Some (goal, term' :: pure)
-
-let excise_pure ({sub} as goal) =
   trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
-  let+ goal, pure =
+  let pure' = Equality.normalize min.cong sub.pure in
-    List.fold_option sub.pure ~init:(goal, []) ~f:(fun (goal, pure) term ->
+  if Term.is_false pure' then None
-        excise_term goal pure term )
+  else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub))
-  in
-  goal |> with_ ~sub:(Sh.with_pure pure sub)
 
 (*   [k; o)
  * ⊢ [l; n)