bug fixes
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1488 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
parent
1f42098a1e
commit
b96ca4eacc
|
@ -110,17 +110,26 @@ public class Disjunction extends AbstractBinaryFormula implements IMaxTerm {
|
||||||
public IFormula getF2() {
|
public IFormula getF2() {
|
||||||
Collection<? extends IFormula> c = HashSetFactory.make(clauses);
|
Collection<? extends IFormula> c = HashSetFactory.make(clauses);
|
||||||
c.remove(getF1());
|
c.remove(getF1());
|
||||||
return make(c);
|
if (c.size() == 1) {
|
||||||
|
return c.iterator().next();
|
||||||
|
} else {
|
||||||
|
return make(c);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
public static Disjunction make(Collection<? extends IFormula> clauses) {
|
public static Disjunction make(Collection<? extends IFormula> clauses) {
|
||||||
|
assert clauses.size() >= 2;
|
||||||
Collection<IFormula> newClauses = HashSetFactory.make();
|
Collection<IFormula> newClauses = HashSetFactory.make();
|
||||||
for (IFormula c : clauses) {
|
for (IFormula c : clauses) {
|
||||||
assert !(c instanceof Disjunction);
|
if (c instanceof Disjunction) {
|
||||||
if (Simplifier.isTautology(c)) {
|
Disjunction d = (Disjunction) c;
|
||||||
return make(BooleanConstantFormula.TRUE);
|
newClauses.addAll(d.clauses);
|
||||||
} else if (!Simplifier.isContradiction(c)) {
|
} else {
|
||||||
newClauses.add(c);
|
if (Simplifier.isTautology(c)) {
|
||||||
|
return make(BooleanConstantFormula.TRUE);
|
||||||
|
} else if (!Simplifier.isContradiction(c)) {
|
||||||
|
newClauses.add(c);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (newClauses.isEmpty()) {
|
if (newClauses.isEmpty()) {
|
||||||
|
|
Loading…
Reference in New Issue