01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic;
12:
13: import junit.framework.TestCase;
14: import de.uka.ilkd.key.logic.op.*;
15: import de.uka.ilkd.key.logic.sort.Sort;
16: import de.uka.ilkd.key.proof.TacletIndex;
17: import de.uka.ilkd.key.rule.RewriteTaclet;
18: import de.uka.ilkd.key.rule.RewriteTacletGoalTemplate;
19: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
20: import de.uka.ilkd.key.rule.TacletForTests;
21: import de.uka.ilkd.key.rule.inst.SVInstantiations;
22:
23: public class TestSyntacticalReplaceVisitor extends TestCase {
24:
25: SVInstantiations insts = null;
26:
27: Term rw;
28: Term t_allxpxpx;
29: private final static TermFactory tf = TermFactory.DEFAULT;
30:
31: public TestSyntacticalReplaceVisitor(String s) {
32: super (s);
33: }
34:
35: public void setUp() {
36: TacletIndex index = null;
37: TacletForTests.setStandardFile(TacletForTests.testRules);
38: TacletForTests.parse();
39: index = TacletForTests.getRules();
40: RewriteTaclet taclet = (RewriteTaclet) index.lookup(
41: "testSyntacticalReplaceVisitor_0").taclet();
42: rw = ((RewriteTacletGoalTemplate) taclet.goalTemplates().head())
43: .replaceWith();
44: SchemaVariable u = (SchemaVariable) rw.varsBoundHere(0)
45: .getQuantifiableVariable(0);
46:
47: SchemaVariable b = (SchemaVariable) rw.sub(0).sub(0).op();
48:
49: SchemaVariable c = (SchemaVariable) rw.sub(0).sub(1).sub(1)
50: .op();
51:
52: SchemaVariable v = (SchemaVariable) rw.sub(0).sub(1)
53: .varsBoundHere(1).getQuantifiableVariable(0);
54:
55: Sort s = ((SortedSchemaVariable) u).sort();
56:
57: LogicVariable x = new LogicVariable(new Name("x"), s);
58: LogicVariable y = new LogicVariable(new Name("y"), s);
59: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
60: new Sort[] { s });
61:
62: Term t_x = tf.createVariableTerm(x);
63: Term t_px = tf.createFunctionTerm(p, t_x);
64: Term t_y = tf.createVariableTerm(y);
65: Term t_py = tf.createFunctionTerm(p, t_y);
66:
67: insts = SVInstantiations.EMPTY_SVINSTANTIATIONS.add(b, t_px)
68: .add(v, t_y).add(u, t_x).add(c, t_py);
69:
70: t_allxpxpx = tf.createQuantifierTerm(Op.ALL, x, tf
71: .createJunctorTerm(Op.AND, t_px, t_px));
72:
73: }
74:
75: public void tearDown() {
76: insts = null;
77: rw = null;
78: t_allxpxpx = null;
79: }
80:
81: public void test1() {
82: SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
83: null, insts);
84: rw.execPostOrder(srv);
85: assertEquals(srv.getTerm(), t_allxpxpx);
86: }
87:
88: public void testSubstitutionReplacement() {
89: Term orig = TacletForTests
90: .parseTerm("{\\subst s x; f(const)}(\\forall s y; p(x))");
91: Term result = TacletForTests
92: .parseTerm("(\\forall s y; p(f(const)))");
93: SyntacticalReplaceVisitor v = new SyntacticalReplaceVisitor(
94: null, SVInstantiations.EMPTY_SVINSTANTIATIONS);
95: orig.execPostOrder(v);
96: assertEquals("Substitution Term not resolved correctly.", v
97: .getTerm().sub(0), result.sub(0));
98: }
99: }
|