delete half-baked logic package
git-svn-id: https://wala.svn.sourceforge.net/svnroot/wala/trunk@2749 f5eafffb-2e1d-0410-98e4-8ec43c5233c4
This commit is contained in:
sjfink
parent
32d846a7f4
commit
30f9303ee1
|
|
@ -1,112 +0,0 @@
|
|||
package com.ibm.wala.core.tests.logic;
|
||||
|
||||
/*******************************************************************************
|
||||
* Copyright (c) 2007 IBM Corporation.
|
||||
* All rights reserved. This program and the accompanying materials
|
||||
* are made available under the terms of the Eclipse Public License v1.0
|
||||
* which accompanies this distribution, and is available at
|
||||
* http://www.eclipse.org/legal/epl-v10.html
|
||||
*
|
||||
* Contributors:
|
||||
* IBM Corporation - initial API and implementation
|
||||
*******************************************************************************/
|
||||
|
||||
|
||||
import java.util.Collection;
|
||||
|
||||
import com.ibm.wala.core.tests.util.WalaTestCase;
|
||||
import com.ibm.wala.logic.BasicTheory;
|
||||
import com.ibm.wala.logic.BasicVocabulary;
|
||||
import com.ibm.wala.logic.BinaryFormula;
|
||||
import com.ibm.wala.logic.BinaryRelation;
|
||||
import com.ibm.wala.logic.FunctionTerm;
|
||||
import com.ibm.wala.logic.IFormula;
|
||||
import com.ibm.wala.logic.IFunction;
|
||||
import com.ibm.wala.logic.ILogicConstants;
|
||||
import com.ibm.wala.logic.IRelation;
|
||||
import com.ibm.wala.logic.ITheory;
|
||||
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.UnaryFunction;
|
||||
import com.ibm.wala.logic.UnaryRelation;
|
||||
import com.ibm.wala.util.collections.HashSetFactory;
|
||||
|
||||
/**
|
||||
* @author Satish Chandra
|
||||
*
|
||||
*/
|
||||
public class FormulaTest extends WalaTestCase {
|
||||
|
||||
public FormulaTest() {
|
||||
super("Formula Test");
|
||||
}
|
||||
|
||||
// F1: f(x,y) /\ g(z)
|
||||
public void testF1() {
|
||||
IntVariable x = IntVariable.make(1);
|
||||
IntVariable y = IntVariable.make(2);
|
||||
IntVariable z = IntVariable.make(3);
|
||||
RelationFormula fxy = RelationFormula.make(BinaryRelation.make("f"), x, y);
|
||||
RelationFormula gz = RelationFormula.make(UnaryRelation.make("g"), z);
|
||||
IFormula f1 = BinaryFormula.make(ILogicConstants.BinaryConnective.AND, fxy, gz);
|
||||
System.err.println(f1);
|
||||
}
|
||||
|
||||
// F2: !(t(p) == q)
|
||||
public void testF2() {
|
||||
IntVariable p = IntVariable.make(4);
|
||||
IntVariable q = IntVariable.make(5);
|
||||
IFormula f2 = NotFormula.make(RelationFormula.makeEquals(FunctionTerm.make(UnaryFunction.make("t"), p), q));
|
||||
System.err.println(f2);
|
||||
}
|
||||
|
||||
// F3: \exists s. (s > 0)
|
||||
public void testF3() {
|
||||
IntVariable s = IntVariable.make(6);
|
||||
IFormula f3 = QuantifiedFormula.make(ILogicConstants.Quantifier.EXISTS, s, RelationFormula.make(BinaryRelation.make(">"), s,
|
||||
IntConstant.make(0)));
|
||||
System.err.println(f3);
|
||||
}
|
||||
|
||||
// F4: In F2, substitute p by q
|
||||
public void testF4() {
|
||||
IntVariable p = IntVariable.make(4);
|
||||
IntVariable q = IntVariable.make(5);
|
||||
IFormula f2 = NotFormula.make(RelationFormula.makeEquals(FunctionTerm.make(UnaryFunction.make("t"), p), q));
|
||||
IFormula f4 = Simplifier.substitute(f2, p, q);
|
||||
System.err.println(f4);
|
||||
}
|
||||
|
||||
public void testTH1() {
|
||||
// Build a "theory"
|
||||
|
||||
IntVariable x = IntVariable.make(1);
|
||||
IntVariable y = IntVariable.make(2);
|
||||
IntVariable z = IntVariable.make(3);
|
||||
RelationFormula fxy = RelationFormula.make(BinaryRelation.make("f"), x, y);
|
||||
RelationFormula gz = RelationFormula.make(UnaryRelation.make("g"), z);
|
||||
IFormula f1 = BinaryFormula.make(ILogicConstants.BinaryConnective.AND, fxy, gz);
|
||||
|
||||
IntVariable p = IntVariable.make(4);
|
||||
IntVariable q = IntVariable.make(5);
|
||||
IFormula f2 = NotFormula.make(RelationFormula.makeEquals(FunctionTerm.make(UnaryFunction.make("t"), p), q));
|
||||
|
||||
Collection<IFormula> sentences = HashSetFactory.make();
|
||||
sentences.add(f1);
|
||||
sentences.add(f2);
|
||||
|
||||
Collection<IFunction> funcs = HashSetFactory.make();
|
||||
funcs.add(UnaryFunction.make("t"));
|
||||
|
||||
Collection<IRelation> rels = HashSetFactory.make();
|
||||
rels.add(BinaryRelation.make("f"));
|
||||
rels.add(UnaryRelation.make("g"));
|
||||
|
||||
ITheory th1 = BasicTheory.make(BasicVocabulary.make(funcs, rels), sentences);
|
||||
System.err.println(th1.toString());
|
||||
}
|
||||
}
|
||||
|
|
@ -1,316 +0,0 @@
|
|||
/*******************************************************************************
|
||||
* Copyright (c) 2007 IBM Corporation.
|
||||
* All rights reserved. This program and the accompanying materials
|
||||
* are made available under the terms of the Eclipse Public License v1.0
|
||||
* which accompanies this distribution, and is available at
|
||||
* http://www.eclipse.org/legal/epl-v10.html
|
||||
*
|
||||
* Contributors:
|
||||
* IBM Corporation - initial API and implementation
|
||||
*******************************************************************************/
|
||||
package com.ibm.wala.core.tests.logic;
|
||||
|
||||
import java.util.Collection;
|
||||
import java.util.Collections;
|
||||
|
||||
import junit.framework.TestCase;
|
||||
|
||||
import com.ibm.wala.logic.AdHocSemiDecisionProcedure;
|
||||
import com.ibm.wala.logic.BinaryFormula;
|
||||
import com.ibm.wala.logic.BinaryRelation;
|
||||
import com.ibm.wala.logic.BooleanConstant;
|
||||
import com.ibm.wala.logic.BooleanConstantFormula;
|
||||
import com.ibm.wala.logic.IFormula;
|
||||
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.util.collections.HashSetFactory;
|
||||
|
||||
/**
|
||||
* tests of logic simplification
|
||||
*
|
||||
* @author sjfink
|
||||
*/
|
||||
public class SimplifyTest extends TestCase {
|
||||
|
||||
/**
|
||||
* before: v1 = 0
|
||||
* theory: empty
|
||||
* after : v1 = 0
|
||||
*/
|
||||
public void test1() {
|
||||
IntVariable v = IntVariable.make(1);
|
||||
IFormula f = RelationFormula.makeEquals(v, 0);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
c = Simplifier.propositionalSimplify(c, t, AdHocSemiDecisionProcedure.singleton());
|
||||
for (IFormula x : c) {
|
||||
System.out.println("after : " + x);
|
||||
}
|
||||
assertTrue(c.size() == 1);
|
||||
assertTrue(c.iterator().next().equals(f));
|
||||
}
|
||||
|
||||
/**
|
||||
* before: v1 = 0
|
||||
* theory: v1 = 0
|
||||
* after : true
|
||||
*/
|
||||
public void test2() {
|
||||
IntVariable v = IntVariable.make(1);
|
||||
IFormula f = RelationFormula.makeEquals(v, 0);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
t.add(f);
|
||||
c = Simplifier.propositionalSimplify(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: v1 = 0
|
||||
* theory: v1 /= 0
|
||||
* after : false
|
||||
*/
|
||||
public void test3() {
|
||||
IntVariable v = IntVariable.make(1);
|
||||
IFormula f = RelationFormula.makeEquals(v, 0);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
t.add(NotFormula.make(f));
|
||||
c = Simplifier.propositionalSimplify(c, t, AdHocSemiDecisionProcedure.singleton());
|
||||
for (IFormula x : c) {
|
||||
System.out.println("after : " + x);
|
||||
}
|
||||
assertTrue(c.size() == 1);
|
||||
assertTrue(c.iterator().next().equals(BooleanConstantFormula.FALSE));
|
||||
}
|
||||
|
||||
/**
|
||||
* before: v1 = 0
|
||||
* theory: (true = true) <=> (v1 /= 0)
|
||||
* after : false
|
||||
*/
|
||||
public void test4() {
|
||||
IntVariable v = IntVariable.make(1);
|
||||
IFormula f = RelationFormula.makeEquals(v, 0);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
|
||||
IFormula lhs = RelationFormula.makeEquals(BooleanConstant.TRUE, BooleanConstant.TRUE);
|
||||
IFormula rhs = NotFormula.make(f);
|
||||
IFormula axiom = BinaryFormula.biconditional(lhs, rhs);
|
||||
t.add(axiom);
|
||||
c = Simplifier.propositionalSimplify(c, t, AdHocSemiDecisionProcedure.singleton());
|
||||
for (IFormula x : c) {
|
||||
System.out.println("after : " + x);
|
||||
}
|
||||
assertTrue(c.size() == 1);
|
||||
assertTrue(c.iterator().next().equals(BooleanConstantFormula.FALSE));
|
||||
}
|
||||
|
||||
// this simplification is disabled; doesn't always make sense.
|
||||
// /**
|
||||
// * before: v1 = 0 theory:
|
||||
// * FORALL v1. v1 = 0
|
||||
// * after : true
|
||||
// */
|
||||
// public void test5() {
|
||||
// IntVariable v = IntVariable.make(1);
|
||||
// IFormula f = RelationFormula.makeEquals(v, 0);
|
||||
// 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)
|
||||
* theory: FORALL v1. foo(v1,v1)
|
||||
* after : foo(v1,v2)
|
||||
*/
|
||||
public void test7() {
|
||||
IntVariable v1 = IntVariable.make(1);
|
||||
IntVariable v2 = IntVariable.make(2);
|
||||
BinaryRelation foo = BinaryRelation.make("foo");
|
||||
IFormula f = RelationFormula.make(foo, v1, v2);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
|
||||
IFormula g = RelationFormula.make(foo, v1, 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(f));
|
||||
}
|
||||
|
||||
/**
|
||||
* before: foo(v1,v2)
|
||||
* theory: FORALL v2. FORALL v1. foo(v1,v1)
|
||||
* after : foo(v1,v2)
|
||||
*/
|
||||
public void test8() {
|
||||
IntVariable v1 = IntVariable.make(1);
|
||||
IntVariable v2 = IntVariable.make(2);
|
||||
BinaryRelation foo = BinaryRelation.make("foo");
|
||||
IFormula f = RelationFormula.make(foo, v1, v2);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
|
||||
IFormula g = RelationFormula.make(foo, v1, v1);
|
||||
IFormula axiom = QuantifiedFormula.forall(v1, g);
|
||||
axiom = QuantifiedFormula.forall(v2, axiom);
|
||||
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(f));
|
||||
}
|
||||
|
||||
/**
|
||||
* before: foo(v1,v2)
|
||||
* theory: FORALL v1. FORALL v2. foo(v1,v1)
|
||||
* after : foo(v1,v2)
|
||||
*/
|
||||
public void test9() {
|
||||
IntVariable v1 = IntVariable.make(1);
|
||||
IntVariable v2 = IntVariable.make(2);
|
||||
BinaryRelation foo = BinaryRelation.make("foo");
|
||||
IFormula f = RelationFormula.make(foo, v1, v2);
|
||||
System.out.println("before: " + f);
|
||||
assertTrue(f != null);
|
||||
|
||||
Collection<IFormula> c = Collections.singleton(f);
|
||||
Collection<IFormula> t = HashSetFactory.make();
|
||||
|
||||
IFormula g = RelationFormula.make(foo, v1, v1);
|
||||
IFormula axiom = QuantifiedFormula.forall(v2, g);
|
||||
axiom = QuantifiedFormula.forall(v1, axiom);
|
||||
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(f));
|
||||
}
|
||||
|
||||
// /**
|
||||
// * 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));
|
||||
// }
|
||||
|
||||
// this simplification is disabled. doesn't always make sense.
|
||||
// /**
|
||||
// * before: foo(3,4) == 4
|
||||
// * theory: FORALL v1. FORALL v2. foo(v1, v2) == v2
|
||||
// * after : true
|
||||
// */
|
||||
// public void test11() {
|
||||
// BinaryFunction foo = BinaryFunction.make("foo");
|
||||
// IFormula f = RelationFormula.makeEquals(FunctionTerm.make(foo,IntConstant.make(3), IntConstant.make(4)), IntConstant.make(4));
|
||||
// System.out.println("before: " + f);
|
||||
// assertTrue(f != null);
|
||||
//
|
||||
// Collection<IFormula> c = Collections.singleton(f);
|
||||
// Collection<IFormula> t = HashSetFactory.make();
|
||||
// IntVariable v1 = IntVariable.make(1);
|
||||
// IntVariable v2 = IntVariable.make(2);
|
||||
// IFormula g = RelationFormula.makeEquals(FunctionTerm.make(foo,v1, v2), v2);
|
||||
// IFormula axiom = QuantifiedFormula.forall(v1, v2, 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));
|
||||
// }
|
||||
}
|
||||
Loading…
Reference in New Issue