[sledge] Remove eliminated existentials from equality relations

Summary:
Currently there is an implicit assumption in Sh.simplify that
variables do not occur free in an equality relation which makes no
constraint on their values. This diff adds a step to formula
simplification that explicitly removes eliminated existentials from
equality relations.

Reviewed By: jvillard

Differential Revision: D20726960

fbshipit-source-id: 7109aa479

sledge/lib/equality.ml

@@ -52,6 +52,7 @@ module Subst : sig
   val compose : t -> t -> t
   val compose1 : key:Term.t -> data:Term.t -> t -> t
   val extend : Term.t -> t -> t option
+  val remove : Var.Set.t -> t -> t
   val map_entries : f:(Term.t -> Term.t) -> t -> t
   val to_alist : t -> (Term.t * Term.t) list
   val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
@@ -109,6 +110,10 @@ end = struct
     | exception Found -> None
     | s -> Some s
 
+  (** remove entries for vars *)
+  let remove xs s =
+    Var.Set.fold ~f:(fun s x -> Term.Map.remove s (Term.var x)) ~init:s xs
+
   (** 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] *)
@@ -1016,6 +1021,8 @@ 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}
+
 (* Replay debugging *)
 
 type call =

sledge/lib/equality.mli

@@ -102,6 +102,10 @@ val solve_for_vars : Var.Set.t list -> t -> Subst.t
     to terms [e] with free variables contained in as short a prefix of [uss]
     as possible. *)
 
+val elim : Var.Set.t -> t -> t
+(** Weaken relation by removing oriented equations [k ↦ _] for [k] in
+    [ks]. *)
+
 (* Replay debugging *)
 
 val replay : string -> unit

sledge/lib/sh.ml

@@ -725,17 +725,19 @@ let remove_absent_xs ks q =
   if Var.Set.is_empty ks then q
   else
     let xs = Var.Set.diff q.xs ks in
+    let cong = Equality.elim ks q.cong 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
+                ; cong= Equality.elim ks sjn.cong
                 ; djns= trim_ks ks sjn.djns } ) )
       in
       trim_ks ks q.djns
     in
-    {q with xs; djns}
+    {q with xs; cong; djns}
 
 let rec simplify_ us rev_xss q =
   [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q]