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 SVC 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/29/2006
033: */
034:
035: public class DecisionProcedureSVC extends DecisionProcedureSmtAuflia {
036:
037: /** A <tt>String</tt> representation of the command used to execute SVC */
038: private static final String SVCCommand = "svc";
039:
040: /** A <tt>String</tt> representing the answer of SVC if it found a benchmark to be
041: * unsatisfiable */
042: private static final String SVCUnsatAnwser = "unsat";
043:
044: /** A <tt>Logger</tt> for monitoring and logging of progress in the decision procedure */
045: private static final Logger logger = Logger
046: .getLogger(DecisionProcedureSVC.class.getName());
047:
048: // Logger is created hierarchical to inherit configuration and behaviour from parent
049:
050: /** A mere constructor.
051: *
052: * @param goal the <tt>Goal</tt> which should be checked for satisfiability
053: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> used to ranslate the the
054: * sequent of the goal
055: * @param services the <tt>Services</tt> used during the translation process
056: */
057: public DecisionProcedureSVC(Goal goal,
058: DecisionProcedureTranslationFactory dptf, Services services) {
059: super (goal, dptf, services);
060: }
061:
062: /** This method is reponsible executing and evaluating SVC. It implements the hook provided in
063: * <tt>DecisionProcedureSmtAuflia</tt>
064: *
065: * @throws RuntimeException if an <tt>Exception</tt> occured due to the invocation or
066: * execution of SVC
067: */
068: protected DecisionProcedureResult execDecProc() {
069:
070: try {
071: // Run SVC on stored translation result (benchmark)
072: logger.info("Running SVC on created benchmark...");
073: Process p = Runtime.getRuntime().exec(SVCCommand);
074: p.getOutputStream().write(
075: getResultBenchmark().toString().getBytes());
076: p.getOutputStream().close();
077: logger.info("SVC exection finished, processing results...");
078:
079: // Retrieve results
080: InputStream in = p.getInputStream();
081: String svcResult = read(in);
082: logger.debug("Retrieved result succussfully!");
083: in.close();
084:
085: // Create DecisionProcedureResult from SVC results
086: boolean result = svcResult.indexOf(SVCUnsatAnwser) >= 0;
087: return new DecisionProcedureResult(result, svcResult,
088: Constraint.BOTTOM);
089:
090: } catch (IOException e) {
091: logger.info("An IOException occured:", e);
092: final String errorMessage = "\"SVC\" execution failed:\n\n"
093: + e
094: + "\n\n"
095: + "To make use of SVC make sure that \n\n"
096: + "1. the binary is named svc "
097: + "2. the directory where the binary resides is in your $PATH variable\n"
098: + "3. the binary has executable file permissions.";
099: throw new RuntimeException(errorMessage);
100: }
101: }
102:
103: }
|