From a07c71352b7e4f084a354df80f74cde522dbb2f6 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 28 Jun 2021 03:34:19 -0700
Subject: [PATCH] [sledge] Add a distinct formula and use it to strengthen
 Sh.pure_approx

Reviewed By: ngorogiannis

Differential Revision: D28907805

fbshipit-source-id: b588e8964
---
 sledge/src/fol/context.ml            |  2 +-
 sledge/src/fol/exp.ml                |  2 ++
 sledge/src/fol/exp.mli               |  1 +
 sledge/src/fol/fml.ml                | 26 +++++++++++++++++++-------
 sledge/src/fol/fml.mli               |  2 ++
 sledge/src/fol/propositional.ml      |  5 ++++-
 sledge/src/fol/propositional_intf.ml |  2 ++
 sledge/src/sh.ml                     |  6 ++++--
 sledge/src/test/solver_test.ml       |  5 ++---
 9 files changed, 37 insertions(+), 14 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 1a00261e7..141297264 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -800,7 +800,7 @@ let rec add_ wrt b r =
   | And {pos; neg} -> Fml.fold_pos_neg ~f:(add_ wrt) ~pos ~neg r
   | Eq (d, e) -> and_eq ~wrt d e r
   | Eq0 e -> and_eq ~wrt Trm.zero e r
-  | Pos _ | Not _ | Or _ | Iff _ | Cond _ | Lit _ -> r
+  | Distinct _ | Pos _ | Not _ | Or _ | Iff _ | Cond _ | Lit _ -> r
 
 let add us b r =
   [%Trace.call fun {pf} -> pf "@ %a@ | %a" Fml.pp b pp r]
diff --git a/sledge/src/fol/exp.ml b/sledge/src/fol/exp.ml
index 6fc9c8118..821593d0e 100644
--- a/sledge/src/fol/exp.ml
+++ b/sledge/src/fol/exp.ml
@@ -341,6 +341,7 @@ module Formula = struct
 
   let eq = ap2f Fml.eq
   let dq a b = Fml.not_ (eq a b)
+  let distinct = apNf Fml.distinct
 
   (* arithmetic *)
 
@@ -391,6 +392,7 @@ module Formula = struct
     match b with
     | Tt -> b
     | Eq (x, y) -> lift_map2 f b Fml.eq x y
+    | Distinct xs -> lift_mapN f b Fml.distinct xs
     | Eq0 x -> lift_map1 f b Fml.eq0 x
     | Pos x -> lift_map1 f b Fml.pos x
     | Not x -> map1 (map_terms ~f) b Fml.not_ x
diff --git a/sledge/src/fol/exp.mli b/sledge/src/fol/exp.mli
index 4bfba9e70..1aa07149d 100644
--- a/sledge/src/fol/exp.mli
+++ b/sledge/src/fol/exp.mli
@@ -109,6 +109,7 @@ and Formula : sig
   (* equality *)
   val eq : Term.t -> Term.t -> t
   val dq : Term.t -> Term.t -> t
+  val distinct : Term.t array -> t
 
   (* arithmetic *)
   val eq0 : Term.t -> t
diff --git a/sledge/src/fol/fml.ml b/sledge/src/fol/fml.ml
index 76c9b8c6e..714903dc8 100644
--- a/sledge/src/fol/fml.ml
+++ b/sledge/src/fol/fml.ml
@@ -52,6 +52,7 @@ let ppx strength fs fml =
     | Not Tt -> pf "ff"
     | Eq (x, y) -> pp_binop pp_t x "=" pp_t y
     | Not (Eq (x, y)) -> pp_binop pp_t x "≠" pp_t y
+    | Distinct xs -> pf "(%a)" (Array.pp "@ ≠ " pp_t) xs
     | Eq0 x -> pp_arith "=" x
     | Not (Eq0 x) -> pp_arith "≠" x
     | Pos x -> pp_arith ">" x
@@ -86,16 +87,16 @@ let _Pos x =
   | Q q -> bool (Q.gt q Q.zero)
   | x -> _Pos x
 
+let sort_eq x y =
+  match Sign.of_int (Trm.compare x y) with
+  | Neg -> _Eq x y
+  | Zero -> tt
+  | Pos -> _Eq y x
+
 let _Eq x y =
   if x == Trm.zero then _Eq0 y
   else if y == Trm.zero then _Eq0 x
   else
-    let sort_eq x y =
-      match Sign.of_int (Trm.compare x y) with
-      | Neg -> _Eq x y
-      | Zero -> tt
-      | Pos -> _Eq y x
-    in
     match (x, y) with
     (* x = y ==> 0 = x - y when x = y is an arithmetic equality *)
     | (Z _ | Q _ | Arith _), _ | _, (Z _ | Q _ | Arith _) ->
@@ -144,7 +145,17 @@ let _Eq x y =
         _Eq (Trm.sized ~siz:(Trm.seq_size_exn a) ~seq:x) a
     | _ -> sort_eq x y
 
+let _Distinct xs =
+  match Array.length xs with
+  | 0 | 1 -> tt
+  | 2 -> _Not (sort_eq xs.(0) xs.(1))
+  | _ ->
+      Array.sort ~cmp:Trm.compare xs ;
+      if Array.contains_adjacent_duplicate ~eq:Trm.equal xs then ff
+      else _Distinct xs
+
 let eq = _Eq
+let distinct = _Distinct
 let eq0 = _Eq0
 let pos = _Pos
 let not_ = _Not
@@ -160,6 +171,7 @@ let rec map_trms b ~f =
   match b with
   | Tt -> b
   | Eq (x, y) -> map2 f b _Eq x y
+  | Distinct xs -> mapN f b _Distinct xs
   | Eq0 x -> map1 f b _Eq0 x
   | Pos x -> map1 f b _Pos x
   | Not x -> map1 (map_trms ~f) b _Not x
@@ -185,7 +197,7 @@ let iter_pos_neg ~pos ~neg ~f =
 let iter_dnf ~meet1 ~top fml ~f =
   let rec add_conjunct fml (cjn, splits) =
     match fml with
-    | Tt | Eq _ | Eq0 _ | Pos _ | Iff _ | Lit _ | Not _ ->
+    | Tt | Eq _ | Distinct _ | Eq0 _ | Pos _ | Iff _ | Lit _ | Not _ ->
         (meet1 fml cjn, splits)
     | And {pos; neg} -> fold_pos_neg ~f:add_conjunct ~pos ~neg (cjn, splits)
     | Or {pos; neg} -> (cjn, (pos, neg) :: splits)
diff --git a/sledge/src/fol/fml.mli b/sledge/src/fol/fml.mli
index e21d5b90c..c072edd26 100644
--- a/sledge/src/fol/fml.mli
+++ b/sledge/src/fol/fml.mli
@@ -14,6 +14,7 @@ type t = private
   | Tt
   (* equality *)
   | Eq of Trm.t * Trm.t
+  | Distinct of Trm.t array
   (* arithmetic *)
   | Eq0 of Trm.t  (** [Eq0(x)] iff x = 0 *)
   | Pos of Trm.t  (** [Pos(x)] iff x > 0 *)
@@ -45,6 +46,7 @@ val bool : bool -> t
 
 (* equality *)
 val eq : Trm.t -> Trm.t -> t
+val distinct : Trm.t array -> t
 
 (* arithmetic *)
 val eq0 : Trm.t -> t
diff --git a/sledge/src/fol/propositional.ml b/sledge/src/fol/propositional.ml
index 0510c8353..c0bd6c5be 100644
--- a/sledge/src/fol/propositional.ml
+++ b/sledge/src/fol/propositional.ml
@@ -19,6 +19,7 @@ struct
     type t =
       | Tt
       | Eq of Trm.t * Trm.t
+      | Distinct of Trm.t array
       | Eq0 of Trm.t
       | Pos of Trm.t
       | Not of t
@@ -82,7 +83,7 @@ struct
       | And {pos; neg} -> Or {pos= neg; neg= pos}
       | Or {pos; neg} -> And {pos= neg; neg= pos}
       | Cond {cnd; pos; neg} -> Cond {cnd; pos= _Not pos; neg= _Not neg}
-      | Tt | Eq _ | Eq0 _ | Pos _ | Lit _ | Iff _ -> Not p )
+      | Tt | Eq _ | Distinct _ | Eq0 _ | Pos _ | Lit _ | Iff _ -> Not p )
       |> check invariant
 
     let _Join cons unit zero ~pos ~neg =
@@ -238,6 +239,7 @@ struct
       |> check invariant
 
     let _Eq x y = Eq (x, y) |> check invariant
+    let _Distinct xs = Distinct xs |> check invariant
     let _Eq0 x = Eq0 x |> check invariant
     let _Pos x = Pos x |> check invariant
     let _Lit p xs = Lit (p, xs) |> check invariant
@@ -253,6 +255,7 @@ struct
       | Eq (x, y) ->
           f x ;
           f y
+      | Distinct xs -> Array.iter ~f xs
       | Eq0 x | Pos x -> f x
       | Not x -> iter_trms ~f x
       | And {pos; neg} | Or {pos; neg} ->
diff --git a/sledge/src/fol/propositional_intf.ml b/sledge/src/fol/propositional_intf.ml
index 819c0e0f5..b9e3f6be4 100644
--- a/sledge/src/fol/propositional_intf.ml
+++ b/sledge/src/fol/propositional_intf.ml
@@ -19,6 +19,7 @@ module type FORMULA = sig
     | Tt
     (* equality *)
     | Eq of trm * trm
+    | Distinct of trm array
     (* arithmetic *)
     | Eq0 of trm  (** [Eq0(x)] iff x = 0 *)
     | Pos of trm  (** [Pos(x)] iff x > 0 *)
@@ -34,6 +35,7 @@ module type FORMULA = sig
 
   val mk_Tt : unit -> t
   val _Eq : trm -> trm -> t
+  val _Distinct : trm array -> t
   val _Eq0 : trm -> t
   val _Pos : trm -> t
   val _Not : t -> t
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 8cd1ecdf6..dbfa495f8 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -639,8 +639,10 @@ let dnf q =
 (** first-order approximation of heap constraints *)
 let rec pure_approx q =
   Formula.andN
-    ( [q.pure]
-    |> List.fold q.heap ~f:(fun seg p -> Formula.dq0 seg.loc :: p)
+    ( [ q.pure
+      ; Formula.distinct
+          (Array.of_list
+             (Term.zero :: List.map ~f:(fun seg -> seg.loc) q.heap)) ]
     |> List.fold q.djns ~f:(fun djn p ->
            Formula.orN (List.map djn ~f:pure_approx) :: p ) )
 
diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml
index 1d6998769..189a15041 100644
--- a/sledge/src/test/solver_test.ml
+++ b/sledge/src/test/solver_test.ml
@@ -246,12 +246,11 @@ let%test_module _ =
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) Solver.infer_frame:
-            ( (  1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp)
-            ∨ (  %a_1 = %a_2
+            ( (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
                ∧ (16 + %l_6) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
-            ∨ (  0 = %n_9 ∧ 16 = %m_8 ∧ (⟨0,%a_2⟩^⟨16,%a_3⟩) = %a_1 ∧ emp)
+            ∨ (  1 = %n_9 ∧ 16 = %m_8 ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1 ∧ emp)
             ) |}]
 
     (* Incompleteness: equivalent to above but using ≤ instead of ∨ *)