From b3cdac76e4ab2a65fa6017de6432b5d075ab4f2e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 2 Mar 2020 08:43:41 -0800
Subject: [PATCH] [sledge] Remove hacky treatment of tautologous existential
 equalities

Summary: Subsumed by strengthened existential witnessing.

Reviewed By: ngorogiannis

Differential Revision: D20120280

fbshipit-source-id: 9cb33faf6
---
 sledge/src/symbheap/solver.ml | 19 +------------------
 1 file changed, 1 insertion(+), 18 deletions(-)

diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index 76419f9b5..ba4486a8f 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/sledge/src/symbheap/solver.ml
@@ -75,25 +75,8 @@ let excise_exists goal =
           let min = Sh.and_subst witnesses goal.min in
           {goal with us; min; xs; pgs= true} )
 
-(* ad hoc treatment to drop tautologous constraints such as ∃x,y. x = y
-   where x and y do not appear elsewhere *)
-let drop_tautology xs sub e =
-  match (e : Term.t) with
-  | Ap2 (Eq, Var _, Var _) ->
-      let vs = Term.fv e in
-      if not (Set.is_subset vs ~of_:xs) then e
-      else
-        let var_strength = Sh.var_strength (Sh.exists xs sub) in
-        if
-          Set.for_all vs ~f:(fun v ->
-              Poly.equal (Map.find var_strength v) (Some `Anonymous) )
-        then Term.true_
-        else e
-  | _ -> e
-
-let excise_term ({min; xs; sub} as goal) pure term =
+let excise_term ({min} as goal) pure term =
   let term' = Equality.normalize min.cong term in
-  let term' = drop_tautology xs sub term' in
   if Term.is_false term' then None
   else if Term.is_true term' then (
     excise (fun {pf} -> pf "excise_pure %a" Term.pp term) ;