some refactoring and more pretty printing

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

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

@@ -0,0 +1,35 @@
+/*******************************************************************************
+ * Copyright (c) 2006 IBM Corporation.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v1.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v10.html
+ *
+ * Contributors:
+ *     IBM Corporation - initial API and implementation
+ *******************************************************************************/
+package com.ibm.wala.logic;
+
+import java.util.Collection;
+import java.util.Collections;
+
+
+public abstract class AbstractConstant implements IConstant {
+  
+  public Kind getKind() {
+    return Kind.CONSTANT;
+   }
+
+  public String prettyPrint(ILogicDecorator d) {
+    return d.prettyPrint(this);
+  }
+
+  public Collection<Variable> getFreeVariables() {
+    return Collections.emptySet();
+  }
+
+  public Collection<? extends IConstant> getConstants() {
+    return Collections.singleton(this);
+  }
+  
+}

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

@@ -104,6 +104,13 @@ public class BinaryFormula implements IFormula {
     return result;
   }
   
+  public Collection<IConstant> getConstants() {
+    Collection<IConstant> result = HashSetFactory.make();
+    result.addAll(f1.getConstants());
+    result.addAll(f2.getConstants());
+    return result;
+  }
+  
   public String prettyPrint(ILogicDecorator d) {
     StringBuffer result = new StringBuffer();
     result.append("(");

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

@@ -10,11 +10,9 @@
  *******************************************************************************/
 package com.ibm.wala.logic;
 
-import java.util.Collection;
-import java.util.Collections;
 
 
-public class BooleanConstant implements IConstant {
+public class BooleanConstant extends AbstractConstant {
   
   public static final BooleanConstant TRUE = new BooleanConstant(true);
   public static final BooleanConstant FALSE = new BooleanConstant(false);
@@ -25,21 +23,8 @@ public class BooleanConstant implements IConstant {
     this.val = val;
   }
 
-  public Collection<Variable> getFreeVariables() {
-    return Collections.emptySet();
-  }
-
-  public Kind getKind() {
-    return Kind.CONSTANT;
-  }
-
   @Override
   public String toString() {
     return Boolean.toString(val);
   }
-
-  public String prettyPrint(ILogicDecorator d) {
-    return Boolean.toString(val);
-  }
-  
 }

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

@@ -16,6 +16,7 @@ import java.util.Collections;
 public class BooleanConstantFormula implements IFormula {
 
   public static final BooleanConstantFormula TRUE = new BooleanConstantFormula(BooleanConstant.TRUE);
+
   public static final BooleanConstantFormula FALSE = new BooleanConstantFormula(BooleanConstant.FALSE);
 
   private final BooleanConstant c;
@@ -28,6 +29,11 @@ public class BooleanConstantFormula implements IFormula {
     return Collections.emptySet();
   }
 
+  public Collection<? extends IConstant> getConstants() {
+    Collection<? extends IConstant> result = Collections.singleton(c);
+    return result;
+  }
+
   public Kind getKind() {
     return Kind.CONSTANT;
   }

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

@@ -67,7 +67,7 @@ public class DefaultDecorator implements ILogicDecorator {
   }
 
   public String prefixNotation(RelationFormula r) {
-    StringBuffer result = new StringBuffer(r.getRelation().getSymbol());
+    StringBuffer result = new StringBuffer(prettyPrint(r.getRelation()));
     result.append("(");
     for (int i = 0; i < r.getRelation().getValence() - 1; i++) {
       result.append(r.getTerms().get(i).prettyPrint(this));
@@ -85,10 +85,14 @@ public class DefaultDecorator implements ILogicDecorator {
     StringBuffer result = new StringBuffer();
     result.append(r.getTerms().get(0).prettyPrint(this));
     result.append(" ");
-    result.append(r.getRelation().getSymbol());
+    result.append(prettyPrint(r.getRelation()));
     result.append(" ");
     result.append(r.getTerms().get(1).prettyPrint(this));
     return result.toString();
   }
 
+  public String prettyPrint(IRelation r) {
+    return r.getSymbol();
+  }
+
 }

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

@@ -104,6 +104,14 @@ public class FunctionTerm implements ITerm {
     }
     return result;
   }
+  
+  public Collection<? extends IConstant> getConstants() {
+    Collection<IConstant> result = HashSetFactory.make();
+    for (ITerm t : parameters) {
+      result.addAll(t.getConstants());
+    }
+    return result;
+  }
 
   @Override
   public int hashCode() {

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

@@ -28,11 +28,22 @@ public interface IFormula {
     RELATION, NEGATION, BINARY, QUANTIFIED, CONSTANT
   }
   
+  /**
+   * Constant and Relation formulae are considered atomic.  Others not.
+   */
   public boolean isAtomic();
 
   public Kind getKind();
   
+  /**
+   * @return the free variables in this formula
+   */
   public Collection<Variable> getFreeVariables();
   
+  /**
+   * @return the constants that appear in this formula
+   */
+  public Collection<? extends IConstant> getConstants();
+  
   public String prettyPrint(ILogicDecorator d);
 }

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

@@ -28,5 +28,7 @@ public interface ILogicDecorator {
   String prettyPrint(FunctionTerm term);
 
   String prettyPrint(RelationFormula formula);
+  
+  String prettyPrint(IRelation r);
 
 }

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

@@ -30,4 +30,6 @@ public interface ITerm {
   public Collection<Variable> getFreeVariables();
 
   public String prettyPrint(ILogicDecorator d);
+
+  public Collection<? extends IConstant> getConstants();
 }

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

@@ -10,11 +10,9 @@
  *******************************************************************************/
 package com.ibm.wala.logic;
 
-import java.util.Collection;
-import java.util.Collections;
 
 
-public class IntConstant implements IConstant {
+public class IntConstant extends AbstractConstant {
   private final int val;
   
   protected IntConstant(int val) {
@@ -25,10 +23,6 @@ public class IntConstant implements IConstant {
     return new IntConstant(val);
   }
   
-  public Kind getKind() {
-    return Kind.CONSTANT;
-   }
-
   public int getVal() {
     return val;
   }
@@ -39,10 +33,6 @@ public class IntConstant implements IConstant {
   }
   
 
-  public String prettyPrint(ILogicDecorator d) {
-    return d.prettyPrint(this);
-  }
-
   @Override
   public int hashCode() {
     final int PRIME = 31;
@@ -64,9 +54,4 @@ public class IntConstant implements IConstant {
       return false;
     return true;
   }
-
-  public Collection<Variable> getFreeVariables() {
-    return Collections.emptySet();
-  }
-  
 }

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

@@ -64,6 +64,10 @@ public class NotFormula implements IFormula {
   public Collection<Variable> getFreeVariables() {
     return f.getFreeVariables();
   }
+  
+  public Collection<? extends IConstant> getConstants() {
+    return f.getConstants();
+  }
 
   @Override
   public String toString() {

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

@@ -103,6 +103,10 @@ public class QuantifiedFormula implements IFormula {
     result.remove(boundV);
     return result;
   }
+  
+  public Collection<? extends IConstant> getConstants() {
+    return f.getConstants();
+  }
 
   @Override
   public String toString() {

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

@@ -129,6 +129,14 @@ public class RelationFormula implements IFormula {
     }
     return result;
   }
+  
+  public Collection<? extends IConstant> getConstants() {
+    Collection<IConstant> result = HashSetFactory.make(terms.size());
+    for (ITerm t : terms) {
+      result.addAll(t.getConstants());
+    }
+    return result;
+  }
 
   @Override
   public String toString() {

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

@@ -80,6 +80,10 @@ public class Variable implements ITerm, Comparable<Variable> {
   public Collection<Variable> getFreeVariables() {
     return Collections.singleton(this);
   }
+  
+  public Collection<? extends IConstant> getConstants() {
+    return Collections.emptySet();
+  }
 
   public int compareTo(Variable o) throws NullPointerException {
     return this.getNumber() - o.getNumber();