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;
019:
020: import java.util.Vector;
021: import org.apache.log4j.Logger;
022: import de.uka.ilkd.key.java.Services;
023: import de.uka.ilkd.key.logic.Semisequent;
024: import de.uka.ilkd.key.logic.Sequent;
025: import de.uka.ilkd.key.logic.Term;
026: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp;
027: import de.uka.ilkd.key.proof.decproc.smtlib.Benchmark;
028: import de.uka.ilkd.key.proof.decproc.smtlib.ConnectiveFormula;
029: import de.uka.ilkd.key.proof.decproc.smtlib.Formula;
030: import de.uka.ilkd.key.proof.decproc.smtlib.TruthValueFormula;
031: import de.uka.ilkd.key.proof.decproc.translation.PreTranslationVisitor;
032: import de.uka.ilkd.key.proof.decproc.translation.TermTranslationVisitor;
033:
034: /** This class is responsible for converting a <tt>Sequent</tt> into the language of the SMT logic
035: * (QF_)AUFLIA.
036: * <p>
037: * To translate a given <tt>Sequent</tt>, a new instance of this class must be created with that
038: * <tt>Sequent</tt> and common <tt>Services</tt> as arguments. The translation is done during the
039: * creation process, so the translation result can be fetched by calling the <tt>getBenchmark</tt>
040: * on the newly created <tt>SmtAufliaTranslation</tt> instance.
041: *
042: * @author akuwertz
043: * @version 1.5, 11/15/2006 (Added support for type predicates)
044: *
045: * @see de.uka.ilkd.key.proof.decproc.smtlib.Benchmark
046: */
047:
048: public class SmtAufliaTranslation {
049:
050: /* Additional fields */
051:
052: /** An identifier for the translated <tt>Sequent</tt> as timestamp */
053: private String proofName = AbstractDecisionProcedure
054: .getCurrentDateString().substring(0, 20).replaceAll("-",
055: "_To_");
056:
057: /** The Benchmark representing the result of the translation process */
058: private Benchmark benchmark;
059:
060: /** The <tt>TermTranslationVisitor</tt> used to translate <tt>Term</tt>s */
061: private final TermTranslationVisitor ttVisitor;
062:
063: /** A <tt>boolean</tt> to determine whether quantifier should be translated or not */
064: private final boolean translateQuantifiers;
065:
066: /** Integer constant to identify the antecedent of a sequent */
067: private static final int ANTECEDENT = 0;
068: /** Integer constant to identify the succedent of a sequent */
069: private static final int SUCCEDENT = 1;
070:
071: /** A <tt>Logger</tt> for logging and debugging of the translation process into SMT syntax */
072: private static final Logger logger = Logger
073: .getLogger(SmtAufliaTranslation.class.getName());
074: // Logger is created hierarchical to inherit configuration and behaviour from parent
075:
076: private static final char[] legaliseSymbol = new char[255];
077:
078: /* Constructor */
079:
080: /** A constructor which starts the translation a given <tt>Sequent</tt> to SMT AUFLIA syntax.
081: * The result can be fetched with the <tt>getBenchmark</tt> method
082: *
083: * @param sequent the <tt>Sequent</tt> which shall be translated
084: * @param services the common <tt>Services</tt> of the KeY prover
085: * @param useQuantifiers determines whether quantifiers should be translated or not
086: *
087: * @see #getBenchmark()
088: */
089: public SmtAufliaTranslation(Sequent sequent, Services services,
090: boolean useQuantifiers) {
091: logger.info("Creating new SmtAufliaTranslation instance... ");
092: translateQuantifiers = useQuantifiers;
093: ttVisitor = new TermTranslationVisitor(services, useQuantifiers);
094: PreTranslationVisitor
095: .setTranslateQuantifers(translateQuantifiers);
096: // Initialize all neccessary objects before starting translation!
097: benchmark = translate(sequent);
098: benchmark.setLogic(useQuantifiers);
099: logger.info("Translation completed!");
100: }
101:
102: /* Public and private methods */
103:
104: /** Returns the resulting translation of the <tt>Sequent</tt> this class was created with, as a
105: * <tt>Benchmark</tt>
106: *
107: * @return the <tt>Benchmark</tt> representing the result of the translation process
108: */
109: public Benchmark getBenchmark() {
110: return benchmark;
111: }
112:
113: /** Translates the given <tt>Sequent</tt> into SMT AUFLIA input syntax and returns
114: * a <tt>Benchmark</tt> representing the translation result.
115: *
116: * @param sequent the <tt>Sequent</tt> which should be translated into SMT AUFLIA syntax
117: * @return the Benchmark representing the translation result
118: */
119: private final Benchmark translate(Sequent sequent) {
120: // Create Benchmark
121: Benchmark smtTranslation = new Benchmark(proofName);
122:
123: // Translate semisequents
124: logger.info("Starting sequent translation with antecedent...");
125: Formula antecedentSequent = translate(sequent.antecedent(),
126: ANTECEDENT);
127: logger
128: .info("Finished translating antecedent, starting with succedent...");
129: Formula succedentSequent = translate(sequent.succedent(),
130: SUCCEDENT);
131: logger.info("Finished translating succedent!");
132:
133: Formula[] helper;
134: logger.info("Retrieving type predicates...");
135: // Assemble type predicates (if existing) by conjunctions
136: Vector typePreds = ttVisitor.getCreatedTypePreds();
137: Formula typePredFormula = null;
138: if (typePreds.size() > 0) {
139: logger.info("Found " + typePreds.size()
140: + " type predicates,"
141: + " integrating them into new formula...");
142: typePredFormula = (Formula) typePreds.get(0);
143: for (int i = 1; i < typePreds.size(); i++) {
144: helper = new Formula[] { typePredFormula,
145: (Formula) typePreds.get(i) };
146: typePredFormula = new ConnectiveFormula(
147: DecisionProcedureSmtAufliaOp.AND, helper);
148: }
149: }
150:
151: // Assemble type hierarchy predicates (if existing) by conjunctions
152: Vector hierarchyPreds = ttVisitor.getHierarchyPreds();
153: Formula typeHierarchyFormula = null;
154: if (hierarchyPreds.size() > 0) {
155: logger.info("Found " + hierarchyPreds.size()
156: + " type hierarchy predicates,"
157: + " integrating them into new formula...");
158: typeHierarchyFormula = (Formula) hierarchyPreds.get(0);
159: for (int i = 1; i < hierarchyPreds.size(); i++) {
160: helper = new Formula[] { typeHierarchyFormula,
161: (Formula) hierarchyPreds.get(i) };
162: typeHierarchyFormula = new ConnectiveFormula(
163: DecisionProcedureSmtAufliaOp.AND, helper);
164: }
165: }
166:
167: // Assemble final translation formula and negate it!
168: if (typeHierarchyFormula != null) {
169: helper = new Formula[] { typeHierarchyFormula,
170: antecedentSequent };
171: antecedentSequent = new ConnectiveFormula(
172: DecisionProcedureSmtAufliaOp.AND, helper);
173: logger
174: .info("Integrated type hierarchy predicate and translation result formula");
175: }
176:
177: if (typePredFormula != null) {
178: helper = new Formula[] { typePredFormula, antecedentSequent };
179: antecedentSequent = new ConnectiveFormula(
180: DecisionProcedureSmtAufliaOp.AND, helper);
181: logger
182: .info("Integrated type predicate and translation result formula");
183: }
184:
185: helper = new Formula[] { antecedentSequent, succedentSequent };
186: Formula finalTranslation = new ConnectiveFormula(
187: DecisionProcedureSmtAufliaOp.IMP, helper);
188: finalTranslation = new ConnectiveFormula(
189: DecisionProcedureSmtAufliaOp.NOT,
190: new Formula[] { finalTranslation });
191: logger.info("Constructed and negated resulting formula!");
192:
193: // Set formula in Benchmark and return
194: smtTranslation.setFormula(finalTranslation);
195: return smtTranslation;
196: }
197:
198: /** Translates the given <tt>Semisequent</tt> into SMT AUFLIA input syntax. The specified
199: * <tt>int</tt> thereby indicates if the given <tt>Semisequent</tt> represents an antecedent
200: * or a succedent
201: *
202: * @param ss the <tt>Semisequent</tt> which should be translated into SMT AUFLIA syntax
203: * @param skolemization a switch for translating the given <tt>Semisequent</tt> as an antecedent
204: * (zero) or as a succedent (one) [The constant fields of this class should be used!]
205: * @return a <tt>Formula</tt> (SMT-LIB) representing the translation result
206: */
207: private final Formula translate(Semisequent ss, int skolemization) {
208: String connective;
209: if (skolemization == ANTECEDENT) {
210: connective = DecisionProcedureSmtAufliaOp.AND;
211: } else {
212: connective = DecisionProcedureSmtAufliaOp.OR;
213: }
214:
215: // Translate all ConstrainedFormulae contained in this Semisequent
216: Vector translations = new Vector(ss.size());
217: for (int i = 0; i < ss.size(); i++) {
218: logger.info("Starting translation of argument formula " + i
219: + " ...");
220: Formula formTranslation = translate(ss.get(i).formula());
221: logger.info("Finished translation of argument formula " + i
222: + "!");
223: logger.debug("Formula: " + ss.get(i).formula());
224: if (formTranslation != null) {
225: logger.debug("was translated into: " + formTranslation);
226: translations.add(formTranslation);
227: } else {
228: logger
229: .debug("...could not be translated, will be ignored!");
230: }
231: }
232: logger
233: .info("All argument formulae of this semisequent have been tranlated! ");
234:
235: // Assemble the translated Formulae to a new Formula, using the defined connective
236: Formula connectedCf = null;
237: logger.info("Starting to assemble the " + translations.size()
238: + " formulae...");
239: if (translations.size() > 1) {
240: connectedCf = (Formula) translations.get(0);
241: logger.debug("Done with first formula!");
242: for (int i = 1; i < translations.size(); i++) {
243: Formula[] helper = { connectedCf,
244: (Formula) translations.get(i) };
245: connectedCf = new ConnectiveFormula(connective, helper);
246: logger.debug("Integrated " + (i + 1) + ". formula!");
247: }
248: } else if (translations.size() == 1) {
249: connectedCf = (Formula) translations.get(0);
250: logger.debug("Done with first formula!");
251: } else if (translations.size() == 0) {
252: // if the semisequent is empty, use semantically equivalent constructs
253: logger
254: .debug("Found empty semisequent (after translation), returning constant!");
255: if (skolemization == ANTECEDENT)
256: connectedCf = new TruthValueFormula(true);
257: else
258: connectedCf = new TruthValueFormula(false);
259: }
260: logger.info("Assembled all formulae for semisequent!");
261: return connectedCf;
262: }
263:
264: /** Translates the given <tt>Term</tt> into SMT AUFLIA input syntax.<p>
265: * Thereby before doing the real translation, it is checked if the given <tt>Term</tt> can be
266: * translated into SMT AUFLIA syntax.<br>
267: * If so, it is translated and an according <tt>Formula</tt> (SMT-LIB) representing the
268: * translation result is returned. If not, <tt>null</tt> is returned
269: *
270: * @param toTranslate the <tt>Term</tt> which should be translated into SMT AUFLIA syntax
271: * @return a <tt>Formula</tt> (SMT-LIB) representing the translation of the given <tt>Term</tt>
272: */
273: private final Formula translate(Term toTranslate) {
274:
275: PreTranslationVisitor preTranslator = (PreTranslationVisitor) PreTranslationVisitor
276: .getInstance();
277: logger
278: .info("Checking translatability with PreTranslationVisitor...");
279: toTranslate.execPreOrder(preTranslator);
280: // No free variables must occur in term toTranslate
281: if (((Boolean) preTranslator.getTranslationResult())
282: .booleanValue()) {
283: if (preTranslator.noFreeVariableOccurrences(toTranslate)) {
284: logger
285: .info("Formula is translatable, executing PostOrderVisitor...");
286: try {
287: toTranslate.execPostOrder(ttVisitor);
288: } catch (RuntimeException e) {
289: ttVisitor.reset();
290: logger.info(
291: "Visitor failed, skipping current formula",
292: e);
293: logger.debug("Reseted TermTranslationVisitor!");
294: throw e;
295: // return null; TODO remove throw (it is only for debugging), uncomment this!
296: }
297: logger.info("Visitor completed, fetching result");
298: return (Formula) ttVisitor.getTranslationResult();
299: }
300: }
301: logger.info("Formula is not translatable!");
302: return null;
303: }
304:
305: // Helper functions for identifier translation from KeY names to allowed names in SMT-LIB
306:
307: /** Converts an arbitrary identifier (as <tt>String</tt>) into a legal SMT-LIB identifier
308: * <p>
309: * An identifier thereby is legal according to the SMT-LIB specifications, if it contains
310: * letters, digits and '_', '.' or ''' only.<br>
311: * The following replacements are done by this method:
312: * <ul>
313: * <li>Letters and digits remain untouched</li>
314: * <li>The characters '_', '.' and ''' also remain untouched</li>
315: * <li>The characters '<' and '>' are replaced by '.'</li>
316: * <li>All unmentioned characters are replaced by '_'</li>
317: * </ul>
318: * Further on, all sequences of "_" are replaced by a single "_" character in the end
319: *
320: * @param identifier the identifier to be converted
321: * @return a legal identifier according to SMT-LIB specifications, built upon the given
322: * identifier
323: */
324: public static final String legaliseIdentifier(String identifier) {
325: StringBuffer legalIdentifier = new StringBuffer();
326: if (legaliseSymbol['a'] != 'a')
327: initialiseLegalSymbols();
328: for (int i = 0; i < identifier.length(); i++) {
329: legalIdentifier
330: .append(legaliseSymbol[identifier.charAt(i)]);
331: }
332: return legalIdentifier.toString().replaceAll("__", "_");
333: }
334:
335: /** Initialises the static <tt>legaliseSymbol</tt> array */
336: private static final void initialiseLegalSymbols() {
337: for (int i = 0; i < legaliseSymbol.length; i++)
338: legaliseSymbol[i] = '_';
339: // Legal symbols
340: for (int i = 'a'; i <= 'z'; i++)
341: legaliseSymbol[i] = (char) i;
342: for (int i = 'A'; i <= 'Z'; i++)
343: legaliseSymbol[i] = (char) i;
344: for (int i = '0'; i <= '9'; i++)
345: legaliseSymbol[i] = (char) i;
346: legaliseSymbol['.'] = '.';
347: legaliseSymbol['\''] = '\'';
348: // Replacements
349: legaliseSymbol[':'] = '_';
350: legaliseSymbol['<'] = '\'';
351: legaliseSymbol['>'] = '\'';
352: }
353:
354: }
|