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 CVCLite 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, 05/08/2006
033: */
034:
035: public class DecisionProcedureCVCLite extends
036: DecisionProcedureSmtAuflia {
037:
038: /** A <tt>String</tt> representation of the command used to execute CVCLite */
039: private static final String CVCLiteCommand = "cvcl";
040: /** <tt>String</tt>s representing the CVCLite command option for SMT-LIB support */
041: private static final String CVCLiteSmtFlag1 = "-lang";
042: private static final String CVCLiteSmtFlag2 = "smtlib";
043: /** A <tt>String</tt> representing the answer of CVCLite if it found a benchmark to be
044: * unsatisfiable */
045: private static final String CVCLiteUnsatAnwser = "Unsatisfiable";
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(DecisionProcedureCVCLite.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 DecisionProcedureCVCLite(Goal goal,
061: DecisionProcedureTranslationFactory dptf, Services services) {
062: super (goal, dptf, services);
063: }
064:
065: /** This method is reponsible executing and evaluating CVCLite. 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 CVCLite
070: */
071: protected DecisionProcedureResult execDecProc() {
072:
073: try {
074: // Run CVCLite on stored translation result (benchmark)
075: logger.info("Running CVCLite on created benchmark...");
076: String[] cmdArray = { CVCLiteCommand, CVCLiteSmtFlag1,
077: CVCLiteSmtFlag2, super .getTempFile().getPath() };
078: Process p = Runtime.getRuntime().exec(cmdArray);
079: logger
080: .info("CVCLite exection finished, processing results...");
081:
082: // Retrieve results
083: InputStream in = p.getInputStream();
084: String cvcResult = read(in);
085: logger.debug("Retrieved result succussfully!");
086: in.close();
087:
088: // Create DecisionProcedureResult from CVCLite results
089: boolean result = cvcResult.indexOf(CVCLiteUnsatAnwser) >= 0;
090: return new DecisionProcedureResult(result, cvcResult,
091: Constraint.BOTTOM);
092:
093: } catch (IOException e) {
094: logger.info("An IOException occured:", e);
095: final String errorMessage = "\"CVCLite\" execution failed:\n\n"
096: + e
097: + "\n\n"
098: + "Currently, CVCLite supports only Linux operated systems!\n\n"
099: + "To make use of CVCLite make sure that \n\n"
100: + "1. the main shell script is named cvcl.sh\n"
101: + "2. the directory where the shell script resides is in your $PATH variable\n"
102: + "3. the shell script and the binary have executable file permissions.";
103: throw new RuntimeException(errorMessage);
104: }
105: }
106:
107: }
|