01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: // This file is part of KeY - Integrated Deductive Software Design
09: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.proof.init;
19:
20: import java.io.IOException;
21: import de.uka.ilkd.key.proof.decproc.JavaDecisionProcedureTranslationFactory;
22: import de.uka.ilkd.key.rule.AbstractIntegerRule;
23: import de.uka.ilkd.key.rule.SVCIntegerRule;
24:
25: /** This class checks if the external decision procedure SVC is available.
26: * <p>
27: * If therefore creates a new process and passes data, formatted as an SMT-Lib Benchmark,
28: * to its input stream. If svc is available, it will terminate normally. (Without passing
29: * syntactically correct data, it won't terminate normally
30: *
31: * @author akuwertz
32: * @version 1.0, 09/11/2006
33: */
34:
35: public class ExecSVC extends AbstractExecDecproc {
36:
37: /** The command used to execute SVC */
38: private static final String cmd = "svc";
39:
40: /* (non-Javadoc)
41: * @see de.uka.ilkd.key.proof.init.AbstractExecDecproc#isAvailable()
42: */
43: public boolean isAvailable() {
44: String benchmark = "(benchmark test :logic QF_AUFLIA :formula false)";
45: boolean available = false;
46: Process process = null;
47: try {
48: process = Runtime.getRuntime().exec(cmd);
49: process.getOutputStream().write(benchmark.getBytes());
50: process.getOutputStream().close();
51: long start = System.currentTimeMillis();
52: while (System.currentTimeMillis() - start < TIMEOUT) {
53: try {
54: available = process.exitValue() == 0;
55: } catch (IllegalThreadStateException itse) {
56: // process has not terminated yet
57: available = false;
58: continue;
59: }
60: break;
61: }
62: } catch (IOException e) {
63: available = false;
64: }
65: return available;
66: }
67:
68: /* (non-Javadoc)
69: * @see de.uka.ilkd.key.proof.init.AbstractExecDecproc#getRule()
70: */
71: public AbstractIntegerRule getRule() {
72: return new SVCIntegerRule(
73: new JavaDecisionProcedureTranslationFactory());
74: }
75:
76: /* (non-Javadoc)
77: * @see de.uka.ilkd.key.proof.init.AbstractExecDecproc#getCmd()
78: */
79: public String getCmd() {
80: return cmd;
81: }
82: }
|