misc. fixes with decorated printing

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

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

@@ -65,19 +65,7 @@ public class CNFFormula extends AbstractBinaryFormula implements ICNFFormula {
   }
 
   public String prettyPrint(ILogicDecorator d) {
-    if (maxTerms.size() == 1) {
-      return getF1().prettyPrint(d);
-    } else {
-      StringBuffer result = new StringBuffer();
-      result.append(" ( ");
-      result.append(getF1().prettyPrint(d));
-      result.append(" ) ");
-      result.append(d.prettyPrint(getConnective()));
-      result.append(" ( ");
-      result.append(getF2().prettyPrint(d));
-      result.append(" )");
-      return result.toString();
-    }
+    return d.prettyPrint(this);
   }
 
   public static ICNFFormula make(IFormula f) {

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

@@ -95,7 +95,7 @@ public class DefaultDecorator implements ILogicDecorator {
     return r.getSymbol();
   }
   
-  public String prettyPrint(BinaryFormula f) {
+  public String prettyPrint(AbstractBinaryFormula f) {
     StringBuffer result = new StringBuffer();
     result.append(" ( ");
     result.append(f.getF1().prettyPrint(this));

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

@@ -117,7 +117,7 @@ public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
     }
   }
 
-  public static Disjunction make(Collection<? extends IFormula> clauses) {
+  public static IMaxTerm make(Collection<? extends IFormula> clauses) {
     assert clauses.size() >= 2;
     Collection<IFormula> newClauses = HashSetFactory.make();
     for (IFormula c : clauses) {
@@ -126,27 +126,27 @@ public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
         newClauses.addAll(d.clauses);
       } else {
         if (Simplifier.isTautology(c)) {
-          return make(BooleanConstantFormula.TRUE);
+          return BooleanConstantFormula.TRUE;
         } else if (!Simplifier.isContradiction(c)) {
           newClauses.add(Simplifier.normalize(c));
         }
       }
     }
     if (newClauses.isEmpty()) {
-      return make(BooleanConstantFormula.FALSE);
+      return (BooleanConstantFormula.FALSE);
+    } else if (newClauses.size() == 1) {
+      IFormula f = newClauses.iterator().next();
+      assert f instanceof IMaxTerm;
+      return (IMaxTerm) f;
+    } else {
+      return new Disjunction(newClauses);
     }
-    return new Disjunction(newClauses);
   }
 
   public Collection<? extends IFormula> getClauses() {
     return Collections.unmodifiableCollection(clauses);
   }
 
-  public static Disjunction make(BooleanConstantFormula f) {
-    Collection<? extends IFormula> c = Collections.singleton(f);
-    return new Disjunction(c);
-  }
-
   @Override
   public String toString() {
     return prettyPrint(DefaultDecorator.instance());

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

@@ -31,7 +31,7 @@ public interface ILogicDecorator {
   
   String prettyPrint(IRelation r);
 
-  String prettyPrint(BinaryFormula binaryFormula);
+  String prettyPrint(AbstractBinaryFormula binaryFormula);
   
   String prettyPrint(NotFormula notFormula);