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: package de.uka.ilkd.key.logic;
009:
010: import de.uka.ilkd.key.java.Services;
011: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
012: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
013: import de.uka.ilkd.key.logic.op.*;
014: import de.uka.ilkd.key.logic.sort.Sort;
015:
016: /**
017: * <p>Use this class if you intend to build complex terms by hand. It is
018: * more convenient than the @link{TermFactory} class.</p>
019: *
020: * <p>Most convenient is its use when being subclassed. Therefore move the term
021: * constructing methods of your application to a separate class and let the new
022: * class extend the TermBuilder.</p>
023: *
024: * <p>Attention: some methods of this class try to simplify some terms. So if you
025: * want to be sure that the term looks exactly as you built it, you
026: * will have to use the TermFactory.</p>
027: */
028: public class TermBuilder {
029:
030: public static final TermBuilder DF = new TermBuilder();
031:
032: protected final static TermFactory tf = TermFactory.DEFAULT;
033:
034: private final static Term tt = TermFactory.DEFAULT
035: .createJunctorTerm(Op.TRUE);
036: private final static Term ff = TermFactory.DEFAULT
037: .createJunctorTerm(Op.FALSE);
038:
039: public TermBuilder() {
040: }
041:
042: public Term TRUE(Services services) {
043: return services.getTypeConverter().getBooleanLDT()
044: .getTrueTerm();
045: }
046:
047: public Term FALSE(Services services) {
048: return services.getTypeConverter().getBooleanLDT()
049: .getFalseTerm();
050: }
051:
052: public Term tt() {
053: return tt;
054: }
055:
056: public Term ff() {
057: return ff;
058: }
059:
060: // To be more general: shouldn't lv be a QuantifiableVariable? Sure!
061: public Term all(QuantifiableVariable lv, Term t2) {
062: if (!t2.freeVars.contains(lv))
063: return t2;
064: return tf.createQuantifierTerm(Op.ALL, lv, t2);
065: }
066:
067: public Term all(QuantifiableVariable[] lv, Term t2) {
068: Term result = t2;
069: for (int i = lv.length - 1; i >= 0; i--) {
070: result = all(lv[i], result);
071: }
072: return result;
073: }
074:
075: public Term ex(QuantifiableVariable lv, Term t2) {
076: if (!t2.freeVars.contains(lv))
077: return t2;
078: return tf.createQuantifierTerm(Op.EX, lv, t2);
079: }
080:
081: public Term ex(QuantifiableVariable[] lv, Term t2) {
082: Term result = t2;
083: for (int i = lv.length - 1; i >= 0; i--) {
084: result = ex(lv[i], result);
085: }
086: return result;
087: }
088:
089: public Term not(Term t) {
090: return tf.createJunctorTermAndSimplify(Op.NOT, t);
091: }
092:
093: public Term and(Term t1, Term t2) {
094: return tf.createJunctorTermAndSimplify(Op.AND, t1, t2);
095: }
096:
097: public Term and(Term[] subTerms) {
098: Term result = tt();
099: for (int i = 0; i < subTerms.length; i++) {
100: result = and(result, subTerms[i]);
101: }
102:
103: return result;
104: }
105:
106: public Term and(ListOfTerm subTerms) {
107: Term result = tt();
108: IteratorOfTerm it = subTerms.iterator();
109: while (it.hasNext()) {
110: result = and(result, it.next());
111: }
112: return result;
113: }
114:
115: public Term or(Term t1, Term t2) {
116: return tf.createJunctorTermAndSimplify(Op.OR, t1, t2);
117: }
118:
119: public Term or(Term[] subTerms) {
120: Term result = ff();
121: for (int i = 0; i < subTerms.length; i++) {
122: result = or(result, subTerms[i]);
123: }
124:
125: return result;
126: }
127:
128: public Term or(ListOfTerm subTerms) {
129: Term result = ff();
130: IteratorOfTerm it = subTerms.iterator();
131: while (it.hasNext()) {
132: result = or(result, it.next());
133: }
134: return result;
135: }
136:
137: public Term imp(Term t1, Term t2) {
138: return tf.createJunctorTermAndSimplify(Op.IMP, t1, t2);
139: }
140:
141: public Term equals(Term t1, Term t2) {
142: if (t1.sort() == Sort.FORMULA || t2.sort() == Sort.FORMULA) {
143: throw new IllegalArgumentException(
144: "Equals is defined betweens terms, not forumulas: "
145: + t1 + ", " + t2);
146: }
147: if (t1.equals(t2))
148: return tt();
149: return tf.createEqualityTerm(t1, t2);
150: }
151:
152: public Term equiv(Term t1, Term t2) {
153: if (t1.sort() != Sort.FORMULA || t2.sort() != Sort.FORMULA) {
154: throw new IllegalArgumentException(
155: "Equivalence is defined on formulas not terms: "
156: + t1 + ", " + t2);
157: }
158: return tf.createJunctorTermAndSimplify(Op.EQV, t1, t2);
159: }
160:
161: public Term geq(Term t1, Term t2, Services services) {
162: final IntegerLDT integerLDT = services.getTypeConverter()
163: .getIntegerLDT();
164: return tf.createFunctionTerm(integerLDT.getGreaterOrEquals(),
165: t1, t2);
166: }
167:
168: public Term gt(Term t1, Term t2, Services services) {
169: final IntegerLDT integerLDT = services.getTypeConverter()
170: .getIntegerLDT();
171: return tf.createFunctionTerm(integerLDT.getGreaterThan(), t1,
172: t2);
173: }
174:
175: public Term lt(Term t1, Term t2, Services services) {
176: final IntegerLDT integerLDT = services.getTypeConverter()
177: .getIntegerLDT();
178: return tf.createFunctionTerm(integerLDT.getLessThan(), t1, t2);
179: }
180:
181: public Term leq(Term t1, Term t2, Services services) {
182: final IntegerLDT integerLDT = services.getTypeConverter()
183: .getIntegerLDT();
184: return tf.createFunctionTerm(integerLDT.getLessOrEquals(), t1,
185: t2);
186: }
187:
188: public Term zero(Services services) {
189: final IntegerLDT integerLDT = services.getTypeConverter()
190: .getIntegerLDT();
191: return integerLDT.translateLiteral(new IntLiteral(0));
192: }
193:
194: public Term one(Services services) {
195: final IntegerLDT integerLDT = services.getTypeConverter()
196: .getIntegerLDT();
197: return integerLDT.translateLiteral(new IntLiteral(1));
198: }
199:
200: public Term NULL(Services services) {
201: return services.getJavaInfo().getNullTerm();
202: }
203:
204: public Term array(Term ref, Term idx) {
205: if (ref == null || idx == null) {
206: throw new TermCreationException(
207: "Tried to build an array access "
208: + "term without providing an "
209: + (ref == null ? "array reference."
210: : "index.") + "(" + ref + "[" + idx
211: + "])");
212: }
213: return tf.createArrayTerm(ArrayOp.getArrayOp(ref.sort()), ref,
214: idx);
215: }
216:
217: public Term dot(Term o, ProgramVariable a) {
218: return tf.createAttributeTerm(a, o);
219: }
220:
221: public Term var(LogicVariable v) {
222: return tf.createVariableTerm(v);
223: }
224:
225: public Term var(ProgramVariable v) {
226: if (!v.isStatic() && v.isMember()) {
227: throw new IllegalArgumentException(
228: "Wrong programvariable kind.");
229: }
230: return tf.createVariableTerm(v);
231: }
232:
233: public Term var(ParsableVariable v) {
234: if (v instanceof ProgramVariable) {
235: return var((ProgramVariable) v);
236: } else if (v instanceof LogicVariable) {
237: return var((LogicVariable) v);
238: } else {
239: throw new IllegalArgumentException(
240: "Wrong parsablevariable kind.");
241: }
242: }
243:
244: public Term func(TermSymbol op) {
245: return tf.createFunctionTerm(op);
246: }
247:
248: public Term func(TermSymbol op, Term s) {
249: return tf.createFunctionTerm(op, s);
250: }
251:
252: public Term func(TermSymbol op, Term s1, Term s2) {
253: return tf.createFunctionTerm(op, s1, s2);
254: }
255:
256: public Term func(TermSymbol op, Term[] s) {
257: return tf.createFunctionTerm(op, s);
258: }
259:
260: public Term box(JavaBlock jb, Term t) {
261: return tf.createBoxTerm(jb, t);
262: }
263:
264: public Term dia(JavaBlock jb, Term t) {
265: return tf.createDiamondTerm(jb, t);
266: }
267:
268: public Term ife(Term cond, Term _then, Term _else) {
269: return tf.createIfThenElseTerm(cond, _then, _else);
270: }
271:
272: public TermFactory tf() {
273: return tf;
274: }
275:
276: /**
277: * builds a Term from a number, given by a String
278: *
279: * @param services Services which contains the number-functions
280: * @param numberString String representing an integer
281: * @return Term in Z-Notation representing the given number
282: */
283: public Term zTerm(Services services, String numberString) {
284: Operator v;
285: Term t;
286: boolean negate = false;
287: int j = 0;
288:
289: Namespace funcNS = services.getNamespaces().functions();
290:
291: if (numberString.substring(0, 1).equals("-")) {
292: negate = true;
293: j = 1;
294: }
295: v = (Function) funcNS.lookup(new Name("#"));
296: t = func((Function) v);
297: v = (Function) funcNS.lookup(new Name(numberString.substring(j,
298: j + 1)));
299: t = func((Function) v, t);
300: for (int i = j + 1; i < numberString.length(); i++) {
301: v = (Function) funcNS.lookup(new Name(numberString
302: .substring(i, i + 1)));
303: t = func((Function) v, t);
304: }
305: if (negate) {
306: v = (Function) funcNS.lookup(new Name("neglit"));
307: t = func((Function) v, t);
308: }
309: v = (Function) funcNS.lookup(new Name("Z"));
310: t = func((Function) v, t);
311: return t;
312: }
313:
314: }
|