001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.logic;
012:
013: import java.io.PrintWriter;
014: import java.io.StringReader;
015: import java.io.StringWriter;
016: import java.util.Stack;
017:
018: import junit.framework.TestCase;
019: import de.uka.ilkd.key.java.Recoder2KeY;
020: import de.uka.ilkd.key.java.Services;
021: import de.uka.ilkd.key.logic.op.*;
022: import de.uka.ilkd.key.logic.sort.Sort;
023: import de.uka.ilkd.key.parser.KeYLexer;
024: import de.uka.ilkd.key.parser.KeYParser;
025: import de.uka.ilkd.key.parser.ParserMode;
026:
027: public class TestClashFreeSubst extends TestCase {
028:
029: TermFactory tf = TermFactory.DEFAULT;
030:
031: NamespaceSet nss;
032:
033: Sort srt;
034:
035: Function f, g;
036: Function p, q;
037:
038: LogicVariable v, x, y, z;
039: Term t_v, t_x, t_y, t_z;
040:
041: ProgramVariable pv0;
042:
043: public TestClashFreeSubst(String name) {
044: super (name);
045: }
046:
047: public void setUp() {
048: nss = new NamespaceSet();
049:
050: parseDecls("\\sorts { srt; }\n" + "\\functions {\n"
051: + " srt f(srt);\n" + " srt g(srt,srt);\n" + "}\n"
052: + "\\predicates {\n" + " p(srt);\n"
053: + " q(srt,srt);\n" + "}");
054:
055: srt = lookup_sort("srt");
056:
057: f = lookup_func("f");
058: g = lookup_func("g");
059: p = lookup_func("p");
060: q = lookup_func("q");
061: pv0 = new LocationVariable(new ProgramElementName("pv0"), srt);
062: nss.variables().add(pv0);
063:
064: // The declaration parser cannot parse LogicVariables; these
065: // are normally declared in quantifiers, so we introduce them
066: // ourselves!
067: v = declareVar("v", srt);
068: t_v = tf.createVariableTerm(v);
069: x = declareVar("x", srt);
070: t_x = tf.createVariableTerm(x);
071: y = declareVar("y", srt);
072: t_y = tf.createVariableTerm(y);
073: z = declareVar("z", srt);
074: t_z = tf.createVariableTerm(z);
075: }
076:
077: Sort lookup_sort(String name) {
078: Sort s = (Sort) nss.sorts().lookup(new Name(name));
079: if (s == null) {
080: throw new RuntimeException("Sort named " + name
081: + " not found");
082: }
083: return s;
084: }
085:
086: Function lookup_func(String name) {
087: Function f = (Function) nss.functions().lookup(new Name(name));
088: if (f == null) {
089: throw new RuntimeException("Function named " + name
090: + " not found");
091: }
092: return f;
093: }
094:
095: LogicVariable declareVar(String name, Sort sort) {
096: LogicVariable v = new LogicVariable(new Name(name), sort);
097: nss.variables().add(v);
098: return v;
099: }
100:
101: private KeYParser stringDeclParser(String s) {
102: Services serv = new Services();
103: Recoder2KeY r2k = new Recoder2KeY(serv, nss);
104: r2k.parseSpecialClasses();
105: return new KeYParser(
106: ParserMode.DECLARATION,
107: new KeYLexer(new StringReader(s), null),
108: "No file. Call of parser from logic/TestClashFreeSubst.java",
109: serv, nss);
110: }
111:
112: public void parseDecls(String s) {
113: try {
114: KeYParser p = stringDeclParser(s);
115: p.decls();
116: } catch (Exception e) {
117: StringWriter sw = new StringWriter();
118: PrintWriter pw = new PrintWriter(sw);
119: e.printStackTrace(pw);
120: throw new RuntimeException("Exc while Parsing:\n" + sw);
121: }
122: }
123:
124: private KeYParser stringTermParser(String s) {
125: return new KeYParser(ParserMode.GLOBALDECL, new KeYLexer(
126: new StringReader(s), null), tf, new Services(), nss);
127: }
128:
129: public Term parseTerm(String s) {
130: try {
131: KeYParser p = stringTermParser(s);
132: return p.term();
133: } catch (Exception e) {
134: StringWriter sw = new StringWriter();
135: PrintWriter pw = new PrintWriter(sw);
136: e.printStackTrace(pw);
137: throw new RuntimeException("Exc while Parsing:\n" + sw);
138: }
139: }
140:
141: public Term parseFma(String s) {
142: try {
143: KeYParser p = stringTermParser(s);
144:
145: return p.formula();
146: } catch (Exception e) {
147: StringWriter sw = new StringWriter();
148: PrintWriter pw = new PrintWriter(sw);
149: e.printStackTrace(pw);
150: throw new RuntimeException("Exc while Parsing:\n" + sw);
151: }
152: }
153:
154: /** transform sequences all x. all y. ... bla to all x,y... . bla).
155: * no rulevars, no javaBlocks.*/
156: private Term toMulti(Term t) {
157: ToMultiVisitor v = new ToMultiVisitor();
158: t.execPostOrder(v);
159: return v.getResult();
160: }
161:
162: private class ToMultiVisitor extends Visitor {
163: private Stack subStack;
164:
165: ToMultiVisitor() {
166: subStack = new Stack();
167: }
168:
169: public void visit(Term visited) {
170: Operator op = visited.op();
171: int arity = visited.arity();
172: if (op == Op.ALL) {
173: Term top = (Term) subStack.peek();
174: if (top.op() == Op.ALL) {
175: QuantifiableVariable[] bv = new QuantifiableVariable[visited
176: .varsBoundHere(0).size()
177: + top.varsBoundHere(0).size()];
178: for (int i = 0; i < visited.varsBoundHere(0).size(); i++) {
179: bv[i] = visited.varsBoundHere(0)
180: .getQuantifiableVariable(i);
181: }
182: for (int i = 0; i < top.varsBoundHere(0).size(); i++) {
183: bv[visited.varsBoundHere(0).size() + i] = top
184: .varsBoundHere(0)
185: .getQuantifiableVariable(i);
186: }
187: subStack.pop();
188: subStack.push(tf.createQuantifierTerm(Op.ALL, bv,
189: top.sub(0)));
190: return;
191: }
192: }
193: ArrayOfQuantifiableVariable[] bv = new ArrayOfQuantifiableVariable[arity];
194: Term[] sub = new Term[arity];
195: for (int i = arity - 1; i >= 0; i--) {
196: sub[i] = (Term) (subStack.pop());
197: bv[i] = visited.varsBoundHere(i);
198: }
199: subStack.push(tf.createTerm(op, sub, bv, null));
200: }
201:
202: Term getResult() {
203: return (Term) subStack.pop();
204: }
205: }
206:
207: // Test Cases
208:
209: public void testSubst() {
210: Term s = parseTerm("f(x)");
211: Term t = parseTerm("g(v,x)");
212: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
213: assertEquals("substitution", parseTerm("g(f(x),x)"), cfs
214: .apply(t));
215: }
216:
217: public void testSubstWary() {
218: Term s = parseTerm("f(x)");
219: Term t = parseTerm("q(v,x)");
220: WaryClashFreeSubst cfs = new WaryClashFreeSubst(v, s);
221: assertEquals("substitution", parseTerm("q(f(x),x)"), cfs
222: .apply(t));
223: }
224:
225: public void testShare() {
226: Term s = parseTerm("f(x)");
227: Term t = parseTerm("g(v,f(x))");
228: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
229: assertSame("share unchanged subterms", t.sub(1), cfs.apply(t)
230: .sub(1));
231: }
232:
233: public void testShareWary() {
234: Term s = parseTerm("f(x)");
235: Term t = parseTerm("q(v,f(x))");
236: WaryClashFreeSubst cfs = new WaryClashFreeSubst(v, s);
237: assertSame("share unchanged subterms", t.sub(1), cfs.apply(t)
238: .sub(1));
239: }
240:
241: /*
242: public void testShareBound() {
243: Term s = parseTerm("f(x)");
244: Term t = parseTerm("g(v,eps v.q(x,v))");
245: ClashFreeSubst cfs = new ClashFreeSubst(v,s);
246: assertSame("sharing with bound variables",
247: t.sub(1), cfs.apply(t).sub(1));
248: }
249:
250: public void testShareAll() {
251: Term s = parseTerm("f(x)");
252: Term t = parseTerm("eps x.g(x,eps v.q(x,v))");
253: ClashFreeSubst cfs = new ClashFreeSubst(v,s);
254: assertSame("sharing whole term despite clash",
255: t, cfs.apply(t));
256: }
257: */
258:
259: public void testClash() {
260: Term s = parseTerm("f(x)");
261: Term t = parseTerm("\\exists x; q(x,v)");
262: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
263: Term res = cfs.apply(t);
264: QuantifiableVariable x1 = res.varsBoundHere(0)
265: .getQuantifiableVariable(0);
266: nss.setVariables(new Namespace(nss.variables(), x1));
267: assertEquals("clash resolution",
268: parseTerm("\\exists x1; q(x1,f(x))"), res);
269: nss.setVariables(nss.variables().parent());
270: }
271:
272: public void testSubstInSubstTerm() {
273: Term s = parseTerm("f(x)");
274: Term t = parseTerm("{\\subst y; f(v)}g(y,v)");
275: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
276: assertEquals("substitute into substitution term",
277: parseTerm("{\\subst y; f(f(x))}g(y,f(x))"), cfs
278: .apply(t));
279: }
280:
281: public void testClashInSubstTerm() {
282: Term s = parseTerm("f(x)");
283: Term t = parseTerm("{\\subst x; f(v)}g(x,v)");
284: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
285: Term res = cfs.apply(t);
286: QuantifiableVariable x1 = res.varsBoundHere(1)
287: .getQuantifiableVariable(0);
288: nss.setVariables(new Namespace(nss.variables(), x1));
289: assertEquals("clash resolution in substitution term",
290: parseTerm("{\\subst x1; f(f(x))}g(x1,f(x))"), res);
291: nss.setVariables(nss.variables().parent());
292: }
293:
294: public void testMultiSubst() {
295: Term s = parseTerm("f(x)");
296: Term t = toMulti(parseFma("\\forall y; \\forall z; q(y,g(v,z))"));
297: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
298: assertEquals(
299: "substitution on multi",
300: toMulti(parseFma("\\forall y; \\forall z; q(y,g(f(x),z))")),
301: cfs.apply(t));
302: }
303:
304: public void testMultiShareBound() {
305: Term s = parseTerm("f(x)");
306: Term t = toMulti(parseFma("\\forall y; \\forall v; \\forall z; q(y,g(v,z))"));
307: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
308: assertSame("sharing on multi", cfs.apply(t), t);
309: }
310:
311: // disabled. multi vars at quantifier currently not supported by
312: // KeY and feature of data structures suppressed by TermFactory. /AR 040420
313: public void xtestMultiClash() {
314: Term s = parseTerm("f(x)");
315: Term t = toMulti(parseFma("\\forall y; \\forall x; \\forall z; q(g(x,y),g(v,z))"));
316: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
317: Term res = cfs.apply(t);
318: QuantifiableVariable x1 = res.varsBoundHere(0)
319: .getQuantifiableVariable(1);
320: nss.setVariables(new Namespace(nss.variables(), x1));
321: assertEquals(
322: "clash resolution in multi term",
323: toMulti(parseTerm("\\forall y; \\forall x1; \\forall z; q(g(x1,y),g(f(x),z))")),
324: res);
325: nss.setVariables(nss.variables().parent());
326: }
327:
328: // disabled. multi vars at quantifier currently not supported by
329: // KeY and feature of data structures suppressed by TermFactory. /AR 040420
330: public void xtestMultiClash1() {
331: Term s = parseTerm("f(x)");
332: Term t = toMulti(parseFma("\\forall y; \\forall x;\\forall z; q(g(x,y),g(v,z))"));
333: ClashFreeSubst cfs = new ClashFreeSubst(v, s);
334: Term res = cfs.apply(t);
335: QuantifiableVariable x1 = res.varsBoundHere(0)
336: .getQuantifiableVariable(2);
337: nss.setVariables(new Namespace(nss.variables(), x1));
338: assertEquals("clash resolution in multi term",
339: toMulti(parseTerm("q(g(x1,y),g(f(x),z))")), res.sub(0));
340: nss.setVariables(nss.variables().parent());
341: }
342:
343: public void testWary0() {
344: Term s = parseTerm("f(pv0)");
345: Term t = parseTerm("q(v,x)");
346: WaryClashFreeSubst cfs = new WaryClashFreeSubst(v, s);
347: assertEquals("substitution", parseTerm("q(f(pv0),x)"), cfs
348: .apply(t));
349: }
350:
351: public void testWary1() {
352: Term s = parseTerm("f(pv0)");
353: Term t = parseTerm("q(v,x) & {pv0:=v}q(x,x)");
354: WaryClashFreeSubst cfs = new WaryClashFreeSubst(v, s);
355: assertEquals("substitution",
356: parseTerm("q(f(pv0),x) & {pv0:=f(pv0)}q(x,x)"), cfs
357: .apply(t));
358: }
359:
360: public void testWary2() {
361: Term s = parseTerm("f(pv0)");
362: Term t = parseTerm("q(v,x) & {pv0:=v}q(x,v)");
363: WaryClashFreeSubst cfs = new WaryClashFreeSubst(v, s);
364: Term res = cfs.apply(t);
365: QuantifiableVariable x1 = res.varsBoundHere(1)
366: .getQuantifiableVariable(0);
367: nss.setVariables(new Namespace(nss.variables(), x1));
368: assertEquals("substitution", parseTerm("{\\subst " + x1.name()
369: + "; f(pv0)} ( q(f(pv0),x) & {pv0:=f(pv0)}q(x,"
370: + x1.name() + ") )"), cfs.apply(t));
371: nss.setVariables(nss.variables().parent());
372: }
373:
374: public void testClashInIfEx() {
375: Term ifEx = parseTerm("\\ifEx x; (x=v) \\then (v=x) \\else (false)");
376: assertEquals(ifEx.freeVars().size(), 1);
377: assertSame(ifEx.freeVars().iterator().next(), v);
378:
379: Term subst = parseTerm("x");
380: ClashFreeSubst cfs = new ClashFreeSubst(v, subst);
381: Term res = cfs.apply(ifEx);
382:
383: assertEquals(res.freeVars().size(), 1);
384: assertSame(res.freeVars().iterator().next(), x);
385: }
386: }
|