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: package de.uka.ilkd.key.proof.init;
018:
019: import java.util.HashMap;
020: import java.util.Iterator;
021: import java.util.NoSuchElementException;
022: import java.util.Map.Entry;
023:
024: import de.uka.ilkd.key.gui.configuration.ProofSettings;
025: import de.uka.ilkd.key.java.Services;
026: import de.uka.ilkd.key.logic.*;
027: import de.uka.ilkd.key.logic.op.Op;
028: import de.uka.ilkd.key.logic.sort.GenericSort;
029: import de.uka.ilkd.key.logic.sort.Sort;
030: import de.uka.ilkd.key.proof.BuiltInRuleIndex;
031: import de.uka.ilkd.key.proof.ProofAggregate;
032: import de.uka.ilkd.key.proof.TacletIndex;
033: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
034: import de.uka.ilkd.key.rule.*;
035:
036: /**
037: * an instance of this class describes the initial configuration of the prover.
038: * This includes sorts, functions, heuristics, and variables namespaces,
039: * information on the underlying java model, and a set of rules.
040: */
041: public class InitConfig {
042:
043: /**
044: * the services class allowing to access information about the underlying
045: * program model
046: */
047: private final Services services;
048:
049: private final Profile profile;
050:
051: /**
052: * the proof environment this init config belongs to
053: */
054: private final ProofEnvironment env;
055:
056: private SetOfTaclet taclets = SetAsListOfTaclet.EMPTY_SET;
057:
058: /**
059: * maps categories to their default choice (both represented as Strings),
060: * which is used if no other choice is specified in the problemfile
061: */
062: private HashMap category2DefaultChoice = new HashMap();
063:
064: /**
065: * maps taclets to their TacletBuilders. This information is needed when
066: * a taclet contains GoalTemplates annotated with taclet-options because
067: * in this case a new taclet has to be created containing only those
068: * GoalTemplates whose options are activated and those who don't belong
069: * to any specific option.
070: */
071: private HashMap taclet2Builder = new HashMap();
072:
073: /**
074: * Set of the rule options activated for the current proof. The rule options
075: * ({@link Choice}s) allow to use different ruleset modelling or skipping
076: * certain features (e.g. nullpointer checks when resolving references)
077: */
078: private SetOfChoice activatedChoices = SetAsListOfChoice.EMPTY_SET;
079:
080: /** HashMap for quick lookups taclet name->taclet */
081: private HashMapFromNameToNamed quickTacletMap;
082:
083: //-------------------------------------------------------------------------
084: //constructors
085: //-------------------------------------------------------------------------
086:
087: public InitConfig(Services services, Profile profile) {
088: this .services = services;
089: this .profile = profile;
090: this .env = new ProofEnvironment(this );
091:
092: sortNS().add(Sort.NULL);
093: funcNS().add(Op.NULL);
094: category2DefaultChoice = ProofSettings.DEFAULT_SETTINGS
095: .getChoiceSettings().getDefaultChoices();
096: }
097:
098: public InitConfig() {
099: this (new Services(), null);
100: }
101:
102: //-------------------------------------------------------------------------
103: //internal methods
104: //-------------------------------------------------------------------------
105:
106: /**
107: * Helper for add().
108: */
109: private void addSorts(NamespaceSet ns, ModStrategy mod) {
110: final IteratorOfNamed sortsIt = ns.sorts().elements()
111: .iterator();
112: while (sortsIt.hasNext()) {
113: final Named named = sortsIt.next();
114: if (named instanceof GenericSort) {
115: if (mod.modifyGenericSorts())
116: sortNS().add(named);
117: } else {
118: if (mod.modifySorts())
119: sortNS().add(named);
120: }
121: }
122: }
123:
124: //-------------------------------------------------------------------------
125: //public interface
126: //-------------------------------------------------------------------------
127:
128: /**
129: * returns the Services of this initial configuration providing access
130: * to the used program model
131: * @return the Services of this initial configuration
132: */
133: public Services getServices() {
134: return services;
135: }
136:
137: public Profile getProfile() {
138: return profile;
139: }
140:
141: /**
142: * returns the proof environment using this initial configuration
143: * @return the ProofEnvironment using this configuration
144: */
145: public ProofEnvironment getProofEnv() {
146: assert env.getInitConfig() == this ;
147: return env;
148: }
149:
150: /**
151: * adds entries to the HashMap that maps categories to their
152: * default choices.
153: * Only entries of <code>init</init> with keys not already contained in
154: * category2DefaultChoice are added.
155: */
156: public void addCategory2DefaultChoices(HashMap init) {
157: Iterator it = init.entrySet().iterator();
158: boolean changed = false;
159: while (it.hasNext()) {
160: Entry entry = (Entry) it.next();
161: if (!category2DefaultChoice.containsKey(entry.getKey())) {
162: changed = true;
163: category2DefaultChoice.put(entry.getKey(), entry
164: .getValue());
165: }
166: }
167: if (changed) {
168: ProofSettings.DEFAULT_SETTINGS.getChoiceSettings()
169: .setDefaultChoices(
170: (HashMap) category2DefaultChoice.clone());
171: }
172: }
173:
174: public void setTaclet2Builder(HashMap taclet2Builder) {
175: this .taclet2Builder = taclet2Builder;
176: }
177:
178: /**
179: * {@link Taclet}s are constructed using {@link TacletBuilder}s this map
180: * contains the pair of a taclet and its builder which is important as
181: * goals of a taclet may depend of the selected choices. Instead of
182: * creating all possible combinations in advance this is done by demand
183: * @return the map from a taclet to its builder
184: */
185: public HashMap getTaclet2Builder() {
186: return taclet2Builder;
187: }
188:
189: /**
190: * sets the set of activated choices of this initial configuration.
191: * For categories without a specified choice the default choice contained
192: * in category2DefaultChoice is added.
193: */
194: public void setActivatedChoices(SetOfChoice activatedChoices) {
195: category2DefaultChoice = ProofSettings.DEFAULT_SETTINGS
196: .getChoiceSettings().getDefaultChoices();
197:
198: final IteratorOfChoice it = activatedChoices.iterator();
199: HashMap c2DC = (HashMap) category2DefaultChoice.clone();
200: Choice c;
201: while (it.hasNext()) {
202: c = it.next();
203: c2DC.remove(c.category());
204: }
205:
206: final Iterator itDef = c2DC.values().iterator();
207: while (itDef.hasNext()) {
208: String s = (String) itDef.next();
209: c = (Choice) choiceNS().lookup(new Name(s));
210: if (c != null) {
211: activatedChoices = activatedChoices.add(c);
212: }
213: }
214: this .activatedChoices = activatedChoices;
215:
216: // invalidate quick taclet cache
217: quickTacletMap = null;
218: }
219:
220: /** Returns the choices which are currently active.
221: * For getting the active choices for a specific proof,
222: * <code>getChoices</code> in <code>de.uka.ilkd.key.proof.Proof
223: * </code> has to be used.
224: */
225: public SetOfChoice getActivatedChoices() {
226: return activatedChoices;
227: }
228:
229: public void setTaclets(SetOfTaclet taclets) {
230: this .taclets = taclets;
231: }
232:
233: public SetOfTaclet getTaclets() {
234: return taclets;
235: }
236:
237: public Taclet lookupActiveTaclet(Name name) {
238: if (quickTacletMap == null) {
239: quickTacletMap = new HashMapFromNameToNamed();
240: IteratorOfTaclet it = activatedTaclets().iterator();
241: while (it.hasNext()) {
242: Taclet t = it.next();
243: quickTacletMap.put(t.name(), t);
244: IteratorOfName itOld = t.oldNames().iterator();
245: while (itOld.hasNext()) {
246: quickTacletMap.put(itOld.next(), t);
247: }
248: }
249: }
250:
251: return (Taclet) quickTacletMap.get(name);
252: }
253:
254: /**
255: * returns the activated taclets of this initial configuration
256: */
257: public SetOfTaclet activatedTaclets() {
258: IteratorOfTaclet it = taclets.iterator();
259: SetOfTaclet result = SetAsListOfTaclet.EMPTY_SET;
260: Taclet t;
261: TacletBuilder b;
262: while (it.hasNext()) {
263: t = it.next();
264: b = (TacletBuilder) taclet2Builder.get(t);
265: if (t.getChoices().subset(activatedChoices)) {
266: if (b != null && b.getGoal2Choices() != null) {
267: t = b
268: .getTacletWithoutInactiveGoalTemplates(activatedChoices);
269: }
270: if (t != null) {
271: result = result.add(t);
272: }
273: }
274: }
275: return result;
276: }
277:
278: /** returns the built-in rules of this initial configuration
279: */
280: public ListOfBuiltInRule builtInRules() {
281: return (profile == null ? SLListOfBuiltInRule.EMPTY_LIST
282: : profile.getStandardRules().getStandardBuiltInRules());
283: }
284:
285: /** returns a newly created taclet index for the set of activated
286: * taclets contained in this initial configuration
287: */
288: public TacletIndex createTacletIndex() {
289: return new TacletIndex(activatedTaclets());
290: }
291:
292: /**
293: * returns a new created index for built in rules (at the moment immutable
294: * list)
295: */
296: public BuiltInRuleIndex createBuiltInRuleIndex() {
297: return new BuiltInRuleIndex(builtInRules());
298: }
299:
300: /**
301: * returns the namespaces of this initial configuration
302: */
303: public NamespaceSet namespaces() {
304: return services.getNamespaces();
305: }
306:
307: /** returns the function namespace of this initial configuration
308: */
309: public Namespace funcNS() {
310: return namespaces().functions();
311: }
312:
313: /** returns the sort namespace of this initial configuration
314: */
315: public Namespace sortNS() {
316: return namespaces().sorts();
317: }
318:
319: /** returns the heuristics namespace of this initial configuration
320: */
321: public Namespace ruleSetNS() {
322: return namespaces().ruleSets();
323: }
324:
325: /** returns the variable namespace of this initial configuration
326: */
327: public Namespace varNS() {
328: return namespaces().variables();
329: }
330:
331: /** returns the program variable namespace of this initial configuration
332: */
333: public Namespace progVarNS() {
334: return namespaces().programVariables();
335: }
336:
337: /** returns the choice namespace of this initial configuration
338: */
339: public Namespace choiceNS() {
340: return namespaces().choices();
341: }
342:
343: public void createNamespacesForActivatedChoices() {
344: IteratorOfChoice it = activatedChoices.iterator();
345: while (it.hasNext()) {
346: Choice c = it.next();
347: funcNS().add(c.funcNS());
348: }
349: }
350:
351: public ProofSettings mergedProofSettings() {
352: ProofSettings defaultSettings = ProofSettings.DEFAULT_SETTINGS;
353: ProofAggregate someProof = null;
354: try {
355: someProof = ((ProofAggregate) getProofEnv().getProofs()
356: .iterator().next());
357: } catch (NoSuchElementException ne) {
358: }
359: if (someProof != null) {
360: return defaultSettings.setChoiceSettings(someProof
361: .getFirstProof().getSettings().getChoiceSettings());
362: } else {
363: return defaultSettings;
364: }
365: }
366:
367: /** adds namespaces to the namespaces of this initial configuration
368: */
369: public void add(NamespaceSet ns, ModStrategy mod) {
370: if (mod.modifyFunctions())
371: funcNS().add(ns.functions());
372: addSorts(ns, mod);
373: if (mod.modifyVariables())
374: varNS().add(ns.variables());
375: if (mod.modifyProgramVariables())
376: progVarNS().add(ns.programVariables());
377: if (mod.modifyHeuristics())
378: ruleSetNS().add(ns.ruleSets());
379: if (mod.modifyChoices())
380: choiceNS().add(ns.choices());
381: }
382:
383: /** returns a copy of this initial configuration copying the namespaces,
384: * the contained JavaInfo while using the immutable set of taclets in the
385: * copy
386: */
387: public InitConfig copy() {
388: InitConfig ic = new InitConfig(services
389: .copyPreservesLDTInformation(), profile);
390: ic.setActivatedChoices(activatedChoices);
391: ic.category2DefaultChoice = ((HashMap) category2DefaultChoice
392: .clone());
393: ic.setTaclet2Builder((HashMap) taclet2Builder.clone());
394: ic.setTaclets(taclets);
395: return ic;
396: }
397:
398: /**
399: * toString
400: */
401: public String toString() {
402: return "Namespaces:" + namespaces() + "\n" + "Services:"
403: + services + "\n" + "Taclets:" + getTaclets() + "\n"
404: + "Built-In:" + builtInRules() + "\n";
405: }
406: }
|