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: //
009: //
010:
011: package de.uka.ilkd.key.proof.decproc;
012:
013: import java.io.*;
014:
015: import org.apache.log4j.Logger;
016:
017: import de.uka.ilkd.key.java.Services;
018: import de.uka.ilkd.key.logic.Constraint;
019: import de.uka.ilkd.key.pp.LogicPrinter;
020: import de.uka.ilkd.key.pp.NotationInfo;
021: import de.uka.ilkd.key.pp.ProgramPrinter;
022: import de.uka.ilkd.key.proof.Goal;
023:
024: /**
025: This class invokes the decision procedure "ICS".
026: */
027:
028: public class DecisionProcedureICS extends AbstractDecisionProcedure {
029:
030: private static final String ICS_COMMAND = "ics";
031:
032: public static final String SPACER = "\\<---This is just a spacer between "
033: + "sequent and ICS input resp. ICS output--->\\";
034:
035: static Logger logger = Logger.getLogger(DecisionProcedureICS.class
036: .getName());
037:
038: public DecisionProcedureICS(Goal goal, Constraint userConstraint,
039: DecisionProcedureTranslationFactory dptf, Services services) {
040: super (goal, userConstraint, dptf, services);
041: }
042:
043: /**
044: * runs first the conversion into the Simplify syntax,
045: * and runs Simplify via a temporary file.
046: */
047: protected DecisionProcedureResult runInternal(
048: ConstraintSet constraintSet, boolean lightWeight) {
049: try {
050: ICSTranslation st = dptf.createICSTranslation(goal
051: .sequent(), constraintSet, goal.node()
052: .getRestrictedMetavariables(), this .services);
053:
054: /* It seems, there are problems with Process and
055: * Standard-IO. Even the simplest program doesn't work
056: * correctly with J2SE 1.4. But I haven't found a bug in
057: * Sun Bug Database.
058: *
059: * try {
060: * Process p = Runtime.getRuntime().exec("cat");
061: * OutputStream out = p.getOutputStream();
062: * InputStream in = p.getInputStream();
063: * out.write("Hello World!\n".getBytes());
064: * out.close();
065: * BufferedReader rd = new BufferedReader(new InputStreamReader(in));
066: * String s;
067: * while ((s = rd.readLine()) != null) {
068: * System.out.println("[" + s + "]");
069: * }
070: * } catch (IOException ioe) {
071: * ioe.printStackTrace();
072: * }
073: *
074: * Instead of control with Standard-IO, I control the
075: * simplify process with a temporary file. -hs. */
076:
077: File file = File.createTempFile("key-ics", null);
078: PrintWriter out = new PrintWriter(new FileWriter(file));
079: out.println(st.getText());
080:
081: logger.info(st.getText());
082:
083: out.close();
084:
085: Process p = Runtime.getRuntime().exec(
086: new String[] { ICS_COMMAND, file.getPath() });
087:
088: InputStream in = p.getInputStream();
089:
090: String response = read(in);
091: in.close();
092:
093: file.delete();
094:
095: // read the output from the command
096: logger.info("Here is what ICS has to say:\n");
097: logger.info(response);
098:
099: //This part is responsible for logging
100: String logdir = System.getProperty("key.ics.logdir");
101: if (logdir == null || logdir.trim().length() == 0) {
102: logger
103: .warn("$KEY_ICS_LOG_DIR is empty or non-existent. Logging (of proofs, not with log4j) of ICS disabled.");
104: } else {
105: try {
106: String logFileName = "ics-log_"
107: + getCurrentDateString() + ".log";
108: PrintWriter logfile = new PrintWriter(
109: new BufferedWriter(new FileWriter(new File(
110: logdir, logFileName))));
111: LogicPrinter sp = new LogicPrinter(
112: new ProgramPrinter(logfile), NotationInfo
113: .createInstance(), services);
114: sp.printSequent(goal.sequent());
115: logfile.print(sp.result().toString());
116: logfile.println(SPACER);
117: logfile.println(st.getText());
118: logfile.println(SPACER);
119: logfile.println(response);
120: logfile.close();
121: } catch (IOException ioe) {
122: logger.error("error while trying to log:\n" + ioe);
123: }
124: }
125: //End of logging part
126: //System.out.println(response.indexOf(":unsat"));
127: if (response.indexOf(":unsat") > -1) {
128: logger
129: .info("ICS has decided and found the negated formula to be unsatisfiable.");
130: return new DecisionProcedureResult(true, response,
131: Constraint.BOTTOM);
132: } else {
133: logger
134: .info("ICS has decided and found the negated formula to be satisfiable.");
135: return new DecisionProcedureResult(false, "",
136: Constraint.BOTTOM);
137: }
138: //constraintSet.chosenConstraint
139: } catch (IOException ioe) {
140: final String errorMessage = "\"ICS\" execution failed:\n\n"
141: + ioe + "\n\n"
142: + "To make use of ICS make sure that\n\n"
143: + "1. the binary is named ics\n"
144: + "2. the directory where the binary "
145: + "resides is in your $PATH variable\n"
146: + "3. the binary has executable file permissions.";
147: throw new RuntimeException(errorMessage);
148: } catch (SimplifyException se) {
149: return new DecisionProcedureResult(false, se.toString(),
150: Constraint.BOTTOM);
151: }
152: }
153:
154: }
|