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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.decproc.smtlib;
019:
020: import java.util.HashSet;
021: import java.util.Vector;
022:
023: /** Represents a formula as defined in the SMT-Lib specification, and specialized in one of the
024: * AUFLIA sublogics. These are QF_AUFLIA and AUFLIA, whereas QF_AUFLIA is the quantifier free
025: * version of AUFLIA. Thereby a formula represents an object which can be assigned a truth
026: * value, i.e. one predicate or many logical connected predicates.
027: * <p>
028: * This class is abstract because it is intended as a frame for realizing subclasses which
029: * specialize in representing one class of predicates in (QF_)-AUFLIA (e.g. uninterpreted predicates).
030: * <p>
031: * Formulae are immutable; their attribute values cannot be changed after they are created.
032: * <p>
033: * This class also contains methods with protected access intended to be used by realizing
034: * subclasses for convenience, as well as methods to access the lists of all uninterpreted functions
035: * and predicates contained in this formula, which are provided for the simple integration of terms
036: * and formulae and into benchmarks.
037: *
038: * @author akuwertz
039: *
040: * @version 1.5, 12/06/2005 (Restructuring and further commenting)
041: *
042: * @see <a href="http://goedel.cs.uiowa.edu/smtlib/logics/QF_AUFLIA.smt">QF_AUFLIA</a>
043: * @see <a href="http://goedel.cs.uiowa.edu/smtlib/logics/AUFLIA.smt">AUFLIA</a>
044: * @see <a href="http://goedel.cs.uiowa.edu/smtlib">SMT-LIB</a>
045: */
046:
047: public abstract class Formula {
048:
049: /** The top-level operator of this <tt>Formula</tt> */
050: private final String op;
051:
052: /** The array of subformulae of this <tt>Formula</tt> */
053: private final Formula[] subformulae;
054:
055: /** A template <tt>Fomula</tt> array assigned to <tt>subformulae</tt> if this <tt>Formula</tt> has no
056: * subformulae. This shared object is intended to lower memory footprint */
057: private static final Formula[] emptySubformulae = new Formula[0];
058:
059: /** The array of subterms of this <tt>Formula</tt> */
060: private final Term[] subterms;
061:
062: /** A template <tt>Term</tt> array assigned to <tt>subterms</tt> if this <tt>Formula</tt> has no
063: * subterms. This shared object is intended to lower memory footprint */
064: private static final Term[] emptySubterms = new Term[0];
065:
066: /** The <tt>Vector</tt> of all uninterpreted functions contained in this <tt>Formula</tt> */
067: private final Vector uninterFuncs;
068:
069: /** The <tt>Vector</tt> of all uninterpreted predicates contained in this <tt>Formula</tt> */
070: private final Vector uninterPreds;
071:
072: /** A template <tt>Vector</tt> assigned to the <tt>Formula</tt> attributes which store the
073: * uninterpreted functions and predicates of this <tt>Formula</tt>, if these fields are empty.
074: * This shared object is intended to lower memory footprint */
075: private static final Vector emptyVector = new Vector();
076:
077: /** The cached hash code for this <tt>Formula</tt> */
078: private final int hashCode;
079:
080: /* Constructor */
081:
082: /** Sole constructor. For invocation by constructors of realizing subclasses.
083: * <p>
084: * This explicit constructor sets the internal fields to the specified values or rather to
085: * values computed out of the given ones. Thereby the top-level operator and the subformulae
086: * and subterms are set directly, whereby the <tt>Vector</tt> of uninterpreted predicates and
087: * functions respectively are computed out of the uninterpreted predicates and functions
088: * contained in the subformulae and subterms.<br>
089: * Therefor all <tt>Formula</tt>e and <tt>Term</tt>s contained as subelements are searched for
090: * uninterpreted predicates (and functions respectively) and the results are merged into a
091: * <tt>Vector</tt>, eleminating duplicate entries.<br>
092: * The <tt>boolean</tt> <tt>addThisUip</tt> is a flag serving as indicator to the constructor
093: * that the calling subclass instance also wishes to be added to the <tt>Vector</tt> of
094: * uninterpreted predicates. If it is set to <tt>true</tt>, the calling instance will be
095: * added to the <tt>Vector</tt> of uninterpreted predicates as its first element.
096: * <p>
097: * This implementation checks for null pointers in the specified arguments. If a null pointer
098: * is found in the top-level operator <tt>op</tt>, all fields will be set to <tt>null</tt>
099: * without throwing any exceptions. This is done to enable realizing subclasses to throw
100: * specific exceptions on their part. It implicates that every subclass realizing this class
101: * must check <tt>op</tt> for being a null pointer, and, if so, throw an exception. Otherwise
102: * the methods defined in this class could fail with a <tt>NullPointerException</tt>, if called
103: * on the created subclass instance.<br>
104: * The same holds for the <tt>Formula</tt>e and <tt>Term</tt>s contained in the subformulae and
105: * subterms arrays. If one of the specified arrays contains any null pointers, all fields of
106: * this <tt>Formula</tt> instance will become undefined, without throwing an exception.
107: * Realizing subclasses therefore have to check or ensure that <tt>forms</tt> and
108: * <tt>terms</tt> contain no null pointers; otherwise the methods defined in this class could
109: * fail with a <tt>NullPointerException</tt>.<br>
110: * In contrary to this, null pointers are allowed for the array objects theirselves. This is done for
111: * convenience and has to same effects as empty arrays would have.
112: *
113: * @param operator the top-level operator of this <tt>Formula</tt>
114: * @param forms the array of subformulae for this <tt>Formula</tt>
115: * @param terms the array of subterms for this <tt>Formula</tt>
116: * @param addThisUip a flag; if set to <tt>true</tt>, the calling subclass instance will be
117: * added the to uninterpreted predicate <tt>Vector</tt> of this <tt>Formula</tt>
118: */
119: protected Formula(String operator, Formula[] forms, Term[] terms,
120: boolean addThisUip) {
121:
122: if (operator == null) {
123: op = null;
124: subformulae = null;
125: subterms = null;
126: uninterFuncs = uninterPreds = null;
127: hashCode = 0;
128: // Handling of this null pointer situation has to be done by subclass
129: return;
130: }
131: op = operator;
132:
133: // Null pointer for forms or terms is allowed for convenience
134: // Given arrays are cloned for immutability (exclusiveness)
135: if (forms == null || forms.length == 0)
136: subformulae = emptySubformulae;
137: else
138: subformulae = (Formula[]) forms.clone();
139: if (terms == null || terms.length == 0)
140: subterms = emptySubterms;
141: else
142: subterms = (Term[]) terms.clone();
143:
144: // Estimate capacity of new uif and uip Vectors to reduce reallocation effects to one
145: int estSizeUip = 0, estSizeUif = 0;
146: Vector[] uipInSubforms = new Vector[subformulae.length];
147: Vector[] uifInSubforms = new Vector[subformulae.length];
148: Vector[] uipInSubterms = new Vector[subterms.length];
149: Vector[] uifInSubterms = new Vector[subterms.length];
150:
151: try {
152: for (int i = 0; i < subformulae.length; i++) {
153: uipInSubforms[i] = subformulae[i].getUIPredicates();
154: uifInSubforms[i] = subformulae[i].getUIF();
155: estSizeUip += uipInSubforms[i].size();
156: estSizeUif += uifInSubforms[i].size();
157: }
158: for (int i = 0; i < subterms.length; i++) {
159: uipInSubterms[i] = subterms[i].getUIPredicatesIteTerm();
160: uifInSubterms[i] = subterms[i].getUIF();
161: estSizeUip += uipInSubterms[i].size();
162: estSizeUif += uifInSubterms[i].size();
163: }
164: } catch (NullPointerException e) {
165: uninterFuncs = uninterPreds = null;
166: hashCode = 0;
167: // Handling of this null pointer situation has to be done by subclass
168: return;
169: }
170:
171: // Compute Vector of uninterpreted predicates contained in this Formula
172: if (!addThisUip && estSizeUip == 0) {
173: // If no uninterpreted predicates contained, use empty template Vector
174: uninterPreds = emptyVector;
175: } else {
176: // Create new Vector of appropriate size and prepare the HashSet for function names
177: HashSet contPredNames = new HashSet(estSizeUip + 1);
178: Vector addUips;
179: if (!addThisUip)
180: addUips = new Vector(estSizeUip);
181: // If addThisUip is true, make sure uninterPreds contains a refenrence to itself
182: else {
183: addUips = new Vector(estSizeUip + 1);
184: addUips.add(this );
185: contPredNames.add(op);
186: }
187: // Compute contained ui predicates
188: Vector uipVector;
189: for (int i = 0; i < uipInSubforms.length; i++) {
190: uipVector = uipInSubforms[i];
191: for (int j = 0; j < uipVector.size(); j++) {
192: if (contPredNames.add(((Formula) uipVector.get(j))
193: .getOp())) {
194: addUips.add(uipVector.get(j));
195: }
196: }
197: }
198: for (int i = 0; i < uipInSubterms.length; i++) {
199: uipVector = uipInSubterms[i];
200: for (int j = 0; j < uipVector.size(); j++) {
201: if (contPredNames.add(((Formula) uipVector.get(j))
202: .getOp())) {
203: addUips.add(uipVector.get(j));
204: }
205: }
206: }
207: addUips.trimToSize();
208: uninterPreds = addUips;
209: }
210:
211: // Compute Vector of uninterpreted functions contained in this Formula
212: if (estSizeUif == 0) {
213: // If no uninterpreted functions contained, use empty template Vector
214: uninterFuncs = emptyVector;
215: } else {
216: // Compute Vector lengths and Vector elements, i.e. uninterpreted functions
217: HashSet contFuncNames = new HashSet(estSizeUif);
218: // Create new Vector of estimated capacity
219: Vector addUifs = new Vector(estSizeUif);
220: // Compute contained ui functions
221: Vector uifVector;
222: for (int i = 0; i < uifInSubforms.length; i++) {
223: uifVector = uifInSubforms[i];
224: for (int j = 0; j < uifVector.size(); j++) {
225: if (contFuncNames.add(((Term) uifVector.get(j))
226: .getFunction())) {
227: addUifs.add(uifVector.get(j));
228: }
229: }
230: }
231: for (int i = 0; i < uifInSubterms.length; i++) {
232: uifVector = uifInSubterms[i];
233: for (int j = 0; j < uifVector.size(); j++) {
234: if (contFuncNames.add(((Term) uifVector.get(j))
235: .getFunction())) {
236: addUifs.add(uifVector.get(j));
237: }
238: }
239: }
240: addUifs.trimToSize();
241: uninterFuncs = addUifs;
242: }
243:
244: // Calculate hash code for this Formula
245: int result = 17;
246: result = 37 * result + op.hashCode();
247: for (int i = 0; i < subformulae.length; i++) {
248: result = 37 * result + subformulae[i].hashCode();
249: }
250: for (int i = 0; i < subterms.length; i++) {
251: result = 37 * result + subterms[i].hashCode();
252: }
253: hashCode = result;
254: }
255:
256: /** Sole constructor; added for convenience.
257: * <p>
258: * Represents only a shorter form of the general constructor, with <tt>addThisUip</tt>
259: * set to <tt>false</tt> by default.
260: *
261: * @param operator the top-level operator of this <tt>Formula</tt>
262: * @param forms the array of subformulae for this <tt>Formula</tt>
263: * @param terms the array of subterms for this <tt>Formula</tt>
264: *
265: * @see de.uka.ilkd.key.proof.decproc.smtlib.Formula#Formula(String, Formula[], Term[], boolean)
266: */
267: protected Formula(String operator, Formula[] forms, Term[] terms) {
268: this (operator, forms, terms, false);
269: }
270:
271: /* Now the public methods and, supplemental, the protected setters */
272:
273: /** Returns the top-level operator of this <tt>Formula</tt>
274: *
275: * @return the top-level operator of this <tt>Formula</tt>
276: */
277: public final String getOp() {
278: return op;
279: }
280:
281: /** Returns a shallow copy of the subformulae array of this <tt>Formula</tt>
282: *
283: * @return the array of subformulae of this <tt>Formula</tt>
284: */
285: public final Formula[] getSubformulae() {
286: return (Formula[]) subformulae.clone();
287: }
288:
289: /** Returns a shallow copy of the subterms array of this <tt>Formula</tt>
290: *
291: * @return the array of subterms of this <tt>Formula</tt>
292: */
293: public final Term[] getSubterms() {
294: return (Term[]) subterms.clone();
295:
296: }
297:
298: /** Returns a <tt>Vector</tt> of all uninterpreted predicates contained in this <tt>Formula</tt>
299: *
300: * @return a <tt>Vector</tt> of all uninterpreted predicates contained in this <tt>Formula</tt>
301: */
302: public final Vector getUIPredicates() {
303: return (Vector) uninterPreds.clone();
304: }
305:
306: /** Returns a <tt>Vector</tt> of all uninterpreted functions contained in this <tt>Formula</tt>
307: * as a shallow copy
308: *
309: * @return a <tt>Vector</tt> of all uninterpreted functions contained in this <tt>Formula</tt>
310: */
311: public final Vector getUIF() {
312: return (Vector) uninterFuncs.clone();
313: }
314:
315: /** Returns true if this <tt>Formula</tt> contains <tt>f</tt> as a subformula.
316: * <p>
317: * This implementation tries to determine containment by first checking if <tt>f</tt>
318: * <tt>equals</tt> this <tt>Formula</tt>. If not, it calls <tt>containsFormula</tt> recursively
319: * first on the subformulae of this <tt>Formula</tt>, then on its subterms, returning
320: * <tt>true</tt> if one of these subelements contains <tt>f</tt>
321: * <p>
322: * If this method is called on an <tt>FletFormula</tt> with the <tt>FormulaVariable</tt>
323: * which will be semantically replaced in the <tt>FletFormula</tt> as argument, it will
324: * only check the replaced <tt>Formula</tt> for occurences of <tt>f</tt>
325: *
326: * @param f the <tt>Formula</tt> to be checked for containment in this <tt>Formula</tt>
327: * @return true if this <tt>Formula</tt> contains f
328: *
329: * @see FletFormula#containsFormula(Formula)
330: */
331: public boolean containsFormula(Formula f) {
332: if (equals(f))
333: return true;
334: for (int i = 0; i < subformulae.length; i++) {
335: if (subformulae[i].containsFormula(f))
336: return true;
337: }
338: for (int i = 0; i < subterms.length; i++) {
339: if (subterms[i].containsFormulaIteTerm(f))
340: return true;
341: }
342: return false;
343: }
344:
345: /** Returns true if this <tt>Formula</tt> contains the <tt>Term</tt> <tt>t</tt>.
346: * <p>
347: * This implementation tries to determine containment recursively by calling
348: * <tt>containsTerm</tt> first on the subformulae of this <tt>Formula</tt>, then on its
349: * subterms, returning <tt>true</tt> if one of these subelements contains <tt>t</tt>.
350: * <p>
351: * If <tt>t</tt> is a <tt>TermVariable</tt>, this method will only check for free
352: * term variables, i.e. if this method is called on a <tt>QuantifierFormula</tt> or a
353: * <tt>LetFormula</tt> with the quantified or rather bound <tt>TermVariable</tt> as argument,
354: * it will return <tt>false</tt>
355: *
356: * @param t the <tt>Term</tt> to be checked for containment in this <tt>Formula</tt>
357: * @return true if this <tt>Formula</tt> contains t
358: *
359: * @see QuantifierFormula#containsTerm(Term)
360: * @see LetFormula#containsTerm(Term)
361: */
362: public boolean containsTerm(Term t) {
363: for (int i = 0; i < subformulae.length; i++) {
364: if (subformulae[i].containsTerm(t))
365: return true;
366: }
367: for (int i = 0; i < subterms.length; i++) {
368: if (subterms[i].containsTerm(t))
369: return true;
370: }
371: return false;
372: }
373:
374: /** Compares this <tt>Formula</tt> to the specified <tt>Object</tt> <tt>o</tt>.
375: * <p>
376: * This implementation tries to determine equality by first checking if <tt>o</tt> is an instance
377: * of <tt>Formula</tt>. If so, it checks if the top-level operator of <tt>o</tt> is equal to that
378: * of this <tt>Formula</tt>. If true, it checks if all subformulae and subterms contained in this
379: * <tt>Formula</tt> are equal to those contained in <tt>o</tt>, and in the same order. If all these
380: * constraints are satisfied, true is returned.
381: * <p>
382: * Overriding methods are recommended to check for object equality in addition; this is not done in
383: * this implementation.
384: *
385: * @param o the <tt>Object</tt> to compare with
386: * @return true if this <tt>Formula</tt> is the same as the specified <tt>Object</tt>;
387: * otherwise false.
388: */
389: public boolean equals(Object o) {
390: if (o instanceof Formula) {
391: Formula f = (Formula) o;
392: if (op.equals(f.getOp())) {
393: if (subformulae.length == f.getSubformulae().length) {
394: if (subterms.length == f.getSubterms().length) {
395: Formula[] fSubformulae = f.getSubformulae();
396: Term[] fSubterms = f.getSubterms();
397: for (int i = 0; i < subformulae.length; i++) {
398: if (!subformulae[i].equals(fSubformulae[i]))
399: return false;
400: }
401: for (int i = 0; i < subterms.length; i++) {
402: if (!subterms[i].equals(fSubterms[i]))
403: return false;
404: }
405: return true;
406: }
407: }
408: }
409: }
410: return false;
411: }
412:
413: /** Returns an int value representing the hash code of this <tt>Formula</tt>.
414: * <p>
415: * The hash code for a <tt>Formula</tt> is calculated during its creation. This is done by
416: * combining the hash code of its operator with the hash codes of, if available, its subformulae
417: * and its subterms to a new hash code. The order of subformulae and subterms matters for this
418: * implementation
419: *
420: * @return the hashCode of this <tt>Term</tt>
421: */
422: public int hashCode() {
423: return hashCode;
424: }
425:
426: /** Returns a String representation of this <tt>Formula</tt>, containing the String
427: * representation of each of its subformulae and/or subterms. The returned <tt>String</tt>
428: * is formatted and can be parsed according to the SMT-Lib grammar specification (chapter seven,
429: * "Concrete Syntax").
430: *
431: * @see <a href="http://combination.cs.uiowa.edu/smtlib/papers/format-v1.1-r05.04.12.pdf">
432: * The SMT-LIB Standard: Version 1.1</a>
433: *
434: * @return a String representation of this <tt>Formula</tt>
435: */
436: public abstract String toString();
437:
438: /** Replaces all occurrences of a specified <tt>FormulaVariable</tt> by a specified
439: * <tt>Formula</tt> in a this <tt>Formula</tt>.
440: * <p>
441: * Thereby this <tt>Formula</tt> and the returned replaced <tt>Formula</tt> share the
442: * same objects in their fields, except for those objects which contained the
443: * specified <tt>FormulaVariable</tt>.<br>
444: * This implicates that if <tt>formVar</tt> is not contained in this <tt>Formula</tt>,
445: * this <tt>Formula</tt> is returned without changes.
446: *
447: * @param formVar the <tt>FormulaVariable</tt> to be replaced
448: * @param replacement the <tt>Formula</tt> used to replace formVar
449: * @return the <tt>Formula</tt> obtained by replacing every (free) occurence of formVar
450: * by replacement in this <tt>Formula</tt>
451: */
452: public abstract Formula replaceFormVar(FormulaVariable formVar,
453: Formula replacement);
454:
455: /** Replaces all occurrences of a specified <tt>TermVariable</tt> by a specified <tt>Term</tt>
456: * in a this <tt>Formula</tt>.
457: * <p>
458: * Thereby this <tt>Formula</tt> and the returned replaced <tt>Formula</tt> share the
459: * same objects in their fields, except for those objects which contained the
460: * specified <tt>TermVariable</tt>.<br>
461: * This implicates that if <tt>termVar</tt> is not contained in this <tt>Formula</tt>,
462: * this <tt>Formula</tt> is returned without changes.
463: *
464: * @param termVar the <tt>TermVariable</tt> to be replaced
465: * @param replacement the <tt>Term</tt> used to replace termVar
466: * @return the <tt>Formula</tt> obtained by replacing every (free) occurence of termVar
467: * by replacement in this <tt>Formula</tt>
468: */
469: public abstract Formula replaceTermVar(TermVariable termVar,
470: Term replacement);
471:
472: // Further internal (protected) methods
473:
474: /** Converts an array into a <tt>Vector</tt>, preserving element order
475: *
476: * @param objects The array which should be converted into a <tt>Vector</tt>
477: * @return a <tt>Vector</tt> containing all the <tt>Object</tt>s in the specified array,
478: * in the same order
479: */
480: protected static final Vector toVector(Object[] objects) {
481: Vector vector = new Vector(objects.length);
482: for (int i = 0; i < objects.length; i++) {
483: vector.add(i, objects[i]);
484: }
485: return vector;
486: }
487:
488: /** Determines if a given identifier represents a legal identifier symbol in (QF_)AUFLIA.
489: * <p>
490: * An identifier is legal if it begins with a letter and consists only of letters, digits and
491: * the characters '.' , '_' and ''' (single quotation mark)
492: *
493: * @param identifier the String to be checked
494: * @return true if the specified String represents a legal identifier symbol; otherwise false
495: *
496: * @throws NullPointerException if <tt>identifier</tt> is null
497: */
498: protected static final boolean isLegalIdentifier(String identifier) {
499: char first = identifier.charAt(0);
500: // First character must be a letter
501: if ((first >= 'A' && first <= 'Z')
502: || (first >= 'a' && first <= 'z')) {
503: char act;
504: // All other characters must be letters or digits or '.', '_' or "'"
505: for (int i = 1; i < identifier.length(); i++) {
506: act = identifier.charAt(i);
507: if (!((act >= 'A' && act <= 'Z')
508: || (act >= 'a' && act <= 'z')
509: || (act >= '0' && act <= '9') || (act == '.'
510: || act == '_' || act == '\'')))
511: return false;
512: }
513: return true;
514: }
515: return false;
516: }
517:
518: }
|