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 junit.framework.TestCase;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
017: import de.uka.ilkd.key.logic.sort.Sort;
018:
019: /** class tests the constraint classes
020: */
021:
022: public class TestConstraint extends TestCase {
023:
024: TermFactory tf = TermFactory.DEFAULT;
025:
026: private Sort sort1 = new PrimitiveSort(new Name("S1"));
027: private Sort sort2 = new PrimitiveSort(new Name("S2"));
028:
029: private Services DEFAULT = null;
030:
031: Function p = new RigidFunction(new Name("p"), Sort.FORMULA,
032: new Sort[] { sort1 });
033: //p(:S1):BOOL
034:
035: Function q = new RigidFunction(new Name("q"), Sort.FORMULA,
036: new Sort[] { sort1, sort1, sort1 });
037:
038: Function r = new RigidFunction(new Name("r"), Sort.FORMULA,
039: new Sort[] { sort1, sort2 });
040: //r(:S1, :S2):BOOL
041: Function r0 = new RigidFunction(new Name("r0"), sort1, new Sort[] {
042: sort1, sort1 });
043: //r(:S1, :S1):S1
044: Function f = new RigidFunction(new Name("f"), sort1,
045: new Sort[] { sort1 });
046: // f(:S1):S1
047: Function h = new RigidFunction(new Name("h"), sort1,
048: new Sort[] { sort1 });
049: // h(:S1):S1
050: Function g = new RigidFunction(new Name("g"), sort1, new Sort[] {
051: sort1, sort1 });
052: // g(:S1,S1):S1
053: Function con = new RigidFunction(new Name("c"), sort1,
054: new PrimitiveSort[0]);
055: Metavariable x = new Metavariable(new Name("x"), sort1); //x:S1
056: Metavariable z = new Metavariable(new Name("z"), sort1); //z:S1
057: Metavariable v = new Metavariable(new Name("v"), sort1); //v:S1
058: Metavariable y = new Metavariable(new Name("y"), sort1); //y:S1
059: Metavariable w = new Metavariable(new Name("w"), sort2); //w:S2
060: Metavariable w0 = new Metavariable(new Name("w0"), sort1); //w:S1
061:
062: LogicVariable lv0 = new LogicVariable(new Name("lv0"), sort1); //lv0:S1
063: LogicVariable lv1 = new LogicVariable(new Name("lv1"), sort1); //lv1:S1
064:
065: public TestConstraint(String name) {
066: super (name);
067: }
068:
069: private Term term_p(TermSymbol var) {
070: Term t_x = tf.createFunctionTerm(var, new Term[] {});
071: Term t_px = tf.createFunctionTerm(p, new Term[] { t_x });
072: return t_px;
073: }
074:
075: private Term term_r(TermSymbol o1S1, TermSymbol o2S2) {
076: Term t_x = tf.createFunctionTerm(o1S1, new Term[] {});
077: Term t_w = tf.createFunctionTerm(o2S2, new Term[] {});
078: return tf.createFunctionTerm(r, new Term[] { t_x, t_w });
079: }
080:
081: public void setUp() {
082:
083: }
084:
085: public void testSatisfiableConstraint1() {
086: Constraint c = Constraint.BOTTOM.unify(term_p(x), term_p(con),
087: DEFAULT);
088: assertTrue(c.isSatisfiable()
089: && ((EqualityConstraint) c).valueOf(x).equals(
090: tf.createFunctionTerm(con, new Term[] {})));
091: }
092:
093: public void testSatisfiableConstraint2() {
094: Constraint c = Constraint.BOTTOM.unify(term_r(x, w), term_r(
095: con, w), DEFAULT);
096: assertTrue(c.isSatisfiable()
097: && c != Constraint.TOP
098: && ((EqualityConstraint) c).valueOf(x).equals(
099: tf.createFunctionTerm(con, new Term[] {}))
100: && ((EqualityConstraint) c).isDefined(w) == false);
101: }
102:
103: // unify(q(X,f(Y),Z),q(Z,X,Y))
104: public void testCycle() {
105: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
106: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
107: Term t1_fy = tf.createFunctionTerm(f, new Term[] { t1_y });
108: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
109: Term t2_x = tf.createFunctionTerm(x, new Term[] {});
110: Term t2_y = tf.createFunctionTerm(y, new Term[] {});
111: Term t2_z = tf.createFunctionTerm(z, new Term[] {});
112: Constraint c = Constraint.BOTTOM.unify(tf.createFunctionTerm(q,
113: new Term[] { t1_x, t1_fy, t1_z }),
114: tf.createFunctionTerm(q,
115: new Term[] { t2_z, t2_x, t2_y }), DEFAULT);
116: assertTrue(c.isSatisfiable() == false);
117: assertSame(c, Constraint.TOP);
118: }
119:
120: // unify(q(X,Y,Z),q(Z,X,Y))
121: public void testMVCycle() {
122: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
123: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
124: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
125: Term t2_x = tf.createFunctionTerm(x, new Term[] {});
126: Term t2_y = tf.createFunctionTerm(y, new Term[] {});
127: Term t2_z = tf.createFunctionTerm(z, new Term[] {});
128: Constraint c = Constraint.BOTTOM.unify(tf.createFunctionTerm(q,
129: new Term[] { t1_x, t1_y, t1_z }),
130: tf.createFunctionTerm(q,
131: new Term[] { t2_z, t2_x, t2_y }), DEFAULT);
132: assertTrue(c.isSatisfiable() == true);
133: }
134:
135: // join constraint {X=r0(Y,Z),Y=con} {Z=f(V),V=con}
136: public void testJoinWithoutSubSume() {
137: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
138: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
139: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
140: Term t2_v = tf.createFunctionTerm(v, new Term[] {});
141: Term t2_z = tf.createFunctionTerm(z, new Term[] {});
142: Constraint c1 = Constraint.BOTTOM.unify(t1_x, tf
143: .createFunctionTerm(r0, new Term[] { t1_y, t1_z }),
144: DEFAULT);
145: c1 = c1.unify(t1_y, tf.createFunctionTerm(con, new Term[] {}),
146: DEFAULT);
147: Constraint c2 = Constraint.BOTTOM.unify(t2_z, tf
148: .createFunctionTerm(f, new Term[] { t2_v }), DEFAULT);
149: c2 = c2.unify(t2_v, tf.createFunctionTerm(con, new Term[] {}),
150: DEFAULT);
151:
152: Constraint c3 = Constraint.BOTTOM.unify(t1_x, tf
153: .createFunctionTerm(r0, new Term[] { t1_y, t1_z }),
154: DEFAULT);
155: c3 = c3.unify(t1_y, tf.createFunctionTerm(con, new Term[] {}),
156: DEFAULT);
157: c3 = c3.unify(t2_z, tf.createFunctionTerm(f,
158: new Term[] { t2_v }), DEFAULT);
159: c3 = c3.unify(t2_v, tf.createFunctionTerm(con, new Term[] {}),
160: DEFAULT);
161:
162: Constraint c4 = c1.join(c2, DEFAULT);
163: assertSame(c4, c4.join(c3, DEFAULT));
164: }
165:
166: // join constraint {X=r0(Y,Z),Y=con} {X=r0(con,Z)}
167: public void testJoinWithSubSume() {
168: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
169: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
170: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
171: Term t2_x = tf.createFunctionTerm(x, new Term[] {});
172: Term t2_z = tf.createFunctionTerm(z, new Term[] {});
173: Constraint c1 = Constraint.BOTTOM.unify(t1_x, tf
174: .createFunctionTerm(r0, new Term[] { t1_y, t1_z }),
175: DEFAULT);
176: c1 = c1.unify(t1_y, tf.createFunctionTerm(con, new Term[] {}),
177: DEFAULT);
178: Constraint c2 = Constraint.BOTTOM.unify(t2_x, tf
179: .createFunctionTerm(r0,
180: new Term[] {
181: tf.createFunctionTerm(con,
182: new Term[] {}), t2_z }),
183: DEFAULT);
184:
185: BooleanContainer booleanCon = new BooleanContainer();
186: assertEquals(c1.join(c2, DEFAULT, booleanCon), c1);
187: assertTrue("Container says false instead of true", booleanCon
188: .val());
189: }
190:
191: public void testElmarsConstraint() {
192: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
193: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
194: Term t1_fy = tf.createFunctionTerm(f, new Term[] { t1_y });
195: Term t1_w = tf.createFunctionTerm(w0, new Term[] {});
196: Term t1_gyw = tf.createFunctionTerm(g,
197: new Term[] { t1_y, t1_w });
198: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
199:
200: Term t1_v = tf.createFunctionTerm(v, new Term[] {});
201:
202: Term t1_hv = tf.createFunctionTerm(h, new Term[] { t1_v });
203: Term t1_gzhv = tf.createFunctionTerm(g, new Term[] { t1_z,
204: t1_hv });
205: Term t1_fv = tf.createFunctionTerm(f, new Term[] { t1_v });
206: Term t1_fx = tf.createFunctionTerm(f, new Term[] { t1_x });
207: Term t1_ffx = tf.createFunctionTerm(f, new Term[] { t1_fx });
208:
209: Term t1_fz = tf.createFunctionTerm(f, new Term[] { t1_z });
210: Term t1_ffz = tf.createFunctionTerm(f, new Term[] { t1_fz });
211: Term t1_hffz = tf.createFunctionTerm(h, new Term[] { t1_ffz });
212: Constraint c = Constraint.BOTTOM.unify(t1_x, t1_fy, DEFAULT);
213: Constraint res = Constraint.BOTTOM.unify(t1_x, t1_fy, DEFAULT);
214: c = c.unify(t1_gyw, t1_gzhv, DEFAULT).unify(t1_fv, t1_ffx,
215: DEFAULT).unify(t1_w, t1_hffz, DEFAULT);
216: res = res.unify(t1_x, t1_fy, DEFAULT)
217: .unify(t1_y, t1_z, DEFAULT).unify(t1_v, t1_fx, DEFAULT)
218: .unify(t1_w, t1_hv, DEFAULT);
219: assertSame(c.join(res, DEFAULT), c); // precond. if c subsumes res c==res
220: }
221:
222: // intersect {X=r0(Y,Z),Y=con} {X=r0(con,Z)}
223: public void testIntersectionConstraint0() {
224: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
225: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
226: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
227: Term t2_x = tf.createFunctionTerm(x, new Term[] {});
228: Term t2_z = tf.createFunctionTerm(z, new Term[] {});
229: Constraint c1 = Constraint.BOTTOM.unify(t1_x, tf
230: .createFunctionTerm(r0, new Term[] { t1_y, t1_z }),
231: DEFAULT);
232: c1 = c1.unify(t1_y, tf.createFunctionTerm(con, new Term[] {}),
233: DEFAULT);
234: Constraint c2 = Constraint.BOTTOM.unify(t2_x, tf
235: .createFunctionTerm(r0,
236: new Term[] {
237: tf.createFunctionTerm(con,
238: new Term[] {}), t2_z }),
239: DEFAULT);
240:
241: ConstraintContainer cc = new ConstraintContainer();
242:
243: assertSame(IntersectionConstraint.intersect(c1, c2, cc), c2);
244: assertSame(cc.val(), c2);
245: assertSame(IntersectionConstraint.intersect(c2, c1, cc), c2);
246: assertSame(cc.val(), Constraint.TOP);
247: assertSame(IntersectionConstraint.intersect(Constraint.TOP, c1,
248: cc), c1);
249: assertSame(cc.val(), c1);
250: assertSame(IntersectionConstraint.intersect(c2, Constraint.TOP,
251: cc), c2);
252: assertSame(cc.val(), Constraint.TOP);
253: assertSame(IntersectionConstraint.intersect(Constraint.BOTTOM,
254: c2, cc), Constraint.BOTTOM);
255: assertSame(cc.val(), Constraint.TOP);
256: assertSame(IntersectionConstraint.intersect(c1,
257: Constraint.BOTTOM, cc), Constraint.BOTTOM);
258: assertSame(cc.val(), Constraint.BOTTOM);
259: }
260:
261: // intersect {X=r0(Y,Z)} {X=r0(con,Z)}
262: public void testIntersectionConstraint1() {
263: Term t1_x = tf.createFunctionTerm(x, new Term[] {});
264: Term t1_y = tf.createFunctionTerm(y, new Term[] {});
265: Term t1_z = tf.createFunctionTerm(z, new Term[] {});
266: Term t2_x = tf.createFunctionTerm(x, new Term[] {});
267: Term t2_z = tf.createFunctionTerm(z, new Term[] {});
268: Constraint c1 = Constraint.BOTTOM.unify(t1_x, tf
269: .createFunctionTerm(r0, new Term[] { t1_y, t1_z }),
270: DEFAULT);
271: Constraint c2 = Constraint.BOTTOM.unify(t2_x, tf
272: .createFunctionTerm(r0,
273: new Term[] {
274: tf.createFunctionTerm(con,
275: new Term[] {}), t2_z }),
276: DEFAULT);
277:
278: ConstraintContainer cc = new ConstraintContainer();
279: ConstraintContainer cc2 = new ConstraintContainer();
280:
281: Constraint c3 = IntersectionConstraint.intersect(c1, c2, cc);
282: assertSame(cc.val(), c2);
283: IntersectionConstraint.intersect(c2, c3, cc);
284: assertSame(cc.val(), c1);
285: IntersectionConstraint.intersect(c1, c3, cc);
286: assertSame(cc.val(), c2);
287: assertSame(IntersectionConstraint.intersect(c3, c1, cc), c3);
288: assertSame(cc.val(), Constraint.TOP);
289: assertSame(IntersectionConstraint.intersect(c3, c2, cc), c3);
290: assertSame(cc.val(), Constraint.TOP);
291: assertSame(IntersectionConstraint.intersect(c3, c3, cc), c3);
292: assertSame(cc.val(), Constraint.TOP);
293: assertSame(IntersectionConstraint.intersect(c3,
294: IntersectionConstraint
295: .intersect(Constraint.TOP, c3, cc), cc2), c3);
296: assertSame(cc2.val(), Constraint.TOP);
297: assertSame(IntersectionConstraint.intersect(c3, cc.val(), cc2),
298: c3);
299: assertSame(cc2.val(), Constraint.TOP);
300: assertSame(IntersectionConstraint.intersect(c3, Constraint.TOP,
301: cc), c3);
302: assertSame(cc.val(), Constraint.TOP);
303:
304: assertSame(c3.join(Constraint.TOP, DEFAULT), Constraint.TOP);
305: assertSame(IntersectionConstraint.intersect(c3, c3.join(
306: Constraint.BOTTOM, DEFAULT)), c3);
307: IntersectionConstraint.intersect(c3.join(Constraint.BOTTOM,
308: DEFAULT), c3, cc);
309: assertSame(cc.val(), Constraint.TOP);
310: assertSame(Constraint.TOP.join(c3, DEFAULT), Constraint.TOP);
311:
312: c3 = c3.join(c3, DEFAULT);
313: assertSame(IntersectionConstraint.intersect(c3, c1), c3);
314: assertSame(IntersectionConstraint.intersect(c3, c1), c3);
315: }
316:
317: // "all lv0. all lv1. p(lv1)" and "all lv1. all lv0. p(lv1)"
318: // should not unify if the term "p(lv1)" is shared
319: public void testBoundVariablesBug() {
320: Term p_lv1 = tf.createFunctionTerm(p, new Term[] { tf
321: .createVariableTerm(lv1) });
322:
323: Term _term0 = tf.createQuantifierTerm(Op.ALL, lv1, p_lv1);
324: Term term0 = tf.createQuantifierTerm(Op.ALL, lv0, _term0);
325:
326: Term _term1 = tf.createQuantifierTerm(Op.ALL, lv0, p_lv1);
327: Term term1 = tf.createQuantifierTerm(Op.ALL, lv1, _term1);
328:
329: assertSame("Terms " + term0 + " and " + term1
330: + " should not be unifiable\n", Constraint.BOTTOM
331: .unify(term0, term1, DEFAULT), Constraint.TOP);
332: }
333:
334: public static void main(String[] args) {
335: new TestConstraint("").testSatisfiableConstraint2();
336: }
337:
338: }
|