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: //
009: //
010: package de.uka.ilkd.key.proof.init;
011:
012: /** Describes if the parts of an initial configuration are to be modified
013: * or not when reading input to the prover.
014: */
015: public class ModStrategy {
016:
017: /** A constant strategy modifying always */
018: public static final ModStrategy MOD_ALL = new ModStrategy();
019: /** A strategy modifying everything except variables*/
020: public static final ModStrategy NO_VARS = new ModStrategy() {
021: public boolean modifyVariables() {
022: return false;
023: }
024: };
025:
026: /** A strategy modifying everything except variables and generic sorts*/
027: public static final ModStrategy NO_VARS_GENSORTS = new ModStrategy() {
028: public boolean modifyVariables() {
029: return false;
030: }
031:
032: public boolean modifyGenericSorts() {
033: return false;
034: }
035: };
036:
037: /** A strategy modifying everything except generic sorts*/
038: public static final ModStrategy NO_GENSORTS = new ModStrategy() {
039: public boolean modifyGenericSorts() {
040: return false;
041: }
042: };
043:
044: /** A strategy modifying everything except variables and functions*/
045: public static final ModStrategy NO_VARS_FUNCS = new ModStrategy() {
046: public boolean modifyVariables() {
047: return false;
048: }
049:
050: public boolean modifyProgramVariables() {
051: return false;
052: }
053:
054: public boolean modifyFunctions() {
055: return false;
056: }
057: };
058:
059: /** A strategy modifying everything except variables, functions and generic sorts*/
060: public static final ModStrategy NO_VARS_FUNCS_GENSORTS = new ModStrategy() {
061: public boolean modifyVariables() {
062: return false;
063: }
064:
065: public boolean modifyProgramVariables() {
066: return false;
067: }
068:
069: public boolean modifyFunctions() {
070: return false;
071: }
072:
073: public boolean modifyGenericSorts() {
074: return false;
075: }
076: };
077:
078: /** A strategy modifying everything except functions*/
079: public static final ModStrategy NO_FUNCS = new ModStrategy() {
080: public boolean modifyProgramVariables() {
081: return false;
082: }
083:
084: public boolean modifyFunctions() {
085: return false;
086: }
087: };
088:
089: /** returns true iff the heuristics namespace should be modified*/
090: public boolean modifyHeuristics() {
091: return true;
092: }
093:
094: /**
095: * returns true iff the sorts namespace should be modified concerning
096: * concrete sorts
097: */
098: public boolean modifySorts() {
099: return true;
100: }
101:
102: /**
103: * returns true iff the sorts namespace should be modified concerning
104: * generic sorts
105: */
106: public boolean modifyGenericSorts() {
107: return true;
108: }
109:
110: /** returns true iff the variable namespace should be modified*/
111: public boolean modifyVariables() {
112: return true;
113: }
114:
115: /** returns true iff the variable namespace should be modified*/
116: public boolean modifyProgramVariables() {
117: return true;
118: }
119:
120: /** returns true iff the functions namespace should be modified*/
121: public boolean modifyFunctions() {
122: return true;
123: }
124:
125: /** returns true iff the choice namespace should be modified*/
126: public boolean modifyChoices() {
127: return true;
128: }
129:
130: /** returns true iff the java model info should be modified*/
131: public boolean modifyJavaInfo() {
132: return true;
133: }
134:
135: }
|