[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

@@ -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
 

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} *)
 

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

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. *)
 
 (**/**)
 

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)

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
 

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]