From 1c37a0f1468f2c5c0a0defff4f0eeaaa4fad6e13 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Jan 2021 04:26:09 -0800 Subject: [PATCH] [sledge] Generalize Context.elim and make it more robust Summary: The current implementation of Context.elim crudely removes oriented equations from terms involving the given variables. This is easy to use in a way that violates the representation invariants of Context, as well as destroys completeness. This diff resolves this by making Context.elim remove the desired variables by rearranging the existing equality classes, in particular promoting a new representative term when the existing representative is to be removed. Also, since this basic approach is incomplete for interpreted terms, they are detected and not removed. As a result, the interface changes to return the set of variables that have been removed. Reviewed By: jvillard Differential Revision: D25756573 fbshipit-source-id: 0eead9281 --- sledge/nonstdlib/set.ml | 9 +++ sledge/nonstdlib/set_intf.ml | 4 ++ sledge/src/fol/context.ml | 105 +++++++++++++++++++++++++++++++++-- sledge/src/fol/context.mli | 9 ++- sledge/src/fol/trm.ml | 5 ++ sledge/src/fol/trm.mli | 6 ++ sledge/src/sh.ml | 31 ++++++----- 7 files changed, 147 insertions(+), 22 deletions(-) diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml index 51d4d72ca..c440fd000 100644 --- a/sledge/nonstdlib/set.ml +++ b/sledge/nonstdlib/set.ml @@ -96,6 +96,11 @@ end) : S with type elt = Elt.t = struct | l, true, r when is_empty l && is_empty r -> `One elt | _ -> `Many ) + let pop s = + match choose s with + | Some elt -> Some (elt, S.remove elt s) + | None -> None + let pop_exn s = let elt = choose_exn s in (elt, S.remove elt s) @@ -106,6 +111,10 @@ end) : S with type elt = Elt.t = struct let exists s ~f = S.exists f s let for_all s ~f = S.for_all f s let fold s z ~f = S.fold f s z + + let reduce xs ~f = + match pop xs with Some (x, xs) -> Some (fold ~f xs x) | None -> None + let to_iter = S.to_iter let of_iter = S.of_iter diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml index 772ef38b3..bebf75802 100644 --- a/sledge/nonstdlib/set_intf.ml +++ b/sledge/nonstdlib/set_intf.ml @@ -52,6 +52,9 @@ module type S = sig val only_elt : t -> elt option val classify : t -> [`Zero | `One of elt | `Many] + val pop : t -> (elt * t) option + (** Find and remove an unspecified element. [O(1)]. *) + val pop_exn : t -> elt * t (** Find and remove an unspecified element. [O(1)]. *) @@ -66,6 +69,7 @@ module type S = sig val exists : t -> f:(elt -> bool) -> bool val for_all : t -> f:(elt -> bool) -> bool val fold : t -> 's -> f:(elt -> 's -> 's) -> 's + val reduce : t -> f:(elt -> elt -> elt) -> elt option (** {1 Convert} *) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 9ff27ff80..a38cb5ec9 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -56,11 +56,14 @@ module Subst : sig val compose : t -> t -> t val compose1 : key:Trm.t -> data:Trm.t -> t -> t val extend : Trm.t -> t -> t option - val remove : Var.Set.t -> t -> t val map_entries : f:(Trm.t -> Trm.t) -> t -> t val to_iter : t -> (Trm.t * Trm.t) iter val fv : t -> Var.Set.t val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t + + (* direct representation manipulation *) + val add : key:Trm.t -> data:Trm.t -> t -> t + val remove : Trm.t -> t -> t end = struct type t = Trm.t Trm.Map.t [@@deriving compare, equal, sexp_of] @@ -139,10 +142,6 @@ end = struct | exception Found -> None | s -> Some s - (** remove entries for vars *) - let remove xs s = - Var.Set.fold ~f:(fun x -> Trm.Map.remove (Trm.var x)) xs s - (** map over a subst, applying [f] to both domain and range, requires that [f] is injective and for any set of terms [E], [f\[E\]] is disjoint from [E] *) @@ -200,6 +199,11 @@ end = struct if s' != s then partition_valid_ t' ks' s' else (t', ks', s') in partition_valid_ empty xs s + + (* direct representation manipulation *) + + let add = Trm.Map.add + let remove = Trm.Map.remove end (** Theory Solver *) @@ -1175,7 +1179,96 @@ let solve_for_vars vss r = else `Continue us_xs ) ~finish:(fun _ -> false) ) )] -let elim xs r = {r with rep= Subst.remove xs r.rep} +(* [elim] removes variables from a context by rearranging the existing + equality classes. Non-representative terms that contain a variable to + eliminate can be simply dropped. If a representative needs to be removed, + a new representative is chosen. This basic approach is insufficient if + interpreted terms are to be removed. For example, eliminating x from x + + 1 = y = z ∧ w = x by just preserving the existing classes between terms + that do not mention x would yield y = z. This would lose provability of + the equality w = y - 1. So variables with interpreted uses are not + eliminated. *) +let elim xs r = + [%trace] + ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs xs pp_raw r) + ~retn:(fun {pf} (ks, r') -> + pf "%a@ %a" Var.Set.pp_xs ks pp_raw r' ; + assert (Var.Set.subset ks ~of_:xs) ; + assert (Var.Set.disjoint ks (fv r')) ) + @@ fun () -> + (* add the uninterpreted uses of terms in delta to approx, and the + interpreted uses to interp *) + let rec add_uninterp_uses approx interp delta = + if not (Trm.Set.is_empty delta) then + let approx = Trm.Set.union approx delta in + let delta, interp = + Trm.Set.fold delta + (Trm.Set.empty, Trm.Set.empty) + ~f: + (fold_uses_of r ~f:(fun use (delta, interp) -> + if is_interpreted use then (delta, Trm.Set.add use interp) + else (Trm.Set.add use delta, interp) )) + in + add_uninterp_uses approx interp delta + else + (* remove the subterms of interpreted uses from approx *) + let rec remove_subtrms misses approx = + if not (Trm.Set.is_empty misses) then + let approx = Trm.Set.diff approx misses in + let misses = + Trm.Set.of_iter + (Iter.flat_map ~f:Trm.trms (Trm.Set.to_iter misses)) + in + remove_subtrms misses approx + else approx + in + remove_subtrms interp approx + in + (* compute terms in relation mentioning vars to eliminate *) + let kills = + add_uninterp_uses Trm.Set.empty Trm.Set.empty + (Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter xs))) + in + let ks = + Trm.Set.fold kills Var.Set.empty ~f:(fun kill ks -> + match Var.of_trm kill with Some k -> Var.Set.add k ks | None -> ks ) + in + (* compute classes including reps *) + let reps = + Subst.fold r.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps -> + Trm.Set.add rep reps ) + in + let clss = + Trm.Set.fold reps (classes r) ~f:(fun rep clss -> + Trm.Map.add_multi ~key:rep ~data:rep clss ) + in + (* trim classes to those that intersect kills *) + let clss = + Trm.Map.filter_mapi clss ~f:(fun ~key:_ ~data:cls -> + let cls = Trm.Set.of_list cls in + if Trm.Set.disjoint kills cls then None else Some cls ) + in + (* enumerate affected classes and update solution subst *) + let rep = + Trm.Map.fold clss r.rep ~f:(fun ~key:rep ~data:cls s -> + (* remove mappings for non-rep class elements to kill *) + let drop = Trm.Set.inter cls kills in + let s = Trm.Set.fold ~f:Subst.remove drop s in + if not (Trm.Set.mem rep kills) then s + else + (* if rep is to be removed, choose new one from the keepers *) + let keep = Trm.Set.diff cls drop in + match + Trm.Set.reduce keep ~f:(fun x y -> + if prefer x y < 0 then x else y ) + with + | Some rep' -> + (* add mappings from each keeper to the new representative *) + Trm.Set.fold keep s ~f:(fun elt s -> + Subst.add ~key:elt ~data:rep' s ) + | None -> s ) + in + (ks, {r with rep}) (* * Replay debugging diff --git a/sledge/src/fol/context.mli b/sledge/src/fol/context.mli index 3d245b44a..cf891ed80 100644 --- a/sledge/src/fol/context.mli +++ b/sledge/src/fol/context.mli @@ -108,9 +108,12 @@ val solve_for_vars : Var.Set.t list -> t -> Subst.t terms [e] with free variables contained in as short a prefix of [uss] as possible. *) -val elim : Var.Set.t -> t -> t -(** [elim ks x] is [x] weakened by removing oriented equations [k ↦ _] for - [k] in [ks]. *) +val elim : Var.Set.t -> t -> Var.Set.t * t +(** [elim vs x] is [(ks, y)] where [ks] is such that [vs ⊇ ks] and + [ks ∩ fv y = ∅] and [y] is such that [∃vs-ks. y] is equivalent to + [∃vs. x]. [elim] only removes terms from the existing representation, + without performing any additional solving. This means that if a variable + in [vs] occurs in an interpreted term in [x], it will not be eliminated. *) (**/**) diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml index f37fb603a..91bcdfd79 100644 --- a/sledge/src/fol/trm.ml +++ b/sledge/src/fol/trm.ml @@ -387,6 +387,11 @@ module T = struct type t = Trm.t [@@deriving compare, sexp] end +module Set = struct + include Set.Make (T) + include Provide_of_sexp (T) +end + module Map = struct include Map.Make (T) include Provide_of_sexp (T) diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli index eb76a33c2..571908ff1 100644 --- a/sledge/src/fol/trm.mli +++ b/sledge/src/fol/trm.mli @@ -37,6 +37,12 @@ end module Arith : Arithmetic.S with type var := Var.t with type trm := t with type t = arith +module Set : sig + include Set.S with type elt := t + + val t_of_sexp : Sexp.t -> t +end + module Map : sig include Map.S with type key := t diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 2afc23746..8e156e2d7 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -753,20 +753,25 @@ let remove_absent_xs ks q = let ks = Var.Set.inter ks q.xs in if Var.Set.is_empty ks then q else - let xs = Var.Set.diff q.xs ks in - let ctx = Context.elim ks q.ctx in - let djns = - let rec trim_ks ks djns = - List.map djns ~f:(fun djn -> - List.map djn ~f:(fun sjn -> - { sjn with - us= Var.Set.diff sjn.us ks - ; ctx= Context.elim ks sjn.ctx - ; djns= trim_ks ks sjn.djns } ) ) + let ks, ctx = Context.elim ks q.ctx in + if Var.Set.is_empty ks then q + else + let xs = Var.Set.diff q.xs ks in + let djns = + let rec trim_ks ks djns = + List.map djns ~f:(fun djn -> + List.map djn ~f:(fun sjn -> + let ks, ctx = Context.elim ks sjn.ctx in + if Var.Set.is_empty ks then sjn + else + { sjn with + us= Var.Set.diff sjn.us ks + ; ctx + ; djns= trim_ks ks sjn.djns } ) ) + in + trim_ks ks q.djns in - trim_ks ks q.djns - in - {q with xs; ctx; djns} + {q with xs; ctx; djns} let rec simplify_ us rev_xss q = [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q]