From 200091fc787a244fd09aa649337ee4196757b0d5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 27 Jan 2020 08:19:30 -0800 Subject: [PATCH] [sledge] Add Equality.Subst.trim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Summary: ``` val trim : bound:Var.Set.t -> Var.Set.t -> t -> t (** [trim bound kills subst] is [subst] without mappings that mention [kills] or [bound ∩ fv x] for removed entries [x ↦ u] *) ``` To be used for existential witnessing and quantifier elimination. Reviewed By: ngorogiannis Differential Revision: D19282644 fbshipit-source-id: d981a1cb4 --- sledge/src/symbheap/equality.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index 6ddf3c6b4..2838d43ed 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -51,6 +51,7 @@ module Subst : sig val extend : Term.t -> t -> t option val map_entries : f:(Term.t -> Term.t) -> t -> t val to_alist : t -> (Term.t * Term.t) list + val trim : bound:Var.Set.t -> Var.Set.t -> t -> t end = struct type t = Term.t Term.Map.t [@@deriving compare, equal, sexp] @@ -111,6 +112,21 @@ end = struct if Term.equal key' key then if Term.equal data' data then s else Map.set s ~key ~data:data' else Map.remove s key |> Map.add_exn ~key:key' ~data:data' ) + + (** [trim bound kills subst] is [subst] without mappings that mention + [kills] or [bound ∩ fv x] for removed entries [x ↦ u] *) + let rec trim ~bound ks s = + let ks', s' = + Map.fold s ~init:(ks, s) ~f:(fun ~key ~data (ks, s) -> + let fv_key = Term.fv key in + let fv_data = Term.fv data in + if Set.disjoint ks (Set.union fv_key fv_data) then (ks, s) + else + let ks = Set.union ks (Set.inter bound fv_key) in + let s = Map.remove s key in + (ks, s) ) + in + if s' != s then trim ~bound ks' s' else s' end (** Theory Solver *)