From 2aacc03880145ded7206191bd56e9326a6fea386 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 16 Apr 2020 03:37:33 -0700
Subject: [PATCH] [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  | 7 +++++++
 sledge/lib/equality.mli | 4 ++++
 sledge/lib/sh.ml        | 4 +++-
 3 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 835762e0f..98065b6bb 100644
--- a/sledge/lib/equality.ml
+++ b/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 =
diff --git a/sledge/lib/equality.mli b/sledge/lib/equality.mli
index 47c39687d..1cea046a3 100644
--- a/sledge/lib/equality.mli
+++ b/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
diff --git a/sledge/lib/sh.ml b/sledge/lib/sh.ml
index 45769dc43..e3293f58b 100644
--- a/sledge/lib/sh.ml
+++ b/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]