support pretty-printing
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1290 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
a206218bde
commit
f7dd414734
|
@ -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
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
||||
}
|
|
@ -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();
|
||||
}
|
||||
|
|
|
@ -33,4 +33,6 @@ public interface IFormula {
|
|||
public Kind getKind();
|
||||
|
||||
public Collection<Variable> getFreeVariables();
|
||||
|
||||
public String prettyPrint(ILogicDecorator d);
|
||||
}
|
||||
|
|
|
@ -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);
|
||||
|
||||
}
|
|
@ -28,4 +28,6 @@ public interface ITerm {
|
|||
public Kind getKind();
|
||||
|
||||
public Collection<Variable> getFreeVariables();
|
||||
|
||||
public String prettyPrint(ILogicDecorator d);
|
||||
}
|
||||
|
|
|
@ -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() {
|
||||
|
|
|
@ -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<Variable> 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;
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
||||
|
|
|
@ -69,6 +69,11 @@ public class Variable implements ITerm, Comparable<Variable> {
|
|||
return "v" + getNumber();
|
||||
}
|
||||
|
||||
public String prettyPrint(ILogicDecorator d) {
|
||||
return d.prettyPrint(this);
|
||||
}
|
||||
|
||||
|
||||
public IntPair getRange() {
|
||||
return range;
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue