more simplification logic
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1537 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
3355b6207e
commit
0852fb888d
|
@ -32,6 +32,10 @@ public abstract class AbstractConstant implements IConstant {
|
||||||
return Collections.singleton(this);
|
return Collections.singleton(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
|
return Collections.singleton(this);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
public abstract boolean equals(Object obj);
|
public abstract boolean equals(Object obj);
|
||||||
|
|
|
@ -103,10 +103,10 @@ public class BinaryFormula extends AbstractBinaryFormula {
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
public Collection<? extends ITerm> getTerms() {
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
Collection<ITerm> result = HashSetFactory.make();
|
Collection<ITerm> result = HashSetFactory.make();
|
||||||
result.addAll(f1.getTerms());
|
result.addAll(f1.getAllTerms());
|
||||||
result.addAll(f2.getTerms());
|
result.addAll(f2.getAllTerms());
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -11,7 +11,6 @@
|
||||||
package com.ibm.wala.logic;
|
package com.ibm.wala.logic;
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
public class BooleanConstant extends AbstractConstant {
|
public class BooleanConstant extends AbstractConstant {
|
||||||
|
|
||||||
public static final BooleanConstant TRUE = new BooleanConstant(true);
|
public static final BooleanConstant TRUE = new BooleanConstant(true);
|
||||||
|
|
|
@ -62,4 +62,8 @@ public class BooleanConstantFormula implements IMaxTerm {
|
||||||
return 163 * c.hashCode();
|
return 163 * c.hashCode();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
|
return Collections.singleton(c);
|
||||||
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -48,10 +48,10 @@ public class CNFFormula extends AbstractBinaryFormula implements ICNFFormula {
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
public Collection<? extends ITerm> getTerms() {
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
Collection<ITerm> result = HashSetFactory.make();
|
Collection<ITerm> result = HashSetFactory.make();
|
||||||
for (IFormula f : maxTerms) {
|
for (IFormula f : maxTerms) {
|
||||||
result.addAll(f.getTerms());
|
result.addAll(f.getAllTerms());
|
||||||
}
|
}
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
|
@ -39,10 +39,10 @@ public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
public Collection<? extends ITerm> getTerms() {
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
Collection<ITerm> result = HashSetFactory.make();
|
Collection<ITerm> result = HashSetFactory.make();
|
||||||
for (IFormula f : clauses) {
|
for (IFormula f : clauses) {
|
||||||
result.addAll(f.getTerms());
|
result.addAll(f.getAllTerms());
|
||||||
}
|
}
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
|
@ -143,4 +143,13 @@ public class FunctionTerm extends AbstractTerm {
|
||||||
return false;
|
return false;
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
|
Collection<ITerm> result = HashSetFactory.make();
|
||||||
|
result.add(this);
|
||||||
|
for (ITerm t : parameters) {
|
||||||
|
result.addAll(t.getAllTerms());
|
||||||
|
}
|
||||||
|
return result;
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -41,9 +41,9 @@ public interface IFormula {
|
||||||
public Collection<? extends IConstant> getConstants();
|
public Collection<? extends IConstant> getConstants();
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* @return the terms that appear in this formula
|
* @return all terms that appear in this formula, including recursive descent on on-atomic terms
|
||||||
*/
|
*/
|
||||||
public Collection<? extends ITerm> getTerms();
|
public Collection<? extends ITerm> getAllTerms();
|
||||||
|
|
||||||
public String prettyPrint(ILogicDecorator d);
|
public String prettyPrint(ILogicDecorator d);
|
||||||
|
|
||||||
|
|
|
@ -32,4 +32,9 @@ public interface ITerm {
|
||||||
public String prettyPrint(ILogicDecorator d);
|
public String prettyPrint(ILogicDecorator d);
|
||||||
|
|
||||||
public Collection<? extends IConstant> getConstants();
|
public Collection<? extends IConstant> getConstants();
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Collect all terms that appear in this term, including subterms if this is a function term
|
||||||
|
*/
|
||||||
|
public Collection<? extends ITerm> getAllTerms();
|
||||||
}
|
}
|
||||||
|
|
|
@ -83,8 +83,8 @@ public class NotFormula implements IFormula {
|
||||||
return f.getConstants();
|
return f.getConstants();
|
||||||
}
|
}
|
||||||
|
|
||||||
public Collection<? extends ITerm> getTerms() {
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
return f.getTerms();
|
return f.getAllTerms();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
|
|
|
@ -108,8 +108,8 @@ public class QuantifiedFormula implements IMaxTerm {
|
||||||
return f.getConstants();
|
return f.getConstants();
|
||||||
}
|
}
|
||||||
|
|
||||||
public Collection<? extends ITerm> getTerms() {
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
return f.getTerms();
|
return f.getAllTerms();
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
|
|
|
@ -35,6 +35,15 @@ public class RelationFormula implements IMaxTerm {
|
||||||
return terms;
|
return terms;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
|
Collection<ITerm> result = HashSetFactory.make();
|
||||||
|
for (ITerm t: terms) {
|
||||||
|
result.addAll(t.getAllTerms());
|
||||||
|
}
|
||||||
|
return result;
|
||||||
|
}
|
||||||
|
|
||||||
private RelationFormula(final IRelation R, final List<ITerm> terms) throws IllegalArgumentException {
|
private RelationFormula(final IRelation R, final List<ITerm> terms) throws IllegalArgumentException {
|
||||||
super();
|
super();
|
||||||
this.R = R;
|
this.R = R;
|
||||||
|
@ -171,4 +180,5 @@ public class RelationFormula implements IMaxTerm {
|
||||||
result.append(terms.get(1).prettyPrint(d));
|
result.append(terms.get(1).prettyPrint(d));
|
||||||
return result.toString();
|
return result.toString();
|
||||||
}
|
}
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
|
@ -275,16 +275,16 @@ public class Simplifier {
|
||||||
Variable bound = q.getBoundVar();
|
Variable bound = q.getBoundVar();
|
||||||
IFormula body = q.getFormula();
|
IFormula body = q.getFormula();
|
||||||
// this could be inefficient. find a better algorithm.
|
// this could be inefficient. find a better algorithm.
|
||||||
for (Variable free : f.getFreeVariables()) {
|
for (ITerm t : f.getAllTerms()) {
|
||||||
if (q.getFreeVariables().contains(free)) {
|
if (q.getFreeVariables().contains(t)) {
|
||||||
Variable fresh = makeFresh(q, f);
|
Variable fresh = makeFresh(q, f);
|
||||||
IFormula testBody = substitute(body, bound, fresh);
|
IFormula testBody = substitute(body, bound, fresh);
|
||||||
IFormula testF = substitute(f, free, fresh);
|
IFormula testF = substitute(f, t, fresh);
|
||||||
if (implies(testBody,testF)) {
|
if (implies(testBody,testF)) {
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
IFormula testBody = substitute(body, bound, free);
|
IFormula testBody = substitute(body, bound, t);
|
||||||
if (implies(testBody, f)) {
|
if (implies(testBody, f)) {
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
|
@ -93,4 +93,8 @@ public class Variable extends AbstractTerm implements Comparable<Variable> {
|
||||||
public int compareTo(Variable o) throws NullPointerException {
|
public int compareTo(Variable o) throws NullPointerException {
|
||||||
return this.getNumber() - o.getNumber();
|
return this.getNumber() - o.getNumber();
|
||||||
}
|
}
|
||||||
|
|
||||||
|
public Collection<? extends ITerm> getAllTerms() {
|
||||||
|
return Collections.singleton(this);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue