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

disable overly expensive quantifier simplification logic 

git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@1672 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
sjfink 2007-08-27 13:46:32 +00:00
parent 8409af2af0
commit 8829f2bdcb
1 changed files with 53 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

104
com.ibm.wala.core.tests/src/com/ibm/wala/core/tests/logic/SimplifyTest.java
View File

@ -24,12 +24,11 @@ import com.ibm.wala.logic.BooleanConstantFormula;
import com.ibm.wala.logic.FunctionTerm;
import com.ibm.wala.logic.IFormula;
import com.ibm.wala.logic.IntConstant;
import com.ibm.wala.logic.IntVariable;
import com.ibm.wala.logic.NotFormula;
import com.ibm.wala.logic.QuantifiedFormula;
import com.ibm.wala.logic.RelationFormula;
import com.ibm.wala.logic.Simplifier;
import com.ibm.wala.logic.UnaryRelation;
import com.ibm.wala.logic.IntVariable;
import com.ibm.wala.util.collections.HashSetFactory;
/**
@ -153,31 +152,33 @@ public class SimplifyTest extends TestCase {
assertTrue(c.size() == 1);
assertTrue(c.iterator().next().equals(BooleanConstantFormula.TRUE));
}
/**
* before: foo(v1,v1)
* theory: FORALL v1. foo(v1,v1)
* after : true
*/
public void test6() {
IntVariable v = IntVariable.make(1);
BinaryRelation foo = BinaryRelation.make("foo");
IFormula f = RelationFormula.make(foo, v, v);
System.out.println("before: " + f);
assertTrue(f != null);
Collection<IFormula> c = Collections.singleton(f);
Collection<IFormula> t = HashSetFactory.make();
IFormula axiom = QuantifiedFormula.forall(v, f);
t.add(axiom);
c = Simplifier.simplify(c, t, AdHocSemiDecisionProcedure.singleton());
for (IFormula x : c) {
System.out.println("after : " + x);
}
assertTrue(c.size() == 1);
assertTrue(c.iterator().next().equals(BooleanConstantFormula.TRUE));
}
//
// /**
// * before: foo(v1,v1)
// * theory: FORALL v1. foo(v1,v1)
// * after : true
// *
// * Quantifier simplification logic currently disabled
// */
// public void test6() {
// IntVariable v = IntVariable.make(1);
// BinaryRelation foo = BinaryRelation.make("foo");
// IFormula f = RelationFormula.make(foo, v, v);
// System.out.println("before: " + f);
// assertTrue(f != null);
//
// Collection<IFormula> c = Collections.singleton(f);
// Collection<IFormula> t = HashSetFactory.make();
//
// IFormula axiom = QuantifiedFormula.forall(v, f);
// t.add(axiom);
// c = Simplifier.simplify(c, t, AdHocSemiDecisionProcedure.singleton());
// for (IFormula x : c) {
// System.out.println("after : " + x);
// }
// assertTrue(c.size() == 1);
// assertTrue(c.iterator().next().equals(BooleanConstantFormula.TRUE));
// }
/**
* before: foo(v1,v2)
@ -262,30 +263,31 @@ public class SimplifyTest extends TestCase {
assertTrue(c.iterator().next().equals(f));
}
/**
* before: foo(0)
* theory: FORALL v1. foo(v1)
* after : true
*/
public void test10() {
UnaryRelation foo = UnaryRelation.make("foo");
IFormula f = RelationFormula.make(foo, IntConstant.make(0));
System.out.println("before: " + f);
assertTrue(f != null);
Collection<IFormula> c = Collections.singleton(f);
Collection<IFormula> t = HashSetFactory.make();
IntVariable v1 = IntVariable.make(1);
IFormula g = RelationFormula.make(foo, v1);
IFormula axiom = QuantifiedFormula.forall(v1, g);
t.add(axiom);
c = Simplifier.simplify(c, t, AdHocSemiDecisionProcedure.singleton());
for (IFormula x : c) {
System.out.println("after : " + x);
}
assertTrue(c.size() == 1);
assertTrue(c.iterator().next().equals(BooleanConstantFormula.TRUE));
}
// /**
// * before: foo(0)
// * theory: FORALL v1. foo(v1)
// * after : true
// Quantifier simplification logic currently disabled
// */
// public void test10() {
// UnaryRelation foo = UnaryRelation.make("foo");
// IFormula f = RelationFormula.make(foo, IntConstant.make(0));
// System.out.println("before: " + f);
// assertTrue(f != null);
//
// Collection<IFormula> c = Collections.singleton(f);
// Collection<IFormula> t = HashSetFactory.make();
// IntVariable v1 = IntVariable.make(1);
// IFormula g = RelationFormula.make(foo, v1);
// IFormula axiom = QuantifiedFormula.forall(v1, g);
// t.add(axiom);
// c = Simplifier.simplify(c, t, AdHocSemiDecisionProcedure.singleton());
// for (IFormula x : c) {
// System.out.println("after : " + x);
// }
// assertTrue(c.size() == 1);
// assertTrue(c.iterator().next().equals(BooleanConstantFormula.TRUE));
// }
/**
* before: foo(3,4) == 4