tweak NotFormula stuff to work better with CNF
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@2704 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
e1adf2113b
commit
e48b76ad21
|
@ -143,7 +143,7 @@ public class CNFFormula extends AbstractBinaryFormula implements ICNFFormula {
|
||||||
case NEGATION:
|
case NEGATION:
|
||||||
NotFormula n = (NotFormula) f;
|
NotFormula n = (NotFormula) f;
|
||||||
if (n.getFormula() instanceof RelationFormula) {
|
if (n.getFormula() instanceof RelationFormula) {
|
||||||
IMaxTerm t = NotFormulaMaxTerm.make((RelationFormula)n.getFormula());
|
IMaxTerm t = NotFormulaMaxTerm.createNotFormulaMaxTerm((RelationFormula)n.getFormula());
|
||||||
return Collections.singleton(t);
|
return Collections.singleton(t);
|
||||||
} else {
|
} else {
|
||||||
// should not get here if other logic is working.
|
// should not get here if other logic is working.
|
||||||
|
|
|
@ -54,7 +54,7 @@ public class NotFormula implements IFormula {
|
||||||
if (r.getRelation().equals(BinaryRelation.LT)) {
|
if (r.getRelation().equals(BinaryRelation.LT)) {
|
||||||
return RelationFormula.make(BinaryRelation.GE, r.getTerms());
|
return RelationFormula.make(BinaryRelation.GE, r.getTerms());
|
||||||
}
|
}
|
||||||
return new NotFormula(f);
|
return NotFormulaMaxTerm.createNotFormulaMaxTerm(r);
|
||||||
case CONSTANT:
|
case CONSTANT:
|
||||||
if (f.equals(BooleanConstantFormula.TRUE)) {
|
if (f.equals(BooleanConstantFormula.TRUE)) {
|
||||||
return BooleanConstantFormula.FALSE;
|
return BooleanConstantFormula.FALSE;
|
||||||
|
|
|
@ -23,7 +23,7 @@ import java.util.Collections;
|
||||||
*/
|
*/
|
||||||
public class NotFormulaMaxTerm extends NotFormula implements IMaxTerm {
|
public class NotFormulaMaxTerm extends NotFormula implements IMaxTerm {
|
||||||
|
|
||||||
public static NotFormulaMaxTerm make(RelationFormula f) {
|
public static NotFormulaMaxTerm createNotFormulaMaxTerm(RelationFormula f) {
|
||||||
return new NotFormulaMaxTerm(f);
|
return new NotFormulaMaxTerm(f);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -418,7 +418,7 @@ public class Simplifier {
|
||||||
NotFormulaMaxTerm n = (NotFormulaMaxTerm) formula;
|
NotFormulaMaxTerm n = (NotFormulaMaxTerm) formula;
|
||||||
RelationFormula F = (RelationFormula) n.getFormula();
|
RelationFormula F = (RelationFormula) n.getFormula();
|
||||||
RelationFormula subF = (RelationFormula)substitute(F, t1, t2);
|
RelationFormula subF = (RelationFormula)substitute(F, t1, t2);
|
||||||
return (F != subF ? NotFormulaMaxTerm.make(subF) : formula);
|
return (F != subF ? NotFormulaMaxTerm.createNotFormulaMaxTerm(subF) : formula);
|
||||||
case QUANTIFIED:
|
case QUANTIFIED:
|
||||||
Assertions.UNREACHABLE();
|
Assertions.UNREACHABLE();
|
||||||
return null;
|
return null;
|
||||||
|
|
Loading…
Reference in New Issue