DASCA
/
WALA
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

better simplification for disjunctions 

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1677 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
sjfink 2007-08-27 19:14:11 +00:00
parent bb33fa62c2
commit 76f3cc188f
1 changed files with 27 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
com.ibm.wala.core/src/com/ibm/wala/logic/Simplifier.java
View File

@ -69,7 +69,7 @@ public class Simplifier {
return Collections.singleton(s);
}
}
/**
* Eliminate quantifiers, by substituting every possible constant value for a
* quantified variable
@ -91,7 +91,8 @@ public class Simplifier {
*
* This is inefficient.
*/
public static Collection<IFormula> simplify(Collection<IFormula> s, Collection<? extends IFormula> theory, ISemiDecisionProcedure dec) {
public static Collection<IFormula> simplify(Collection<IFormula> s, Collection<? extends IFormula> theory,
ISemiDecisionProcedure dec) {
boolean changed = true;
while (changed) {
changed = false;
@ -120,7 +121,8 @@ public class Simplifier {
/**
* Simplify the set s based on simple propositional logic.
*/
public static Collection<IFormula> propositionalSimplify(Collection<IFormula> s, Collection<? extends IFormula> t, ISemiDecisionProcedure dec ) {
public static Collection<IFormula> propositionalSimplify(Collection<IFormula> s, Collection<? extends IFormula> t,
ISemiDecisionProcedure dec) {
debug1(s, t);
Collection<ICNFFormula> cs = toCNF(s);
Collection<ICNFFormula> ct = toCNF(t);
@ -155,8 +157,11 @@ public class Simplifier {
otherFacts.addAll(collectClauses(Collections.singleton(f)));
otherFacts.remove(d);
otherFacts.removeAll(removedClauses);
if (d instanceof Disjunction) {
d = simplifyDisjunction((Disjunction) d, otherFacts, dec);
}
if (dec.isContradiction(d, otherFacts)) {
return Collections.singleton(BooleanConstantFormula.FALSE);
} else if (facts.contains(d) || dec.isTautology(d, otherFacts)) {
@ -171,6 +176,20 @@ public class Simplifier {
return result;
}
private static IMaxTerm simplifyDisjunction(Disjunction d, Collection<IMaxTerm> otherFacts, ISemiDecisionProcedure dec) {
Collection<IFormula> result = HashSetFactory.make();
for (IFormula f : d.getClauses()) {
if (dec.isContradiction(f, otherFacts)) {
result.add(BooleanConstantFormula.FALSE);
} else if (dec.isTautology(f, otherFacts)) {
result.add(BooleanConstantFormula.TRUE);
} else {
result.add(f);
}
}
return Disjunction.make(result);
}
/**
* Collect all {@link IMaxTerm}s that appear in the formulae in s
*/
@ -340,7 +359,6 @@ public class Simplifier {
return Wildcard.make(max + 1);
}
/**
* in formula f, substitute the term t2 for all free occurrences of t1
*
@ -369,7 +387,7 @@ public class Simplifier {
RelationFormula r = (RelationFormula) formula;
List<ITerm> terms = new LinkedList<ITerm>();
for (ITerm t : r.getTerms()) {
Map<Wildcard,ITerm> binding = HashMapFactory.make();
Map<Wildcard, ITerm> binding = HashMapFactory.make();
terms.add(substitute(t, t1, t2, binding));
}
return RelationFormula.make(r.getRelation(), terms);
@ -505,7 +523,8 @@ public class Simplifier {
* Attempt to distribute the NOT from a NotFormula
*
* @return the original formula if the distribution is unsuccessful
* @throws IllegalArgumentException if f == null
* @throws IllegalArgumentException
* if f == null
*/
public static IFormula distributeNot(NotFormula f) throws IllegalArgumentException {
if (f == null) {