From bd5d81924ce37229d1817c4334cc040cfaf837d5 Mon Sep 17 00:00:00 2001
From: sjfink <sjfink@f5eafffb-2e1d-0410-98e4-8ec43c5233c4>
Date: Mon, 23 Jul 2007 17:12:52 +0000
Subject: [PATCH] an optimization

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1538 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
---
 .../src/com/ibm/wala/logic/Simplifier.java    | 39 +++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
index 9f392d0a2..836c276f1 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
+++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
@@ -266,11 +266,17 @@ public class Simplifier {
   }
 
   private static boolean implies(IFormula axiom, IFormula f) {
+
     if (normalize(axiom).equals(normalize(f))) {
       return true;
     }
     if (axiom.getKind().equals(IFormula.Kind.QUANTIFIED)) {
       QuantifiedFormula q = (QuantifiedFormula) axiom;
+      
+      if (!innerStructureMatches(q,f)) {
+        return false;
+      }
+      
       if (q.getQuantifier().equals(Quantifier.FORALL)) {
         Variable bound = q.getBoundVar();
         IFormula body = q.getFormula();
@@ -315,6 +321,39 @@ public class Simplifier {
   // return true;
   // }
 
+  private static boolean innerStructureMatches(QuantifiedFormula q, IFormula f) {
+    IFormula g = innermost(q);
+    if (!f.getKind().equals(g.getKind())) {
+      return false;
+    } else {
+      // TODO be less conservative
+      return true;
+    }
+//    switch (g.getKind()) {
+//    case BINARY:
+//      return true;
+//    case CONSTANT:
+//      return g.equals(f);
+//    case NEGATION:
+//      return true;
+//    case RELATION:
+//      RelationFormula r1 = (RelationFormula)g;
+//      RelationFormula r2 = (RelationFormula)f;
+//      return r1.getRelation().equals(r2.getRelation());
+//    case QUANTIFIED:
+//    default:
+//      Assertions.UNREACHABLE();
+  }
+  
+  public static IFormula innermost(QuantifiedFormula q) {
+    IFormula g = q.getFormula();
+    if (g.getKind().equals(IFormula.Kind.QUANTIFIED)) {
+      return innermost((QuantifiedFormula)g);
+    } else {
+      return g;
+    }
+   }
+
   private static Variable makeFresh(IFormula f, IFormula g) {
     int max = 0;
     for (Variable v : f.getFreeVariables()) {