From f7dd414734a0653c227223d1f317ac29046d49d5 Mon Sep 17 00:00:00 2001 From: sjfink Date: Fri, 15 Jun 2007 21:27:03 +0000 Subject: [PATCH] support pretty-printing git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1290 f5eafffb-2e1d-0410-98e4-8ec43c5233c4 --- .../src/com/ibm/wala/logic/BinaryFormula.java | 23 +++++---- .../com/ibm/wala/logic/BooleanConstant.java | 4 ++ .../wala/logic/BooleanConstantFormula.java | 6 ++- .../com/ibm/wala/logic/DefaultDecorator.java | 47 +++++++++++++++++++ .../src/com/ibm/wala/logic/FunctionTerm.java | 8 +++- .../src/com/ibm/wala/logic/IFormula.java | 2 + .../com/ibm/wala/logic/ILogicDecorator.java | 28 +++++++++++ .../src/com/ibm/wala/logic/ITerm.java | 2 + .../src/com/ibm/wala/logic/IntConstant.java | 5 ++ .../src/com/ibm/wala/logic/NotFormula.java | 15 ++++-- .../com/ibm/wala/logic/QuantifiedFormula.java | 6 ++- .../com/ibm/wala/logic/RelationFormula.java | 20 ++++---- .../src/com/ibm/wala/logic/Variable.java | 5 ++ 13 files changed, 144 insertions(+), 27 deletions(-) create mode 100644 com.ibm.wala.core/src/com/ibm/wala/logic/DefaultDecorator.java create mode 100644 com.ibm.wala.core/src/com/ibm/wala/logic/ILogicDecorator.java diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java index 6af08fb74..133221604 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BinaryFormula.java @@ -103,19 +103,22 @@ public class BinaryFormula implements IFormula { result.addAll(f2.getFreeVariables()); return result; } + + public String prettyPrint(ILogicDecorator d) { + StringBuffer result = new StringBuffer(); + result.append("("); + result.append(f1.prettyPrint(d)); + result.append(") "); + result.append(d.prettyPrint(b)); + result.append(" ("); + result.append(f2.prettyPrint(d)); + result.append(")"); + return result.toString(); + } @Override public String toString() { - StringBuffer result = new StringBuffer(); - result.append("("); - result.append(f1); - result.append(") "); - result.append(b); - result.append(" ("); - result.append(f2); - result.append(")"); - return result.toString(); - + return prettyPrint(DefaultDecorator.instance()); } @Override diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java index abdf6c2c6..2313a3167 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstant.java @@ -37,5 +37,9 @@ public class BooleanConstant implements IConstant { public String toString() { return Boolean.toString(val); } + + public String prettyPrint(ILogicDecorator d) { + return Boolean.toString(val); + } } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java index 82d1b19e7..845cb8a8b 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/BooleanConstantFormula.java @@ -38,7 +38,11 @@ public class BooleanConstantFormula implements IFormula { @Override public String toString() { - return c.toString(); + return prettyPrint(DefaultDecorator.instance()); + } + + public String prettyPrint(ILogicDecorator d) { + return d.prettyPrint(c); } } 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 new file mode 100644 index 000000000..622ee464c --- /dev/null +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/DefaultDecorator.java @@ -0,0 +1,47 @@ +/******************************************************************************* + * Copyright (c) 2007 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 com.ibm.wala.logic.ILogicConstants.BinaryConnective; +import com.ibm.wala.logic.ILogicConstants.Quantifier; + +public class DefaultDecorator implements ILogicDecorator { + + private final static DefaultDecorator INSTANCE = new DefaultDecorator(); + + protected DefaultDecorator() { + } + + public static DefaultDecorator instance() { + return INSTANCE; + } + + public String prettyPrint(BinaryConnective b) { + return b.toString(); + } + + public String prettyPrint(BooleanConstant c) { + return c.toString(); + } + + public String prettyPrint(Variable v) { + return v.toString(); + } + + public String prettyPrint(Quantifier q) { + return q.toString(); + } + + public String prettyPrint(IConstant constant) { + return constant.toString(); + } + +} diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java b/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java index 753c2589f..86f9ffab0 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/FunctionTerm.java @@ -36,13 +36,17 @@ public class FunctionTerm implements ITerm { @Override public String toString() { + return prettyPrint(DefaultDecorator.instance()); + } + + public String prettyPrint(ILogicDecorator d) { StringBuffer result = new StringBuffer(f.getSymbol()); result.append("("); for (int i = 0; i < f.getNumberOfParameters() - 1; i++) { - result.append(parameters.get(i)); + result.append(parameters.get(i).prettyPrint(d)); result.append(","); } - result.append(parameters.get(f.getNumberOfParameters() - 1)); + result.append(parameters.get(f.getNumberOfParameters() - 1).prettyPrint(d)); result.append(")"); return result.toString(); } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java index 1493e6e93..6e88c6486 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/IFormula.java @@ -33,4 +33,6 @@ public interface IFormula { public Kind getKind(); public Collection getFreeVariables(); + + public String prettyPrint(ILogicDecorator d); } 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 new file mode 100644 index 000000000..7747dcb88 --- /dev/null +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/ILogicDecorator.java @@ -0,0 +1,28 @@ +/******************************************************************************* + * Copyright (c) 2007 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 com.ibm.wala.logic.ILogicConstants.BinaryConnective; +import com.ibm.wala.logic.ILogicConstants.Quantifier; + +public interface ILogicDecorator { + + String prettyPrint(BinaryConnective b); + + String prettyPrint(BooleanConstant c); + + String prettyPrint(Variable boundVar); + + String prettyPrint(Quantifier quantifier); + + String prettyPrint(IConstant constant); + +} diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java b/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java index ad9cec486..6ebbcdc67 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/ITerm.java @@ -28,4 +28,6 @@ public interface ITerm { public Kind getKind(); public Collection getFreeVariables(); + + public String prettyPrint(ILogicDecorator d); } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/IntConstant.java b/com.ibm.wala.core/src/com/ibm/wala/logic/IntConstant.java index 874209f71..28ea7215e 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/IntConstant.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/IntConstant.java @@ -37,6 +37,11 @@ public class IntConstant implements IConstant { public String toString() { return String.valueOf(val); } + + + public String prettyPrint(ILogicDecorator d) { + return d.prettyPrint(this); + } @Override public int hashCode() { diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java index c7cdc55b9..0382556ef 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/NotFormula.java @@ -14,7 +14,7 @@ import java.util.Collection; /** * @author sjfink - * + * */ public class NotFormula implements IFormula { @@ -27,10 +27,10 @@ public class NotFormula implements IFormula { throw new IllegalArgumentException("f cannot be null"); } } - + public static IFormula make(IFormula f) { if (f instanceof RelationFormula) { - RelationFormula r = (RelationFormula)f; + RelationFormula r = (RelationFormula) f; if (r.getRelation().equals(BinaryRelation.EQUALS)) { return RelationFormula.make(BinaryRelation.NE, r.getTerms()); } @@ -64,11 +64,16 @@ public class NotFormula implements IFormula { public Collection getFreeVariables() { return f.getFreeVariables(); } - + @Override public String toString() { - return "not(" + f + ")"; + return prettyPrint(DefaultDecorator.instance()); } + + public String prettyPrint(ILogicDecorator d) { + return "not(" + f.prettyPrint(d) + ")"; + } + public boolean isAtomic() { return false; } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java index bd4db5d25..ecf166db9 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/QuantifiedFormula.java @@ -108,7 +108,11 @@ public class QuantifiedFormula implements IFormula { public String toString() { return getQuantifier() + " " + getBoundVar() + getBoundVar().getRange() + "." + getFormula(); } - + + public String prettyPrint(ILogicDecorator d) { + return d.prettyPrint(getQuantifier()) + " " + d.prettyPrint(getBoundVar()) + "." + getFormula().prettyPrint(d); + } + public boolean isAtomic() { return false; } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java b/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java index ceff160c1..f3898a3cc 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/RelationFormula.java @@ -132,34 +132,38 @@ public class RelationFormula implements IFormula { @Override public String toString() { + return prettyPrint(DefaultDecorator.instance()); + } + + public String prettyPrint(ILogicDecorator d) { if (R.getValence() == 2) { - return infixNotation(); + return infixNotation(d); } else { - return prefixNotation(); + return prefixNotation(d); } } - private String prefixNotation() { + private String prefixNotation(ILogicDecorator d) { StringBuffer result = new StringBuffer(R.getSymbol()); result.append("("); for (int i = 0; i < R.getValence() - 1; i++) { - result.append(terms.get(i)); + result.append(terms.get(i).prettyPrint(d)); result.append(","); } if (R.getValence() > 0) - result.append(terms.get(R.getValence() - 1)); + result.append(terms.get(R.getValence() - 1).prettyPrint(d)); result.append(")"); return result.toString(); } - private String infixNotation() { + private String infixNotation(ILogicDecorator d) { assert R.getValence() == 2; StringBuffer result = new StringBuffer(); - result.append(terms.get(0)); + result.append(terms.get(0).prettyPrint(d)); result.append(" "); result.append(R.getSymbol()); result.append(" "); - result.append(terms.get(1)); + result.append(terms.get(1).prettyPrint(d)); return result.toString(); } diff --git a/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java b/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java index 6bf798268..b94559ad1 100644 --- a/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java +++ b/com.ibm.wala.core/src/com/ibm/wala/logic/Variable.java @@ -69,6 +69,11 @@ public class Variable implements ITerm, Comparable { return "v" + getNumber(); } + public String prettyPrint(ILogicDecorator d) { + return d.prettyPrint(this); + } + + public IntPair getRange() { return range; }