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 de.uka.ilkd.key.gui.ExceptionDialog;
021: import de.uka.ilkd.key.gui.KeYMediator;
022: import de.uka.ilkd.key.gui.Main;
023: import de.uka.ilkd.key.gui.SwingWorker;
024: import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent;
025: import de.uka.ilkd.key.proof.IteratorOfGoal;
026: import de.uka.ilkd.key.proof.Proof;
027: import de.uka.ilkd.key.rule.*;
028: import de.uka.ilkd.key.util.ExceptionHandlerException;
029: import de.uka.ilkd.key.util.KeYExceptionHandler;
030:
031: public class DecProcRunner implements Runnable {
032:
033: Main main;
034: KeYMediator mediator;
035: String currentDecProc;
036:
037: Proof proof = null;
038: int totalGoals = 0;
039: KeYExceptionHandler exceptionHandler = null;
040:
041: private SwingWorker worker;
042:
043: public DecProcRunner(Main main) {
044: this .main = main;
045: mediator = main.mediator();
046: currentDecProc = mediator.getProof().getSettings()
047: .getDecisionProcedureSettings().getDecisionProcedure();
048: exceptionHandler = mediator.getExceptionHandler();
049: }
050:
051: public void run() {
052: /* Invoking start() on the SwingWorker causes a new Thread
053: * to be created that will call construct(), and then
054: * finished(). Note that finished() is called even if
055: * the worker is interrupted because we catch the
056: * InterruptedException in doWork().
057: */
058: worker = new SwingWorker() {
059: public Object construct() {
060: Object res = doWork();
061: return res;
062: }
063:
064: public void finished() {
065: mediator.startInterface(true);
066: Main main = Main.getInstance();
067: String msg = (String) get();
068: if (!"".equals(msg)) {
069: if (Main.batchMode) {
070: System.exit(-1);
071: } else {
072: // mediator.notify(new GeneralFailureEvent(re.getMessage()));
073: new ExceptionDialog(main, exceptionHandler
074: .getExceptions());
075: exceptionHandler.clear();
076: }
077: } else {
078: int nrGoalsClosed = mediator
079: .getNrGoalsClosedByAutoMode();
080: main.setStatusLine(currentDecProc + ": "
081: + totalGoals
082: + (totalGoals != 1 ? " goals" : " goal")
083: + " processed, " + nrGoalsClosed
084: + (nrGoalsClosed != 1 ? " goals" : " goal")
085: + " could be closed!");
086: if (nrGoalsClosed > 0
087: && !mediator.getProof().closed()) {
088: final String informationMsg = nrGoalsClosed
089: + ((nrGoalsClosed > 1) ? " goals have been closed"
090: : " goal has been closed");
091: mediator.notify(new GeneralInformationEvent(
092: informationMsg));
093: }
094:
095: }
096: }
097: };
098: mediator.stopInterface(true);
099: worker.start();
100: }
101:
102: private Object doWork() {
103: String status = "";
104: mediator.resetNrGoalsClosedByHeuristics();
105: try {
106: try {
107: totalGoals = mediator.getProof().openGoals().size();
108: int cnt = 0;
109: IteratorOfGoal i = mediator.getProof().openGoals()
110: .iterator();
111: BuiltInRule simpRule = null;
112: mediator.stopInterface(true);
113: mediator.setInteractive(false);
114: main.setStatusLine(
115: "Running external decision procedure: "
116: + currentDecProc, totalGoals);
117: while (i.hasNext()) {
118: //AR: %% GUI-Rule separation, many rule instances:
119: if (mediator.getProof().getSettings()
120: .getDecisionProcedureSettings()
121: .useSimplify())
122: simpRule = new SimplifyIntegerRule(
123: false,
124: new JavaDecisionProcedureTranslationFactory());
125: else if (mediator.getProof().getSettings()
126: .getDecisionProcedureSettings().useICS())
127: simpRule = new ICSIntegerRule(
128: false,
129: new JavaDecisionProcedureTranslationFactory());
130: else if (mediator.getProof().getSettings()
131: .getDecisionProcedureSettings()
132: .useCVCLite())
133: simpRule = new CVCLiteIntegerRule(
134: false,
135: new JavaDecisionProcedureTranslationFactory());
136: else if (mediator.getProof().getSettings()
137: .getDecisionProcedureSettings().useCVC3())
138: simpRule = new CVC3IntegerRule(
139: false,
140: new JavaDecisionProcedureTranslationFactory());
141: else if (mediator.getProof().getSettings()
142: .getDecisionProcedureSettings().useSVC())
143: simpRule = new SVCIntegerRule(
144: false,
145: new JavaDecisionProcedureTranslationFactory());
146: else if (mediator.getProof().getSettings()
147: .getDecisionProcedureSettings().useYices())
148: simpRule = new YicesIntegerRule(
149: false,
150: new JavaDecisionProcedureTranslationFactory());
151: else if (mediator.getProof().getSettings()
152: .getDecisionProcedureSettings()
153: .useSMT_Translation())
154: simpRule = new SmtTranslationIntegerRule(
155: false,
156: new JavaDecisionProcedureTranslationFactory());
157:
158: BuiltInRuleApp birApp = new BuiltInRuleApp(
159: simpRule, null, mediator
160: .getUserConstraint()
161: .getConstraint());
162: mediator
163: .getProof()
164: .env()
165: .registerRule(
166: simpRule,
167: de.uka.ilkd.key.proof.mgt.AxiomJustification.INSTANCE);
168: i.next().apply(birApp);
169: cnt++;
170: main.getProgressMonitor().setProgress(cnt);
171: }
172: // main.setStandardStatusLine();
173: } catch (ExceptionHandlerException e) {
174: throw e;
175: } catch (Throwable thr) {
176: exceptionHandler.reportException(thr);
177: }
178: } catch (ExceptionHandlerException ex) {
179: main
180: .setStatusLine("Running external decision procedure failed");
181: status = ex.toString();
182: }
183: return status;
184: }
185:
186: }
|