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.proof.init;
009:
010: import de.uka.ilkd.key.collection.SetAsListOfString;
011: import de.uka.ilkd.key.collection.SetOfString;
012: import de.uka.ilkd.key.gui.Main;
013: import de.uka.ilkd.key.gui.configuration.ProofSettings;
014: import de.uka.ilkd.key.logic.Name;
015: import de.uka.ilkd.key.proof.*;
016: import de.uka.ilkd.key.proof.decproc.JavaDecisionProcedureTranslationFactory;
017: import de.uka.ilkd.key.proof.mgt.AxiomJustification;
018: import de.uka.ilkd.key.proof.mgt.RuleJustification;
019: import de.uka.ilkd.key.rule.AbstractIntegerRule;
020: import de.uka.ilkd.key.rule.ListOfBuiltInRule;
021: import de.uka.ilkd.key.rule.Rule;
022: import de.uka.ilkd.key.rule.SLListOfBuiltInRule;
023: import de.uka.ilkd.key.strategy.IteratorOfStrategyFactory;
024: import de.uka.ilkd.key.strategy.SetAsListOfStrategyFactory;
025: import de.uka.ilkd.key.strategy.SetOfStrategyFactory;
026: import de.uka.ilkd.key.strategy.StrategyFactory;
027: import de.uka.ilkd.key.util.ProgressMonitor;
028:
029: public abstract class AbstractProfile implements Profile {
030:
031: private Main main;
032:
033: private AbstractExecDecproc[] execDecprocs;
034:
035: private final RuleCollection standardRules;
036:
037: private final SetOfStrategyFactory strategies;
038:
039: private final SetOfString supportedGC;
040: private final SetOfGoalChooserBuilder supportedGCB;
041:
042: private GoalChooserBuilder prototype;
043:
044: protected AbstractProfile(String standardRuleFilename,
045: SetOfGoalChooserBuilder supportedGCB, Main main) {
046:
047: // First initialise execDecproc, because it is used in initBuiltInRules()!
048: int concreteDecprocs = ConcreteExecDecproc.getDecprocNumber();
049: execDecprocs = new AbstractExecDecproc[concreteDecprocs + 1]; // +1 for later added dec procs!
050: for (int i = 0; i < concreteDecprocs; i++) {
051: execDecprocs[i] = new ConcreteExecDecproc(i);
052: }
053: // Add dec procs that cannot be treated uniformly within ConcreteExecDecproc
054: execDecprocs[concreteDecprocs++] = new ExecSVC();
055:
056: standardRules = new RuleCollection(RuleSource
057: .initRuleFile(standardRuleFilename), initBuiltInRules());
058: strategies = getStrategyFactories();
059: this .supportedGCB = supportedGCB;
060: this .supportedGC = extractNames(supportedGCB);
061: this .prototype = getDefaultGoalChooserBuilder();
062: assert (this .prototype != null);
063:
064: }
065:
066: private static SetOfString extractNames(
067: SetOfGoalChooserBuilder supportedGCB) {
068:
069: SetOfString result = SetAsListOfString.EMPTY_SET;
070:
071: final IteratorOfGoalChooserBuilder it = supportedGCB.iterator();
072: while (it.hasNext()) {
073: result = result.add(it.next().name());
074: }
075:
076: return result;
077: }
078:
079: public AbstractProfile(String standardRuleFilename) {
080: this (standardRuleFilename, null);
081: }
082:
083: public AbstractProfile(String standardRuleFilename, Main main) {
084: this (standardRuleFilename,
085: SetAsListOfGoalChooserBuilder.EMPTY_SET
086: .add(new DefaultGoalChooserBuilder()), main);
087: }
088:
089: public RuleCollection getStandardRules() {
090: return standardRules;
091: }
092:
093: protected SetOfStrategyFactory getStrategyFactories() {
094: return SetAsListOfStrategyFactory.EMPTY_SET;
095: }
096:
097: protected ListOfBuiltInRule initBuiltInRules() {
098: ListOfBuiltInRule builtInRules = SLListOfBuiltInRule.EMPTY_LIST;
099:
100: final ProgressMonitor monitor = main == null ? null : main
101: .getProgressMonitor();
102: if (monitor != null) {
103: monitor.setMaximum(execDecprocs.length);
104: }
105: if (main != null) {
106: main
107: .setStatusLine("Check for available decision procedures");
108: }
109:
110: // check whether decisionProcedure is in $PATH. If not, the
111: // taclet "Run Decision Procedure" won't be available.
112:
113: for (int i = 0; i < execDecprocs.length; i++) {
114:
115: if (execDecprocs[i].isAvailable()) {
116: final AbstractIntegerRule iRule = execDecprocs[i]
117: .getRule();
118:
119: builtInRules = builtInRules
120: .prepend(iRule
121: .clone(new JavaDecisionProcedureTranslationFactory()));
122: if (main != null) {
123: main.setStatusLine("Found: "
124: + execDecprocs[i].getCmd());
125: }
126: }
127: if (monitor != null) {
128: monitor.setProgress(i);
129: }
130: }
131: if (main != null) {
132: main.setStandardStatusLine();
133: }
134: return builtInRules;
135: }
136:
137: public SetOfStrategyFactory supportedStrategies() {
138: return strategies;
139: }
140:
141: public boolean supportsStrategyFactory(Name strategy) {
142: return getStrategyFactory(strategy) != null;
143: }
144:
145: public StrategyFactory getStrategyFactory(Name n) {
146: IteratorOfStrategyFactory it = getStrategyFactories()
147: .iterator();
148: while (it.hasNext()) {
149: final StrategyFactory sf = it.next();
150: if (sf.name().equals(n)) {
151: return sf;
152: }
153: }
154: return null;
155: }
156:
157: /**
158: * returns the names of the supported goal chooser
159: * builders
160: */
161: public SetOfString supportedGoalChoosers() {
162: return supportedGC;
163: }
164:
165: /**
166: * returns the default builder for a goal chooser
167: * @return this implementation returns a new instance of
168: * {@link DefaultGoalChooserBuilder}
169: */
170: public GoalChooserBuilder getDefaultGoalChooserBuilder() {
171: return new DefaultGoalChooserBuilder();
172: }
173:
174: /**
175: * sets the user selected goal chooser builder to be used as prototype
176: * @throws IllegalArgumentException if a goal chooser of the given name is not
177: * supported
178: */
179: public void setSelectedGoalChooserBuilder(String name) {
180:
181: this .prototype = lookupGC(name);
182:
183: if (this .prototype == null) {
184: throw new IllegalArgumentException("Goal chooser:" + name
185: + " is not supported by this profile.");
186: }
187: }
188:
189: /**
190: * looks up the demanded goal chooser is supported and returns a
191: * new instance if possible otherwise <code>null</code> is returned
192: *
193: * @param name the String with the goal choosers name
194: * @return a new instance of the builder or <code>null</code> if the
195: * demanded chooser is not supported
196: */
197: public GoalChooserBuilder lookupGC(String name) {
198: final IteratorOfGoalChooserBuilder it = supportedGCB.iterator();
199: while (it.hasNext()) {
200: final GoalChooserBuilder supprotedGCB = it.next();
201: if (supprotedGCB.name().equals(name)) {
202: return supprotedGCB.copy();
203: }
204: }
205: return null;
206: }
207:
208: /**
209: * returns a copy of the selected goal choooser builder
210: */
211: public GoalChooserBuilder getSelectedGoalChooserBuilder() {
212: return prototype.copy();
213: }
214:
215: /**
216: * any standard rule has is by default justified by an axiom rule
217: * justification
218: * @return the justification for the standardrules
219: */
220: public RuleJustification getJustification(Rule r) {
221: return AxiomJustification.INSTANCE;
222: }
223:
224: /**
225: * sets the given settings to some default depending on the profile
226: */
227: public void updateSettings(ProofSettings settings) {
228: }
229: }
|