optimized substitution routines to not allocate unnecessarily

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@2684 f5eafffb-2e1d-0410-98e4-8ec43c5233c4

com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java

@@ -14,7 +14,6 @@ import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.Comparator;
-import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 
@@ -33,8 +32,7 @@ public class Simplifier {
   private final static boolean DEBUG = false;
 
   /**
-   * Eliminate quantifiers, by substituting every possible constant value for a
+   * Eliminate quantifiers, by substituting every possible constant value for a quantified variable
-   * quantified variable
    */
   public static ITheory eliminateQuantifiers(ITheory t, Collection<? extends IFormula> constraints) {
     if (t == null) {
@@ -48,8 +46,7 @@ public class Simplifier {
   }
 
   /**
-   * Eliminate quantifiers, by substituting every possible constant value for a
+   * Eliminate quantifiers, by substituting every possible constant value for a quantified variable
-   * quantified variable
    */
   private static Collection<? extends IFormula> eliminateQuantifiers(IFormula s) {
     Assertions.UNREACHABLE("implement me");
@@ -72,8 +69,7 @@ public class Simplifier {
   }
 
   /**
-   * Eliminate quantifiers, by substituting every possible constant value for a
+   * Eliminate quantifiers, by substituting every possible constant value for a quantified variable
-   * quantified variable
    */
   public static Collection<? extends IFormula> eliminateQuantifiers(Collection<? extends IFormula> s) {
     if (s == null) {
@@ -87,8 +83,7 @@ public class Simplifier {
   }
 
   /**
-   * this is uglified a little to avoid tail recursion, which leads to stack
+   * this is uglified a little to avoid tail recursion, which leads to stack overflow.
-   * overflow.
    * 
    * This is inefficient.
    */
@@ -145,11 +140,11 @@ public class Simplifier {
     }
     return result;
   }
+
   /**
    * Simplify the set s based on simple propositional logic.
    */
-  public static IFormula propositionalSimplify(IFormula f, Collection<? extends IFormula> t,
+  public static IFormula propositionalSimplify(IFormula f, Collection<? extends IFormula> t, ISemiDecisionProcedure dec) {
-      ISemiDecisionProcedure dec) {
     Collection<IFormula> result = propositionalSimplify(Collections.singleton(f), t, dec);
     return result.iterator().next();
   }
@@ -317,7 +312,8 @@ public class Simplifier {
   // *
   // * @return a pair (p1, p2) meaning "substitute p2 for p1"
   // */
-//  private static Pair<ITerm, ITerm> getNextEqualitySubstitution(Collection<IFormula> s, Collection<? extends IFormula> theory,
+  // private static Pair<ITerm, ITerm> getNextEqualitySubstitution(Collection<IFormula> s, Collection<? extends
+  // IFormula> theory,
   // Collection<IFormula> alreadyUsed) {
   // Collection<IFormula> candidates = HashSetFactory.make();
   // candidates.addAll(s);
@@ -391,8 +387,7 @@ public class Simplifier {
   /**
    * in formula f, substitute the term t2 for all free occurrences of t1
    * 
-   * @throws IllegalArgumentException
+   * @throws IllegalArgumentException if formula is null
-   *             if formula is null
    */
   public static IFormula substitute(IFormula formula, ITerm t1, ITerm t2) {
     if (formula == null) {
@@ -401,25 +396,50 @@ public class Simplifier {
     switch (formula.getKind()) {
     case BINARY:
       AbstractBinaryFormula b = (AbstractBinaryFormula) formula;
-      return BinaryFormula.make(b.getConnective(), substitute(b.getF1(), t1, t2), substitute(b.getF2(), t1, t2));
+      // TODO separate out cases for CNFFormula and Disjunction?
+      IFormula F1 = b.getF1();
+      IFormula subF1 = substitute(F1, t1, t2);
+      IFormula F2 = b.getF2();
+      IFormula subF2 = substitute(F2, t1, t2);
+      if (F1 != subF1 || F2 != subF2) {
+        return BinaryFormula.make(b.getConnective(), subF1, subF2);
+      } else {
+        return formula;
+      }
     case NEGATION:
       NotFormula n = (NotFormula) formula;
-      return NotFormula.make(substitute(n.getFormula(), t1, t2));
+      IFormula F = n.getFormula();
+      IFormula subF = substitute(F, t1, t2);
+      return F != subF ? NotFormula.make(subF) : formula;
     case QUANTIFIED:
       QuantifiedFormula q = (QuantifiedFormula) formula;
       if (q.getBoundVar().equals(t1)) {
         return q;
       } else {
-        return QuantifiedFormula.make(q.getQuantifier(), q.getBoundVar(), substitute(q.getFormula(), t1, t2));
+        IFormula body = q.getFormula();
+        IFormula subBody = substitute(body, t1, t2);
+        if (body != subBody) {
+          return QuantifiedFormula.make(q.getQuantifier(), q.getBoundVar(), subBody);
+        } else {
+          return formula;
+        }
       }
     case RELATION:
       RelationFormula r = (RelationFormula) formula;
-      List<ITerm> terms = new LinkedList<ITerm>();
+      List<ITerm> rTerms = r.getTerms();
-      for (ITerm t : r.getTerms()) {
+      List<ITerm> terms = new ArrayList<ITerm>(rTerms.size());
+      boolean someChange = false;
+      for (ITerm t : rTerms) {
         Map<Wildcard, ITerm> binding = HashMapFactory.make();
-        terms.add(substitute(t, t1, t2, binding));
+        ITerm subTerm = substituteInTerm(t, t1, t2, binding);
+        terms.add(subTerm);
+        someChange = someChange || t != subTerm;
       }
+      if (someChange) {
         return RelationFormula.make(r.getRelation(), terms);
+      } else {
+        return formula;
+      }
     case CONSTANT:
       return formula;
     default:
@@ -431,7 +451,7 @@ public class Simplifier {
   /**
    * in term t, substitute t2 for free occurrences of t1
    */
-  public static ITerm substitute(ITerm t, ITerm t1, ITerm t2, Map<Wildcard, ITerm> binding) {
+  public static ITerm substituteInTerm(ITerm t, ITerm t1, ITerm t2, Map<Wildcard, ITerm> binding) {
     assert t != null;
     assert t1 != null;
     assert t2 != null;
@@ -445,11 +465,19 @@ public class Simplifier {
       return t;
     case FUNCTION:
       FunctionTerm f = (FunctionTerm) t;
-      List<ITerm> terms = new LinkedList<ITerm>();
+      List<ITerm> parameters = f.getParameters();
-      for (ITerm p : f.getParameters()) {
+      List<ITerm> terms = new ArrayList<ITerm>(parameters.size());
-        terms.add(substitute(p, t1, t2, binding));
+      boolean someChange = false;
+      for (ITerm p : parameters) {
+        ITerm subTerm = substituteInTerm(p, t1, t2, binding);
+        terms.add(subTerm);
+        someChange = someChange || p != subTerm;
       }
+      if (someChange) {
         return FunctionTerm.make(f.getFunction(), terms);
+      } else {
+        return t;
+      }
     case VARIABLE:
       if (t1.equals(t)) {
         return t2;
@@ -481,10 +509,17 @@ public class Simplifier {
     case FUNCTION:
       FunctionTerm ft = (FunctionTerm) t;
       List<ITerm> terms = new ArrayList<ITerm>();
+      boolean someChange = false;
       for (ITerm p : ft.getParameters()) {
-        terms.add(bindingOf(p, binding));
+        ITerm bindingOfP = bindingOf(p, binding);
+        terms.add(bindingOfP);
+        someChange = someChange || p != bindingOfP;
       }
+      if (someChange) {
         return FunctionTerm.make(ft.getFunction(), terms);
+      } else {
+        return t;
+      }
     default:
       Assertions.UNREACHABLE(t);
       return null;
@@ -492,9 +527,8 @@ public class Simplifier {
   }
 
   /**
-   * Does the term t1 match the pattern t2? Note that this deals with wildcards.
+   * Does the term t1 match the pattern t2? Note that this deals with wildcards. Records bindings from Wildcards to
-   * Records bindings from Wildcards to Terms in the binding map ... modified as
+   * Terms in the binding map ... modified as a side effect.
-   * a side effect.
    */
   private static boolean termsMatch(ITerm t1, ITerm t2, Map<Wildcard, ITerm> binding) {
     if (t1.equals(t2)) {
@@ -552,8 +586,7 @@ public class Simplifier {
    * Attempt to distribute the NOT from a NotFormula
    * 
    * @return the original formula if the distribution is unsuccessful
-   * @throws IllegalArgumentException
+   * @throws IllegalArgumentException if f == null
-   *             if f == null
    */
   public static IFormula distributeNot(NotFormula f) throws IllegalArgumentException {
     if (f == null) {