[sledge] Support Equality.solve generating fresh variables

Reviewed By: ngorogiannis

Differential Revision: D19286633

fbshipit-source-id: 41ba53d65

sledge/src/symbheap/equality.ml

@@ -142,10 +142,18 @@ let rec is_constant e =
       Qset.for_all ~f:(fun arg _ -> is_constant arg) args
   | Label _ | Float _ | Integer _ -> true
 
-let solve _ e f =
+let solve ~us ~xs e f =
   [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp e Term.pp f]
   ;
   let rec solve_ e f s =
+    let extend ~trm ~rep (us, xs, s) =
+      Some (us, xs, Subst.compose1 ~key:trm ~data:rep s)
+    in
+    let fresh name (us, xs, s) =
+      let x, us = Var.fresh name ~wrt:us in
+      let xs = Set.add xs x in
+      (Term.var x, (us, xs, s))
+    in
     let solve_uninterp e f =
       match ((e : Term.t), (f : Term.t)) with
       | Integer {data= m}, Integer {data= n} when not (Z.equal m n) -> None
@@ -153,13 +161,13 @@ let solve _ e f =
         match (is_constant e, is_constant f) with
         (* orient equation to discretionarily prefer term that is constant
            or compares smaller as class representative *)
-        | true, false -> Some (Subst.compose1 ~key:f ~data:e s)
-        | false, true -> Some (Subst.compose1 ~key:e ~data:f s)
+        | true, false -> extend ~trm:f ~rep:e s
+        | false, true -> extend ~trm:e ~rep:f s
         | _ ->
-            let key, data =
+            let trm, rep =
               if Term.compare e f > 0 then (e, f) else (f, e)
             in
-            Some (Subst.compose1 ~key ~data s) )
+            extend ~trm ~rep s )
     in
     let concat_size args =
       Vector.fold_until args ~init:Term.zero
@@ -173,7 +181,7 @@ let solve _ e f =
     | (Add _ | Mul _ | Integer _), _ | _, (Add _ | Mul _ | Integer _) -> (
         let e_f = Term.sub e f in
         match Term.solve_zero_eq e_f with
-        | Some (key, data) -> Some (Subst.compose1 ~key ~data s)
+        | Some (trm, rep) -> extend ~trm ~rep s
         | None -> solve_uninterp e_f Term.zero )
     | ApN (Concat, ms), ApN (Concat, ns) -> (
       match (concat_size ms, concat_size ns) with
@@ -186,16 +194,20 @@ let solve _ e f =
       | _ -> solve_uninterp e f )
     | _ -> solve_uninterp e f
   in
-  solve_ e f Subst.empty
+  (solve_ e f (us, xs, Subst.empty) >>| fun (_, xs, s) -> (xs, s))
   |>
   [%Trace.retn fun {pf} ->
-    function Some s -> pf "%a" Subst.pp s | None -> pf "false"]
+    function
+    | Some (xs, s) -> pf "%a%a" Var.Set.pp_xs xs Subst.pp s
+    | None -> pf "false"]
 
 (** Equality Relations *)
 
 (** see also [invariant] *)
 type t =
-  { sat: bool  (** [false] only if constraints are inconsistent *)
+  { xs: Var.Set.t
+        (** existential variables that did not appear in input equations *)
+  ; sat: bool  (** [false] only if constraints are inconsistent *)
   ; rep: Subst.t
         (** functional set of oriented equations: map [a] to [a'],
             indicating that [a = a'] holds, and that [a'] is the
@@ -274,7 +286,8 @@ let invariant r =
 
 (** Core operations *)
 
-let true_ = {sat= true; rep= Subst.empty} |> check invariant
+let true_ =
+  {xs= Var.Set.empty; sat= true; rep= Subst.empty} |> check invariant
 
 (** terms are congruent if equal after normalizing subterms *)
 let congruent r a b =
@@ -317,8 +330,9 @@ let extend a r = extend a r |> check invariant
 let merge us a b r =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]
   ;
-  ( match solve us a b with
-  | Some s -> {r with rep= Subst.compose r.rep s}
+  ( match solve ~us ~xs:r.xs a b with
+  | Some (xs, s) ->
+      {r with xs= Set.union r.xs xs; rep= Subst.compose r.rep s}
   | None -> {r with sat= false} )
   |>
   [%Trace.retn fun {pf} r' ->
@@ -354,22 +368,18 @@ let close us r =
     pf "%a" pp_diff (r, r') ;
     invariant r']
 
-(** Exposed interface *)
-
 let and_eq us a b r =
-  [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp a Term.pp b pp r]
-  ;
-  ( if not r.sat then r
+  if not r.sat then r
   else
     let a' = canon r a in
     let b' = canon r b in
     let r = extend a' r in
     let r = extend b' r in
-    if Term.equal a' b' then r else close us (merge us a' b' r) )
-  |>
-  [%Trace.retn fun {pf} r' ->
-    pf "%a" pp_diff (r, r') ;
-    invariant r']
+    if Term.equal a' b' then r else close us (merge us a' b' r)
+
+let extract_xs r = (r.xs, {r with xs= Var.Set.empty})
+
+(** Exposed interface *)
 
 let is_true {sat; rep} =
   sat && Subst.for_alli rep ~f:(fun ~key:a ~data:a' -> Term.equal a a')
@@ -401,13 +411,15 @@ let difference r a b =
     function Some d -> pf "%a" Z.pp_print d | None -> pf ""]
 
 let and_ us r s =
-  if not r.sat then r
+  ( if not r.sat then r
   else if not s.sat then s
   else
     let s, r =
       if Subst.length s.rep <= Subst.length r.rep then (s, r) else (r, s)
     in
     Subst.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> and_eq us e e' r)
+  )
+  |> extract_xs
 
 let or_ us r s =
   [%Trace.call fun {pf} -> pf "@[<hv 1>   %a@ @<2>∨ %a@]" pp r pp s]
@@ -429,8 +441,18 @@ let or_ us r s =
     let rs = merge_mems rs r s in
     let rs = merge_mems rs s r in
     rs )
+  |> extract_xs
+  |>
+  [%Trace.retn fun {pf} (_, r) -> pf "%a" pp r]
+
+let and_eq us a b r =
+  [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp a Term.pp b pp r]
+  ;
+  and_eq us a b r |> extract_xs
   |>
-  [%Trace.retn fun {pf} -> pf "%a" pp]
+  [%Trace.retn fun {pf} (_, r') ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
 
 let rename r sub =
   [%Trace.call fun {pf} -> pf "%a" pp r]

sledge/src/symbheap/equality.mli

@@ -20,13 +20,13 @@ include Invariant.S with type t := t
 val true_ : t
 (** The diagonal relation, which only equates each term with itself. *)
 
-val and_eq : Var.Set.t -> Term.t -> Term.t -> t -> t
+val and_eq : Var.Set.t -> Term.t -> Term.t -> t -> Var.Set.t * t
 (** Conjoin an equation to a relation. *)
 
-val and_ : Var.Set.t -> t -> t -> t
+val and_ : Var.Set.t -> t -> t -> Var.Set.t * t
 (** Conjunction. *)
 
-val or_ : Var.Set.t -> t -> t -> t
+val or_ : Var.Set.t -> t -> t -> Var.Set.t * t
 (** Disjunction. *)
 
 val rename : t -> Var.Subst.t -> t

sledge/src/symbheap/equality_test.ml

@@ -36,10 +36,16 @@ let%test_module _ =
     let x = Term.var x_
     let y = Term.var y_
     let z = Term.var z_
-    let and_eq = and_eq wrt
-    let and_ = and_ wrt
-    let or_ = or_ wrt
-    let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r)
+
+    let of_eqs l =
+      List.fold ~init:(wrt, true_)
+        ~f:(fun (us, r) (a, b) -> and_eq us a b r)
+        l
+      |> snd
+
+    let and_eq a b r = and_eq wrt a b r |> snd
+    let and_ r s = and_ wrt r s |> snd
+    let or_ r s = or_ wrt r s |> snd
     let f1 = of_eqs [(!0, !1)]
 
     let%test _ = is_false f1

sledge/src/symbheap/sh.ml

@@ -350,6 +350,19 @@ let bind_exists q ~wrt =
   |>
   [%Trace.retn fun {pf} (_, q') -> pf "%a" pp q']
 
+let exists_fresh xs q =
+  [%Trace.call fun {pf} ->
+    pf "{@[%a@]}@ %a" Var.Set.pp xs pp q ;
+    assert (
+      Set.disjoint xs q.us
+      || fail "Sh.exists_fresh xs ∩ q.us: %a" Var.Set.pp
+           (Set.inter xs q.us) () )]
+  ;
+  ( if Set.is_empty xs then q
+  else {q with xs= Set.union q.xs xs} |> check invariant )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
+
 let exists xs q =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp xs pp q]
   ;
@@ -380,8 +393,9 @@ let and_cong cong q =
   [%Trace.call fun {pf} -> pf "%a@ %a" Equality.pp cong pp q]
   ;
   let q = extend_us (Equality.fv cong) q in
-  let cong = Equality.and_ q.us q.cong cong in
-  (if Equality.is_false cong then false_ q.us else {q with cong})
+  let xs, cong = Equality.and_ (Set.union q.us q.xs) q.cong cong in
+  ( if Equality.is_false cong then false_ q.us
+  else exists_fresh xs {q with cong} )
   |>
   [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]
 
@@ -406,9 +420,12 @@ let star q1 q2 =
       let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in
       let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
       assert (Set.equal us (Set.union us1 us2)) ;
-      let cong = Equality.and_ us c1 c2 in
+      let xs, cong =
+        Equality.and_ (Set.union us (Set.union xs1 xs2)) c1 c2
+      in
       if Equality.is_false cong then false_ us
       else
+        exists_fresh xs
           { us
           ; xs= Set.union xs1 xs2
           ; cong
@@ -462,8 +479,8 @@ let rec pure (e : Term.t) =
   ;
   let us = Term.fv e in
   let eq_false b =
-    let cong = Equality.and_eq us b Term.false_ Equality.true_ in
-    {emp with us; cong; pure= [e]}
+    let xs, cong = Equality.and_eq us b Term.false_ Equality.true_ in
+    exists_fresh xs {emp with us; cong; pure= [e]}
   in
   ( match e with
   | Integer {data} -> if Z.is_false data then false_ us else emp
@@ -477,9 +494,9 @@ let rec pure (e : Term.t) =
         (star (pure cnd) (pure thn))
         (star (pure (Term.not_ cnd)) (pure els))
   | Ap2 (Eq, e1, e2) ->
-      let cong = Equality.(and_eq us e1 e2 true_) in
+      let xs, cong = Equality.(and_eq us e1 e2 true_) in
       if Equality.is_false cong then false_ us
-      else {emp with us; cong; pure= [e]}
+      else exists_fresh xs {emp with us; cong; pure= [e]}
   | _ -> {emp with us; pure= [e]} )
   |>
   [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]