an optimization
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1538 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
0852fb888d
commit
bd5d81924c
|
@ -266,11 +266,17 @@ public class Simplifier {
|
||||||
}
|
}
|
||||||
|
|
||||||
private static boolean implies(IFormula axiom, IFormula f) {
|
private static boolean implies(IFormula axiom, IFormula f) {
|
||||||
|
|
||||||
if (normalize(axiom).equals(normalize(f))) {
|
if (normalize(axiom).equals(normalize(f))) {
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
if (axiom.getKind().equals(IFormula.Kind.QUANTIFIED)) {
|
if (axiom.getKind().equals(IFormula.Kind.QUANTIFIED)) {
|
||||||
QuantifiedFormula q = (QuantifiedFormula) axiom;
|
QuantifiedFormula q = (QuantifiedFormula) axiom;
|
||||||
|
|
||||||
|
if (!innerStructureMatches(q,f)) {
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
if (q.getQuantifier().equals(Quantifier.FORALL)) {
|
if (q.getQuantifier().equals(Quantifier.FORALL)) {
|
||||||
Variable bound = q.getBoundVar();
|
Variable bound = q.getBoundVar();
|
||||||
IFormula body = q.getFormula();
|
IFormula body = q.getFormula();
|
||||||
|
@ -315,6 +321,39 @@ public class Simplifier {
|
||||||
// return true;
|
// return true;
|
||||||
// }
|
// }
|
||||||
|
|
||||||
|
private static boolean innerStructureMatches(QuantifiedFormula q, IFormula f) {
|
||||||
|
IFormula g = innermost(q);
|
||||||
|
if (!f.getKind().equals(g.getKind())) {
|
||||||
|
return false;
|
||||||
|
} else {
|
||||||
|
// TODO be less conservative
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
// switch (g.getKind()) {
|
||||||
|
// case BINARY:
|
||||||
|
// return true;
|
||||||
|
// case CONSTANT:
|
||||||
|
// return g.equals(f);
|
||||||
|
// case NEGATION:
|
||||||
|
// return true;
|
||||||
|
// case RELATION:
|
||||||
|
// RelationFormula r1 = (RelationFormula)g;
|
||||||
|
// RelationFormula r2 = (RelationFormula)f;
|
||||||
|
// return r1.getRelation().equals(r2.getRelation());
|
||||||
|
// case QUANTIFIED:
|
||||||
|
// default:
|
||||||
|
// Assertions.UNREACHABLE();
|
||||||
|
}
|
||||||
|
|
||||||
|
public static IFormula innermost(QuantifiedFormula q) {
|
||||||
|
IFormula g = q.getFormula();
|
||||||
|
if (g.getKind().equals(IFormula.Kind.QUANTIFIED)) {
|
||||||
|
return innermost((QuantifiedFormula)g);
|
||||||
|
} else {
|
||||||
|
return g;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
private static Variable makeFresh(IFormula f, IFormula g) {
|
private static Variable makeFresh(IFormula f, IFormula g) {
|
||||||
int max = 0;
|
int max = 0;
|
||||||
for (Variable v : f.getFreeVariables()) {
|
for (Variable v : f.getFreeVariables()) {
|
||||||
|
|
Loading…
Reference in New Issue