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: package de.uka.ilkd.key.visualdebugger;
009:
010: import java.util.Iterator;
011: import java.util.LinkedList;
012: import java.util.List;
013:
014: import de.uka.ilkd.key.gui.RuleAppListener;
015: import de.uka.ilkd.key.proof.*;
016: import de.uka.ilkd.key.proof.init.ProofOblInput;
017: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
018: import de.uka.ilkd.key.proof.proofevent.IteratorOfNodeReplacement;
019: import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
020: import de.uka.ilkd.key.rule.*;
021: import de.uka.ilkd.key.strategy.Strategy;
022: import de.uka.ilkd.key.util.ProgressMonitor;
023:
024: /**
025: * Starts and runs a proof attempt mostly separated from the rest of the KeY
026: * system. It may be used for non-user visible sub proofs.
027: */
028: public class ProofStarter {
029:
030: private IGoalChooser goalChooser;
031:
032: private int maxSteps = -1;
033:
034: private ProofOblInput po;
035:
036: private Proof proof;
037:
038: private Strategy strategy;
039:
040: private List progressMonitors = new LinkedList();
041:
042: private boolean useDecisionProcedures;
043:
044: /** creates an instance of this proof starter */
045: public ProofStarter() {
046: this .goalChooser = new DefaultGoalChooser();
047: // for the moment to maintain old default
048: useDecisionProcedures = true;
049: }
050:
051: /**
052: * applies rules that are chosen by the active strategy
053: *
054: * @return true iff a rule has been applied, false otherwise
055: */
056: private synchronized boolean applyAutomaticRule() {
057:
058: // Look for the strategy ...
059: RuleApp app = null;
060: Goal g;
061:
062: while ((g = goalChooser.getNextGoal()) != null) {
063:
064: app = g.getRuleAppManager().next();
065:
066: if (app == null)
067: goalChooser.removeGoal(g);
068: else
069: break;
070: }
071: if (app == null)
072: return false;
073:
074: if (g != null) {
075: goalChooser.updateGoalList(g.node(), g.apply(app));
076: }
077:
078: return true;
079: }
080:
081: // - Note: This should be removed
082: private void applySimplificationOnGoals(ListOfGoal goals,
083: BuiltInRule decisionProcedureRule) {
084: if (goals.isEmpty()) {
085: return;
086: }
087:
088: final Proof p = goals.head().node().proof();
089:
090: final IteratorOfGoal i = goals.iterator();
091: p.env().registerRule(decisionProcedureRule,
092: de.uka.ilkd.key.proof.mgt.AxiomJustification.INSTANCE);
093: while (i.hasNext()) {
094: final Goal g = i.next();
095: final BuiltInRuleApp birApp = new BuiltInRuleApp(
096: decisionProcedureRule, null, p.getUserConstraint()
097: .getConstraint());
098: g.apply(birApp);
099: }
100: }
101:
102: /**
103: * returns the proof resulting from the proof attempt
104: *
105: * @return the proof
106: */
107: public Proof getProof() {
108: return proof;
109: }
110:
111: /**
112: * initializes the proof starter, i.e. the proof is created and set up
113: *
114: * @param po
115: * the ProofOblInput with the proof (proof attempt is only
116: * started on the first proof)
117: */
118: public void init(ProofOblInput po) {
119:
120: if (this .po != null) {
121: throw new IllegalStateException(
122: "Proofstarter has been already" + " instantiated.");
123: }
124:
125: this .po = po;
126: this .proof = po.getPO().getFirstProof();
127: }
128:
129: /**
130: * informs the registered progress monitors about the current progress (i.e.
131: * the number of rules applied until now)
132: * @param progress the int counting the number of applied rules
133: */
134: private void informProgressMonitors(int progress) {
135: final Iterator it = progressMonitors.iterator();
136: while (it.hasNext()) {
137: ((ProgressMonitor) it.next()).setProgress(progress);
138: }
139: }
140:
141: /**
142: * initialises the registered progress monitors with the maximal
143: * steps to be performed
144: * @param maxSteps an int indicating the maximal steps to be performed
145: */
146: private void initProgressMonitors(int maxSteps) {
147: final Iterator it = progressMonitors.iterator();
148: while (it.hasNext()) {
149: ((ProgressMonitor) it.next()).setMaximum(maxSteps);
150: }
151: }
152:
153: /**
154: * adds a progress monitor to the proof starter. The progress monitor will
155: * be informed about the progress when performing a proof search. Therefore
156: * its {@link ProgressMonitor#setMaximum(int)} will be called handing over the
157: * maximal number of rule steps to be performed before the proof attempt is stopped.
158: * After each rule application the monitor will receive a call to
159: * {@link ProgressMonitor#setProgress(int)}
160: *
161: * @param pm the ProgressMonitor to be added
162: */
163: public void addProgressMonitor(ProgressMonitor pm) {
164: synchronized (progressMonitors) {
165: if (!progressMonitors.contains(pm)) {
166: progressMonitors.add(pm);
167: }
168: }
169: }
170:
171: /**
172: * removes <code>pm</code> from the list of progress monitor to be informed
173: * @param pm the ProgressMonitor to be removed
174: */
175: public void removeProgressMonitor(ProgressMonitor pm) {
176: synchronized (progressMonitors) {
177: progressMonitors.remove(pm);
178: }
179: }
180:
181: /**
182: * starts a proof attempt
183: * @param env the ProofEnvironment to which the proof object will be registered
184: * @return <code>true</code> if the proof attempt terminated normally (i.e. no error has occured).
185: * In particular <code>true</code> does <em>not</em> mean that the proof has been closed.
186: */
187: public boolean run(ProofEnvironment env) {
188: if (proof == null) {
189: throw new IllegalStateException(
190: "Proofstarter must be initialized before.");
191: }
192:
193: final Strategy oldStrategy = proof.getActiveStrategy();
194: if (strategy == null) {
195: // in this case take the strategy of the proof settings
196: setStrategy(proof.getActiveStrategy());
197: } else {
198: proof.setActiveStrategy(strategy);
199: }
200:
201: if (maxSteps == -1) {
202: // take default settings
203: setMaxSteps(proof.getSettings().getStrategySettings()
204: .getMaxSteps());
205: }
206:
207: final BuiltInRule decisionProcedureRule;
208: if (useDecisionProcedures) {
209: decisionProcedureRule = findSimplifyRule();
210: } else {
211: decisionProcedureRule = null;
212: }
213:
214: env.registerProof(po, po.getPO());
215:
216: goalChooser.init(proof, proof.openGoals());
217: final ProofListener pl = new ProofListener();
218:
219: Goal.addRuleAppListener(pl);
220:
221: try {
222:
223: int countApplied = 0;
224: synchronized (progressMonitors) {
225: initProgressMonitors(maxSteps);
226: while (countApplied < maxSteps && applyAutomaticRule()) {
227: countApplied++;
228: informProgressMonitors(countApplied);
229: }
230: }
231: if (useDecisionProcedures && decisionProcedureRule != null) {
232: applySimplificationOnGoals(proof.openGoals(),
233: decisionProcedureRule);
234: }
235: } catch (Throwable e) {
236: System.err.println(e);
237: e.printStackTrace();
238: return false;
239: } finally {
240: Goal.removeRuleAppListener(pl);
241: env.removeProofList(po.getPO());
242: proof.setActiveStrategy(oldStrategy);
243: }
244:
245: return true;
246: }
247:
248: /**
249: * returns the decision procedure rule invoking simplify, if available otherwise null
250: * is returned
251: * @return the decision procedure calling Simplify or null if none has been found
252: */
253: private BuiltInRule findSimplifyRule() {
254: BuiltInRule decisionProcedureRule = null;
255: final IteratorOfBuiltInRule builtinRules = proof.getSettings()
256: .getProfile().getStandardRules()
257: .getStandardBuiltInRules().iterator();
258: while (builtinRules.hasNext()) {
259: final BuiltInRule bir = builtinRules.next();
260: if (bir instanceof SimplifyIntegerRule) {
261: decisionProcedureRule = bir;
262: break;
263: }
264: }
265: return decisionProcedureRule;
266: }
267:
268: /**
269: * sets the maximal amount of steps to be performed
270: *
271: * @param maxSteps
272: * the int limiting the maximal amount of steps done in
273: * automatic proof mode
274: * @throws an
275: * IllegalArgumentException if <tt>maxSteps</tt> is lesser
276: * than zero
277: */
278: public void setMaxSteps(int maxSteps) {
279: if (maxSteps < 0) {
280: throw new IllegalArgumentException(
281: "Number of maximal proof"
282: + " steps must be zero or positive.");
283: }
284: this .maxSteps = maxSteps;
285: }
286:
287: /**
288: * sets the strategy to be used for the prove attempt
289: *
290: * @param strategy
291: * the Strategy to use
292: */
293: public void setStrategy(Strategy strategy) {
294: this .strategy = strategy;
295: }
296:
297: private class ProofListener implements RuleAppListener {
298:
299: /** invoked when a rule has been applied */
300: public void ruleApplied(ProofEvent e) {
301: if (e.getSource() != proof)
302: return;
303:
304: RuleAppInfo rai = e.getRuleAppInfo();
305: if (rai == null)
306: return;
307:
308: synchronized (ProofStarter.this ) {
309: ListOfGoal newGoals = SLListOfGoal.EMPTY_LIST;
310: IteratorOfNodeReplacement it = rai
311: .getReplacementNodes();
312: Node node;
313: Goal goal;
314:
315: while (it.hasNext()) {
316: node = it.next().getNode();
317: goal = proof.getGoal(node);
318: if (goal != null)
319: newGoals = newGoals.prepend(goal);
320: }
321:
322: goalChooser.updateGoalList(rai.getOriginalNode(),
323: newGoals);
324: }
325: }
326:
327: }
328:
329: /**
330: * if activated the proof starter will run decision procedures on all open goals
331: * after the normal proof search has stopped.
332: * @param useDecisionProcedures the boolean if <tt>true</tt> activates otherwise disables
333: * running the decision procedures
334: */
335: public void setUseDecisionProcedure(boolean useDecisionProcedures) {
336: this.useDecisionProcedures = useDecisionProcedures;
337: }
338:
339: }
|