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