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.io.IOException;
021: import java.io.InputStream;
022: import org.apache.log4j.Logger;
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.logic.Constraint;
025: import de.uka.ilkd.key.proof.Goal;
026:
027: /** /** This class is responsible for invoking the back-end decision procedure Yices on a
028: * <tt>Benchmark</tt>, evaluating its results and returning them represented properly to
029: * <tt>DecisionProcedureSmtAuflia</tt>
030: *
031: * @author akuwertz
032: * @version 1.0, 09/20/2006
033: */
034:
035: public class DecisionProcedureYices extends DecisionProcedureSmtAuflia {
036:
037: /** A <tt>String</tt> representation of the command used to execute Yices */
038: private static final String YicesCommand = "yices";
039:
040: /** <tt>String</tt>s representing the Yicese command option for SMT-LIB support */
041: private static final String YicesSmtFlag = "-smt";
042:
043: /** A <tt>String</tt> representing the answer of Yices if it found a benchmark to be
044: * unsatisfiable */
045: private static final String YicesUnsatAnwser = "unsat";
046:
047: /** A <tt>Logger</tt> for monitoring and logging of progress in the decision procedure */
048: private static final Logger logger = Logger
049: .getLogger(DecisionProcedureYices.class.getName());
050:
051: // Logger is created hierarchical to inherit configuration and behaviour from parent
052:
053: /** A mere constructor.
054: *
055: * @param goal the <tt>Goal</tt> which should be checked for satisfiability
056: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> used to ranslate the the
057: * sequent of the goal
058: * @param services the <tt>Services</tt> used during the translation process
059: */
060: public DecisionProcedureYices(Goal goal,
061: DecisionProcedureTranslationFactory dptf, Services services) {
062: super (goal, dptf, services);
063: }
064:
065: /** This method is reponsible executing and evaluating Yices. It implements the hook provided in
066: * <tt>DecisionProcedureSmtAuflia</tt>
067: *
068: * @throws RuntimeException if an <tt>Exception</tt> occured due to the invocation or
069: * execution of Yices
070: */
071: protected DecisionProcedureResult execDecProc() {
072:
073: try {
074: // Run Yices on stored translation result (benchmark)
075: logger.info("Running Yices on created benchmark...");
076:
077: String[] cmdArray = { YicesCommand, YicesSmtFlag,
078: super .getTempFile().getPath() };
079: Process p = Runtime.getRuntime().exec(cmdArray);
080: logger
081: .info("Yices exection finished, processing results...");
082:
083: // Retrieve results
084: InputStream in = p.getInputStream();
085: String yicesResult = read(in);
086: logger.debug("Retrieved result succussfully!");
087: in.close();
088:
089: // Create DecisionProcedureResult from Yices results
090: boolean result = yicesResult.indexOf(YicesUnsatAnwser) >= 0;
091: return new DecisionProcedureResult(result, yicesResult,
092: Constraint.BOTTOM);
093:
094: } catch (IOException e) {
095: logger.info("An IOException occured:", e);
096: final String errorMessage = "\"Yices\" execution failed:\n\n"
097: + e
098: + "\n\n"
099: + "To make use of Yices make sure that \n\n"
100: + "1. the binary is named yices "
101: + "2. the directory where the binary resides is in your $PATH variable\n"
102: + "3. the binary has executable file permissions.";
103: throw new RuntimeException(errorMessage);
104: }
105: }
106:
107: }
|