From 66afbbc77d6e56576fb3609130af81f49fd2a93a Mon Sep 17 00:00:00 2001
From: sjfink <sjfink@f5eafffb-2e1d-0410-98e4-8ec43c5233c4>
Date: Mon, 13 Aug 2007 19:24:32 +0000
Subject: [PATCH] misc. fixes with decorated printing

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1614 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
---
 .../src/com/ibm/wala/logic/CNFFormula.java     | 14 +-------------
 .../com/ibm/wala/logic/DefaultDecorator.java   |  2 +-
 .../src/com/ibm/wala/logic/Disjunction.java    | 18 +++++++++---------
 .../com/ibm/wala/logic/ILogicDecorator.java    |  2 +-
 4 files changed, 12 insertions(+), 24 deletions(-)

diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
index c70cb31e0..3c5186e90 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/CNFFormula.java
+++ b/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) {
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/DefaultDecorator.java b/com.ibm.wala.core/src/com/ibm/wala/logic/DefaultDecorator.java
index d68bd1f6b..9118bbb37 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/DefaultDecorator.java
+++ b/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));
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
index 825a4d7de..dc73bf3e0 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/Disjunction.java
+++ b/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());
diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/ILogicDecorator.java b/com.ibm.wala.core/src/com/ibm/wala/logic/ILogicDecorator.java
index 119dab3c4..527e92959 100644
--- a/com.ibm.wala.core/src/com/ibm/wala/logic/ILogicDecorator.java
+++ b/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);