From a7b0d68574773af6b2ed79227786062cf2f0534f Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 27 Jan 2020 08:19:56 -0800 Subject: [PATCH] [sledge] Support Equality.solve generating fresh variables Reviewed By: ngorogiannis Differential Revision: D19286633 fbshipit-source-id: 41ba53d65 --- sledge/src/symbheap/equality.ml | 70 ++++++++++++++++++---------- sledge/src/symbheap/equality.mli | 6 +-- sledge/src/symbheap/equality_test.ml | 14 ++++-- sledge/src/symbheap/sh.ml | 43 +++++++++++------ 4 files changed, 89 insertions(+), 44 deletions(-) diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index 29df5cb56..b5961d73d 100644 --- a/sledge/src/symbheap/equality.ml +++ b/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 "@[ %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] diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli index aaa492167..a656d9e81 100644 --- a/sledge/src/symbheap/equality.mli +++ b/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 diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml index 26f48fbe3..e2763232f 100644 --- a/sledge/src/symbheap/equality_test.ml +++ b/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 diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index c55e84f7a..e70499e94 100644 --- a/sledge/src/symbheap/sh.ml +++ b/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,15 +420,18 @@ 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 - { us - ; xs= Set.union xs1 xs2 - ; cong - ; pure= List.append p1 p2 - ; heap= List.append h1 h2 - ; djns= List.append d1 d2 } ) + exists_fresh xs + { us + ; xs= Set.union xs1 xs2 + ; cong + ; pure= List.append p1 p2 + ; heap= List.append h1 h2 + ; djns= List.append d1 d2 } ) |> [%Trace.retn fun {pf} q -> pf "%a" pp q ; @@ -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]