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 de.uka.ilkd.key.logic.Term;
014:
015: /** This class implements a visitor used to determine the translatability of KeY <tt>Term</tt>s
016: * into SMT-LIB <tt>Formula</tt>e.
017: * <p>
018: * This implementation is intended for KeY <tt>Term</tt>s of <tt>Sort</tt> <tt>Formula</tt>. To
019: * determine if a given <tt>Term</tt> can be translated into SMT-LIB syntax, its
020: * <tt>execPretOrder</tt> method should be called with an instance of this class as argument.
021: * The determined result can be fetched subsequently by the <tt>getTranslationResult</tt> method,
022: * which in case of this class delivers a Boolean indicating the translatability
023: * <p>
024: * This class also provides a factory method that can be used to get an instance of this class.
025: * It implements the singleton pattern and allows reusing the same visitor object for multiple
026: * successive translations, in conjunction with the reset method
027: *
028: * @author akuwertz
029: * @version 1.4, 12/10/2006 (Introduced new superclass 'TranslationVisitor')
030: */
031:
032: public class PreTranslationVisitor extends TranslationVisitor {
033:
034: /* Additional fields */
035:
036: /** A <tt>PreTranslationVisitor</tt> instance serving as a singleton. It allows object reuse
037: * and therefore saving memory */
038: private static PreTranslationVisitor singleton = null;
039:
040: /** A <tt>boolean</tt> indicating if the singleton instance should translate quantifiers */
041: private static boolean translateQuantifiers;
042:
043: /** A <tt>boolean</tt> flag indicating if the currently visited <tt>Term</tt> is considered
044: * translatable into SMT-Lib syntax */
045: private boolean isTranslatable;
046:
047: /** A <tt>boolean</tt> indicating if this <tt>PreTranslationVisitor</tt> instance translates
048: * quantifiers */
049: private final boolean isTranslatingQuantifiers;
050:
051: /* Constructors */
052:
053: /** Sole constructor.
054: * <p>
055: * Creates a new <tt>PreTranslationVisitor</tt> and initialises it with the rules for all
056: * operators that can not be translated
057: *
058: * @param useQuantifier boolean that determines whether quantifiers will be translated or not
059: */
060: public PreTranslationVisitor(boolean useQuantifier) {
061:
062: // Create a prefix identifying this class for logging
063: loggingSubclass = "Pre";
064:
065: // This list of rules must contain only these rules to handle untranslatable Term operators
066: ListOfIOperatorTranslation trRules = SLListOfIOperatorTranslation.EMPTY_LIST;
067: if (!useQuantifier) {
068: trRules = trRules.append(new TranslateQuantifier()).append(
069: new TranslateLogicVariable());
070: }
071: trRules = trRules.append(new TranslateIUpdateOperator())
072: .append(new TranslateModality()).append(
073: new TranslateProgramMethod()).append(
074: new TranslateMetavariable());
075:
076: setTranslationRules(trRules);
077: isTranslatable = true;
078: isTranslatingQuantifiers = useQuantifier;
079: }
080:
081: /** A factory method returning a <tt>PreTranslationVisitor</tt> instance.
082: * <p>
083: * This method uses the Singleton pattern. It is intended to enable the reuse of an already created
084: * visitor object after a complete translation. Use this method to get an instance of
085: * <tt>PreTranslationVisitor</tt> if there is no need for concurrency.
086: * <p>
087: * To specify whether the returned instance should translate quantifiers or not, the
088: * <tt>setTranslateQuantifiers</tt> method must be called prior to calling this method
089: *
090: * @return a <tt>PreTranslationVisitor</tt> instance.
091: *
092: * @throws IllegalStateException if the cached <tt>PreTranslationVisitor</tt> instance is not
093: * considered reusable at this point of time
094: *
095: * @see TranslationVisitor#getInstance()
096: * @see #setTranslateQuantifers(boolean)
097: */
098: public synchronized static TranslationVisitor getInstance() {
099: if (singleton == null
100: || singleton.isTranslatingQuantifiers != translateQuantifiers) {
101: logger
102: .debug("Creating and storing new PreTranslationVisitor"
103: + " as singleton...");
104: singleton = new PreTranslationVisitor(translateQuantifiers);
105: }
106: if (!singleton.isReusable())
107: throw new IllegalStateException(NoReuseStateException);
108: return singleton;
109: }
110:
111: /* Now the protected and public methods */
112:
113: /** The visit method of this <tt>PreTranslationVisitor</tt>. Takes a <tt>Term</tt> and tries
114: * to determine its translatability by its <tt>Operator</tt>
115: *
116: * @see de.uka.ilkd.key.logic.Visitor#visit(de.uka.ilkd.key.logic.Term)
117: */
118: public void visit(Term t) {
119: if (isTranslatable) {
120: logger
121: .info(logThis("Starting to check term for translatability..."));
122: for (int i = 0; i < translationRules.length; i++) {
123: if (translationRules[i].isApplicable(t.op())) {
124: logger.info(logThis("Found appliable rule: "
125: + translationRules[i].getClass().getName()
126: .replaceAll(
127: translationRules[i]
128: .getClass()
129: .getPackage()
130: .getName()
131: + ".", "")
132: + " - term is not translatable!"));
133: isTranslatable = false;
134: // Leave loop after successful translation
135: i = translationRules.length;
136: }
137: }
138: logger.info(logThis("Finished checking term!"));
139: logger.debug(logThis("Checked term: " + t.toString()));
140: }
141: }
142:
143: /** Determines whether a <tt>PreTranslationVisitor</tt> instance retrieved by the
144: * <tt>getInstance</tt> method translated quantifiers or not
145: *
146: * @param useQuantifiers specifies if quantifiers should be translated or not
147: *
148: * @see #getInstance()
149: */
150: public static void setTranslateQuantifers(boolean useQuantifiers) {
151: translateQuantifiers = useQuantifiers;
152: }
153:
154: /** Checks whether a given <tt>Term</tt> contains any free quantifiable variables
155: *
156: * @param t the <tt>Term</tt> to be checked for free variable occurrences
157: * @return true if no free variables occur in <tt>t</tt>
158: */
159: public boolean noFreeVariableOccurrences(Term t) {
160: if (t.freeVars().size() != 0) {
161: logger.info(logThis("Found free variables in term: " + t));
162: return false;
163: }
164: logger
165: .info(logThis("Checked for free variables - no occurences"));
166: return true;
167: }
168:
169: /** Returns true if the <tt>Term</tt> visited during the last pretranslation process
170: * can be translated into SMT-Lib syntax.
171: * <p>
172: * A <tt>Term</tt> is considered translatable if it does not represent a <tt>Quantifier</tt>,
173: * a <tt>Metavariable</tt>, a <tt>Modality</tt> or an <tt>IUpdateOperator</tt> and does not
174: * contain any subterm representing one of the above mentioned <tt>Operator</tt>s.
175: * <p>
176: * This method should not be called directly but only accessed via the
177: * <tt>getTranslationResult</tt> method
178: *
179: * @return a <tt>Boolean </tt> indicating if the currently visited <tt>Term</tt> is considered
180: * translatable into SMT-Lib syntax; otherwise false
181: */
182: protected Object getResult() {
183: Boolean result = new Boolean(isTranslatable);
184: isTranslatable = true; // Reset to resuable state
185: return result;
186: }
187:
188: /** Returns true if this <tt>PreTranslationVisitor</tt> is ready for the next translation process
189: * <p>
190: * This holds if that translation process has finished and the <tt>getTranslationResult</tt>
191: * method was called, or if the <tt>reset</tt> method has been called in an arbitrary state
192: *
193: * @return true if this <tt>TranslationVisitor</tt> is ready to be reused; otherwise false
194: */
195: protected boolean isReusable() {
196: return super .isReusable() && isTranslatable;
197: }
198:
199: /* (non-Javadoc)
200: * @see de.uka.ilkd.key.proof.decproc.translation.TranslationVisitor#reset()
201: */
202: public void reset() {
203: super .reset();
204: isTranslatable = true;
205: logger.debug(logThis("Reseted PreTranslationVisitor!"));
206: }
207:
208: }
|