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.proof.decproc.translation;
012:
013: import java.util.Vector;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.LogicVariable;
017: import de.uka.ilkd.key.logic.sort.Sort;
018: import de.uka.ilkd.key.proof.decproc.smtlib.Formula;
019: import de.uka.ilkd.key.proof.decproc.smtlib.TermVariable;
020:
021: /** This class implements a visitor used to translate <tt>Term</tt>s in KeY into <tt>Formula</tt>e
022: * in SMT-LIB.
023: * <p>
024: * This implementation is intended for KeY <tt>Term</tt>s of <tt>Sort</tt> <tt>Formula</tt>. To
025: * translate a given <tt>Term</tt>, its <tt>execPostOrder</tt> method should be called with an
026: * instance of this class as argument. The translation result can then be fetched using the
027: * <tt>getTranslationResult</tt> method of this class.
028: * <p>
029: * Prior to translating a <tt>Term</tt> with this class, its translatability should be checked by
030: * using the <tt>PreTranslationVisitor</tt> subclass.
031: * <p>
032: * This class also provides a factory method that can be used to get an instance of this class.
033: * It implements the singleton pattern and allows reusing the same visitor object for multiple
034: * successive translations
035: *
036: * @author akuwertz
037: * @version 1.5, 12/10/2006 (Introduced new superclass 'TranslationVisitor')
038: */
039:
040: public class TermTranslationVisitor extends TranslationVisitor {
041:
042: /* Additional fields */
043:
044: /** A <tt>TermTranslationVisitor</tt> instance serving as a singleton. It allows object reuse
045: * and therefore saving memory */
046: private static TermTranslationVisitor singleton = null;
047:
048: /** The <tt>Services</tt> currently used by the singleton instance */
049: private static Services currentServices;
050:
051: /** A <tt>boolean</tt> indicating if the singleton instance should translate quantifiers */
052: private static boolean translateQuantifiers;
053:
054: /** A Vector serving as a stack for already translated subterms */
055: private Vector argumentStack = new Vector();
056:
057: /** The currently used instance of <tt>CreateTypePred</tt> */
058: private CreateTypePred typePredCreator;
059:
060: /** The <tt>Term</tt> been currently translated by the <tt>visit</tt> method */
061: private Term currentTerm = null;
062:
063: /** The <tt>Services</tt> used by this <tt>TermTranslationVisitor</tt> instance */
064: private final Services usedServices;
065:
066: /** A <tt>boolean</tt> indicating if this <tt>TermTranslationVisitor</tt> instance translates
067: * quantifiers */
068: private final boolean isTranslatingQuantifiers;
069:
070: /* String constants for failures during translation process */
071: private static final String stackCountException = "Argument stack contains less elements than: ";
072: private static final String internalStateCorruptedError = "Translation has been corrupted due to internal errors!";
073:
074: /* Constructors */
075:
076: /** Sole constructor.
077: * <p>
078: * Creates a new <tt>TermTranslationVisitor</tt> and initialises it with all known translation
079: * rules.<br>
080: * If <tt>useQuantifier</tt> is set to <tt>true</tt>, KeY <tt>Term</tt>s containing
081: * quantifier operators will be translated; otherwise, they are declared untranslatable
082: *
083: * @param services the common <tt>Services</tt> of the KeY prover
084: * @param useQuantifier boolean that determines if quantifiers will be translated or not
085: */
086: public TermTranslationVisitor(Services services,
087: boolean useQuantifier) {
088:
089: usedServices = services;
090: isTranslatingQuantifiers = useQuantifier;
091:
092: // Create a prefix identifying this class for logging
093: loggingSubclass = "ttVis";
094:
095: // This command adds all available translation rules to this visitor. They will be used in
096: // its visit method by applying the first suitable rule to translate the given operator, so
097: // consider rule order carefully!
098: logger.info(logThis("Creating new TermTranslationVisitor..."));
099: ListOfIOperatorTranslation trRules = SLListOfIOperatorTranslation.EMPTY_LIST
100: .append(new TranslateJunctor()).append(
101: new TranslateIfThenElse()).append(
102: new TranslateEquality());
103: if (useQuantifier) {
104: trRules = trRules.append(new TranslateQuantifier()).append(
105: new TranslateLogicVariable());
106: }
107: trRules = trRules.append(new TranslateFunction()).append(
108: new TranslateAttributeOp()).append(
109: new TranslateArrayOp()).append(
110: new TranslateProgramVariable()).append(
111: new TranslateUnknownOp());
112:
113: logger.debug(logThis("Setting translation rules"));
114: this .setTranslationRules(trRules);
115:
116: // Initialize the type predicate creation class
117: typePredCreator = new CreateTypePred(usedServices);
118:
119: }
120:
121: /** A factory method returning a <tt>TermTranslationVisitor</tt> instance.
122: * <p>
123: * This method uses the Singleton pattern. It is intended to enable the reuse of an already created
124: * visitor object after a complete translation. Use this method to get an instance of
125: * <tt>TermTranslationVisitor</tt> if there is no need for concurrency
126: * <p>
127: * A translation process is considered complete after its result has been fetched by the
128: * <tt>getTranslationResult</tt> method of this class
129: * <p>
130: * To specify whether the returned instance should translate quantifiers or not, the
131: * <tt>setTranslateQuantifiers</tt> method must be called prior to calling this method.<br>
132: * To specify the <tt>Services</tt> the returned instance should use, the <tt>setServices</tt>
133: * method must be called prior to calling this method
134: *
135: * @return a <tt>TermTranslationVisitor</tt> instance
136: *
137: * @throws NullPointerException if no <tt>Services</tt> have been set with <tt>setServices</tt>
138: * @throws IllegalStateException if the cached <tt>TermTranslationVisitor</tt> instance is not
139: * considered reusable at this point of time
140: *
141: * @see TranslationVisitor#getInstance()
142: * @see #setTranslateQuantifers(boolean)
143: * @see #setServices(Services)
144: */
145: public synchronized static TranslationVisitor getInstance() {
146: if (singleton == null
147: || singleton.isTranslatingQuantifiers != translateQuantifiers
148: || !singleton.usedServices.equals(currentServices)) {
149: logger
150: .debug("Storing created TermTranslationVisitor instance as singleton...");
151: singleton = new TermTranslationVisitor(currentServices,
152: translateQuantifiers);
153: }
154: if (!singleton.isReusable())
155: throw new IllegalStateException(NoReuseStateException);
156: return singleton;
157: }
158:
159: /* Now the public methods */
160:
161: /** The visit method of this <tt>TermTranslationVisitor</tt>. Takes a <tt>Term</tt> and tries
162: * to translate its <tt>Operator</tt> into SMT-LIB syntax.
163: * <p>
164: * The translation result is stored in an internal stack for further processing
165: *
166: * @see de.uka.ilkd.key.logic.Visitor#visit(de.uka.ilkd.key.logic.Term)
167: * @see #getTranslationResult()
168: */
169: public void visit(Term t) {
170: logger.info(logThis("Starting term translation..."));
171: currentTerm = t;
172: for (int i = 0; i < translationRules.length; i++) {
173: if (translationRules[i].isApplicable(t.op())) {
174: logger.info(logThis("Appling rule: "
175: + translationRules[i].getClass().getName()
176: .replaceAll(
177: translationRules[i].getClass()
178: .getPackage().getName()
179: + ".", "")));
180: argumentStack.add(translationRules[i].translate(t.op(),
181: this ));
182: logger.info(logThis("Finished term translation!"));
183: logger
184: .debug(logThis("Term: "
185: + currentTerm.toString()));
186: logger.debug(logThis("was translated into: "
187: + argumentStack.lastElement()));
188: // Leave loop after successful translation
189: i = translationRules.length;
190: }
191: }
192: }
193:
194: /** Determines whether a <tt>TermTranslationVisitor</tt> instance retrieved by the
195: * <tt>getInstance</tt> method translated quantifiers or not
196: *
197: * @param useQuantifiers specifies if quantifiers should be translated or not
198: *
199: * @see #getInstance()
200: */
201: public static void setTranslateQuantifers(boolean useQuantifiers) {
202: translateQuantifiers = useQuantifiers;
203: }
204:
205: /** Sets the <tt>Services</tt> that should be used by a <tt>TermTranslationVisitor</tt>
206: * instance retrieved by the <tt>getInstance</tt> method
207: *
208: * @param services <tt>Services</tt> to be used
209: *
210: * @see #getInstance()
211: */
212: public static void setServices(Services services) {
213: currentServices = services;
214: }
215:
216: /** Empties the type predicate storages.<br>
217: * All type predicates that have been created during <tt>Term</tt> translation processes since
218: * either the creation of this instance or the last call to this method will be deleted
219: */
220: public void clearTypePreds() {
221: typePredCreator = new CreateTypePred(usedServices);
222: }
223:
224: /** Returns the translation of a (logic) <tt>Term</tt> of <tt>Sort</tt> <tt>Formula</tt>,
225: * which was built by successive calls of the <tt>visit</tt> method through the
226: * <tt>execPostOrder</tt> method on this <tt>Term</tt>.<br>
227: * Also resets this <tt>TermTranslationVisitor</tt> for further reuse, so that this method
228: * can only be called once per <tt>Term</tt> translation
229: *
230: * @return the translation of the <tt>Term</tt> on which the <tt>execPostOrder</tt> method
231: * was called with this <tt>TermTranslationvisitor</tt> as argument
232: */
233: protected Object getResult() {
234: if (argumentStack.size() != 1)
235: throw new Error(internalStateCorruptedError);
236: // Reset this instance for reuse: empty argument stack...
237: return (Formula) argumentStack.remove(0);
238: }
239:
240: /** Returns a <tt>Vector</tt> containing all type predicates created during all <tt>Term</tt>
241: * translation process since either to creation of this instance or the last call to the
242: * <tt>clearTypePreds</tt> method
243: *
244: * @return the <tt>Vector </tt> of created type predicates
245: *
246: * @throws IllegalStateException if this method is called during an unfinished translation
247: * process or before any translation was initiated
248: * @see #clearTypePreds()
249: */
250: public Vector getCreatedTypePreds() {
251: if (!super .isReusable()) {
252: throw new IllegalStateException(
253: translationNotFinishedException);
254: }
255: return typePredCreator.getCreatedTypePreds();
256: }
257:
258: /** Returns a <tt>Vector</tt> containing all hierarchy predicates needed for the current
259: * translation.<br>
260: * The current translation thereby means all <tt>Term</tt> translation processes since either
261: * the creation of this instance or the last call to the <tt>clearTypePreds</tt> method
262: *
263: *
264: * @return the <tt>Vector </tt> of created hierarchy predicates
265: *
266: * @throws IllegalStateException if this method is called during an unfinished translation
267: * process or before any translation was initiated
268: * @see #clearTypePreds()
269: */
270: public Vector getHierarchyPreds() {
271: if (!super .isReusable()) {
272: throw new IllegalStateException(
273: translationNotFinishedException);
274: }
275: return typePredCreator.createObjHierarchyPreds();
276: }
277:
278: /* Now some protected helper functions, mainly intended for package internal usage */
279:
280: /** Returns an <tt>Object</tt> array containing the translation of the last <tt>count</tt>
281: * translated <tt>Term</tt>s.<br>
282: * Thereby the latest translation has the highest index. All returned translations are removed
283: * from their internal storage
284: *
285: * @param count the number of translations that should be returned
286: * @return an <tt>Object</tt> array containing the last <tt>count</tt> stored translations
287: *
288: * @throws IndexOutOfBoundsException if count is higher than the count of currently stored
289: *
290: * @see #visit(Term)
291: */
292: protected Object[] getTranslatedArguments(int count) {
293: if (count > argumentStack.size()) {
294: throw new IndexOutOfBoundsException(stackCountException
295: + count);
296: }
297: // Get the last count translated Terms/Formulae
298: Object[] translatedArgs = new Object[count];
299: for (int i = count - 1; i >= 0; i--) {
300: translatedArgs[i] = argumentStack.remove(argumentStack
301: .size() - 1);
302: }
303: return translatedArgs;
304: }
305:
306: /** Translates a given <tt>LogicVariable</tt> into its SMT-LIB representation.
307: * <p>
308: * This method uses the same class to translate the given <tt>LogicVariable</tt> as the
309: * <tt>visit</tt> method but can be applied to a single <tt>LogicVariable</tt> instead of
310: * a whole <tt>Term</tt>.
311: *
312: * @param lv the <tt>LogicVariable</tt> to be translated manually
313: * @return the SMT-LIB representation of the translated <tt>LogicVariable</tt>
314: */
315: protected TermVariable translateLvManually(LogicVariable lv) {
316: TermVariable translation = null;
317: logger
318: .info(logThis("Starting manual logic variable translation: "
319: + lv.name()));
320: for (int i = 0; i < translationRules.length; i++) {
321: if (translationRules[i] instanceof TranslateLogicVariable) {
322: logger.info(logThis("Appling rule: "
323: + translationRules[i].getClass().getName()
324: .replaceAll(
325: translationRules[i].getClass()
326: .getPackage().getName()
327: + ".", "")));
328: // Important: the translate method of class LogicVariable does not change
329: // the stack of this TermTranslationVisitor!
330: translation = (TermVariable) translationRules[i]
331: .translate(lv, this );
332: logger
333: .info(logThis("Finished manual logic variable translation!"));
334: // Leave loop after successful translation
335: i = translationRules.length;
336: }
337: }
338: return translation;
339: }
340:
341: /* (non-Javadoc)
342: * @see de.uka.ilkd.key.proof.decproc.translation.CreateTypePred#getTypePredLv(de.uka.ilkd.key.logic.sort.Sort, de.uka.ilkd.key.proof.decproc.smtlib.TermVariable)
343: */
344: protected Formula createTypePredLv(Sort type, TermVariable termVar) {
345: return typePredCreator.getTypePredLv(type, termVar);
346: }
347:
348: /* (non-Javadoc)
349: * @see de.uka.ilkd.key.proof.decproc.translation.CreateTypePred#createTypePredUif(de.uka.ilkd.key.logic.sort.Sort, java.lang.String, int)
350: */
351: protected void createTypePredUif(Sort type, String funcName,
352: int argCount) {
353: typePredCreator.createTypePredUif(type, funcName, argCount);
354: }
355:
356: /** Returns the currently translated <tt>Term</tt>
357: *
358: * @return the currently translated <tt>Term</tt>
359: */
360: protected Term getCurrentTerm() {
361: return currentTerm;
362: }
363:
364: /** Returns the KeY <tt>Services</tt> used for translation
365: *
366: * @return the KeY <tt>Services</tt> used for translation
367: */
368: protected Services getServices() {
369: return usedServices;
370: }
371:
372: /** Returns true if this <tt>TermTranslationVisitor</tt> is ready for the next translation
373: * process.
374: * <p>
375: * This holds under the following conditions:
376: * - This instance was in reusable state and no translation has yet been initiated
377: * - The <tt>reset</tt> was called in an arbitrary state
378: * - The current translation has finish and the <tt>getTranslationResult</tt> method was
379: * called on this instance
380: *
381: * @return true if this <tt>TranslationVisitor</tt> is ready to be reused; otherwise false
382: */
383: protected boolean isReusable() {
384: return super .isReusable() && argumentStack.isEmpty();
385: }
386:
387: /** Resets this <tt>TermTranslationVisitor</tt> for reuse.<br>
388: * After execution of this method the state of this <tt>TermTranslationVisistor</tt> is
389: * equals to that of a newly created <tt>TermTranslationVisitor</tt>
390: */
391: public void reset() {
392: super.reset();
393: if (!argumentStack.isEmpty())
394: argumentStack.clear();
395: }
396:
397: }
|