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