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:
011: package de.uka.ilkd.key.strategy;
012:
013: import java.util.Properties;
014:
015: public class StrategyProperties extends Properties {
016:
017: public final static String SPLITTING_OPTIONS_KEY = "SPLITTING_OPTIONS_KEY";
018: public final static String SPLITTING_NORMAL = "SPLITTING_NORMAL";
019: public final static String SPLITTING_OFF = "SPLITTING_OFF";
020: public final static String SPLITTING_DELAYED = "SPLITTING_DELAYED";
021:
022: public final static String LOOP_OPTIONS_KEY = "LOOP_OPTIONS_KEY";
023: public final static String LOOP_EXPAND = "LOOP_EXPAND";
024: public final static String LOOP_INVARIANT = "LOOP_INVARIANT";
025: public final static String LOOP_NONE = "LOOP_NONE";
026:
027: public final static String METHOD_OPTIONS_KEY = "METHOD_OPTIONS_KEY";
028: public final static String METHOD_EXPAND = "METHOD_EXPAND";
029: public final static String METHOD_CONTRACT = "METHOD_CONTRACT";
030: public final static String METHOD_NONE = "METHOD_NONE";
031:
032: public final static String QUERY_OPTIONS_KEY = "QUERY_OPTIONS_KEY";
033: public final static String QUERY_EXPAND = "QUERY_EXPAND";
034: public final static String QUERY_PROGRAMS_TO_RIGHT = "QUERY_PROGRAMS_TO_RIGHT";
035: public final static String QUERY_NONE = "QUERY_NONE";
036:
037: public final static String NON_LIN_ARITH_OPTIONS_KEY = "NON_LIN_ARITH_OPTIONS_KEY";
038: public final static String NON_LIN_ARITH_NONE = "NON_LIN_ARITH_NONE";
039: public final static String NON_LIN_ARITH_DEF_OPS = "NON_LIN_ARITH_DEF_OPS";
040: public final static String NON_LIN_ARITH_COMPLETION = "NON_LIN_ARITH_COMPLETION";
041:
042: public final static String QUANTIFIERS_OPTIONS_KEY = "QUANTIFIERS_OPTIONS_KEY";
043: public final static String QUANTIFIERS_NONE = "QUANTIFIERS_NONE";
044: public final static String QUANTIFIERS_NON_SPLITTING = "QUANTIFIERS_NON_SPLITTING";
045: public final static String QUANTIFIERS_NON_SPLITTING_WITH_PROGS = "QUANTIFIERS_NON_SPLITTING_WITH_PROGS";
046: public final static String QUANTIFIERS_INSTANTIATE = "QUANTIFIERS_INSTANTIATE";
047:
048: public final static int USER_TACLETS_NUM = 3;
049: private final static String USER_TACLETS_OPTIONS_KEY_BASE = "USER_TACLETS_OPTIONS_KEY";
050:
051: public static String USER_TACLETS_OPTIONS_KEY(int i) {
052: return USER_TACLETS_OPTIONS_KEY_BASE + i;
053: }
054:
055: public final static String USER_TACLETS_OFF = "USER_TACLETS_OFF";
056: public final static String USER_TACLETS_LOW = "USER_TACLETS_LOW";
057: public final static String USER_TACLETS_HIGH = "USER_TACLETS_HIGH";
058:
059: static Properties defaultMap = new Properties();
060:
061: static {
062: defaultMap
063: .setProperty(SPLITTING_OPTIONS_KEY, SPLITTING_DELAYED);
064: defaultMap.setProperty(LOOP_OPTIONS_KEY, LOOP_INVARIANT);
065: defaultMap.setProperty(METHOD_OPTIONS_KEY, METHOD_EXPAND);
066: defaultMap.setProperty(QUERY_OPTIONS_KEY, QUERY_NONE);
067: defaultMap.setProperty(NON_LIN_ARITH_OPTIONS_KEY,
068: NON_LIN_ARITH_NONE);
069: defaultMap.setProperty(QUANTIFIERS_OPTIONS_KEY,
070: QUANTIFIERS_NON_SPLITTING_WITH_PROGS);
071: for (int i = 1; i <= USER_TACLETS_NUM; ++i)
072: defaultMap.setProperty(USER_TACLETS_OPTIONS_KEY(i),
073: USER_TACLETS_OFF);
074: }
075:
076: public StrategyProperties() {
077: put(SPLITTING_OPTIONS_KEY, defaultMap
078: .get(SPLITTING_OPTIONS_KEY));
079: put(LOOP_OPTIONS_KEY, defaultMap.get(LOOP_OPTIONS_KEY));
080: put(METHOD_OPTIONS_KEY, defaultMap.get(METHOD_OPTIONS_KEY));
081: put(QUERY_OPTIONS_KEY, defaultMap.get(QUERY_OPTIONS_KEY));
082: put(NON_LIN_ARITH_OPTIONS_KEY, defaultMap
083: .get(NON_LIN_ARITH_OPTIONS_KEY));
084: put(QUANTIFIERS_OPTIONS_KEY, defaultMap
085: .get(QUANTIFIERS_OPTIONS_KEY));
086: for (int i = 1; i <= USER_TACLETS_NUM; ++i)
087: put(USER_TACLETS_OPTIONS_KEY(i), defaultMap
088: .get(USER_TACLETS_OPTIONS_KEY(i)));
089: }
090:
091: public static String getDefaultProperty(String key) {
092: return defaultMap.getProperty(key);
093: }
094:
095: public String getProperty(String key) {
096: String val = super .getProperty(key);
097: if (val != null)
098: return val;
099: return defaultMap.getProperty(key);
100: }
101:
102: public static StrategyProperties read(Properties p) {
103: StrategyProperties sp = new StrategyProperties();
104:
105: sp.put(SPLITTING_OPTIONS_KEY, readSingleOption(p,
106: SPLITTING_OPTIONS_KEY));
107: sp.put(LOOP_OPTIONS_KEY, readSingleOption(p, LOOP_OPTIONS_KEY));
108: sp.put(METHOD_OPTIONS_KEY, readSingleOption(p,
109: METHOD_OPTIONS_KEY));
110: sp.put(QUERY_OPTIONS_KEY,
111: readSingleOption(p, QUERY_OPTIONS_KEY));
112: sp.put(NON_LIN_ARITH_OPTIONS_KEY, readSingleOption(p,
113: NON_LIN_ARITH_OPTIONS_KEY));
114: sp.put(QUANTIFIERS_OPTIONS_KEY, readSingleOption(p,
115: QUANTIFIERS_OPTIONS_KEY));
116: for (int i = 1; i <= USER_TACLETS_NUM; ++i)
117: sp.put(USER_TACLETS_OPTIONS_KEY(i), readSingleOption(p,
118: USER_TACLETS_OPTIONS_KEY(i)));
119:
120: return sp;
121: }
122:
123: /**
124: * @param p
125: * @return
126: */
127: private static Object readSingleOption(Properties p, String key) {
128: Object o = (String) p.get("[StrategyProperty]" + key);
129: if (o == null)
130: o = defaultMap.get(key);
131: return o;
132: }
133:
134: public void write(Properties p) {
135: p.put("[StrategyProperty]" + SPLITTING_OPTIONS_KEY,
136: get(SPLITTING_OPTIONS_KEY));
137: p.put("[StrategyProperty]" + LOOP_OPTIONS_KEY,
138: get(LOOP_OPTIONS_KEY));
139: p.put("[StrategyProperty]" + METHOD_OPTIONS_KEY,
140: get(METHOD_OPTIONS_KEY));
141: p.put("[StrategyProperty]" + QUERY_OPTIONS_KEY,
142: get(QUERY_OPTIONS_KEY));
143: p.put("[StrategyProperty]" + NON_LIN_ARITH_OPTIONS_KEY,
144: get(NON_LIN_ARITH_OPTIONS_KEY));
145: p.put("[StrategyProperty]" + QUANTIFIERS_OPTIONS_KEY,
146: get(QUANTIFIERS_OPTIONS_KEY));
147: for (int i = 1; i <= USER_TACLETS_NUM; ++i)
148: p.put("[StrategyProperty]" + USER_TACLETS_OPTIONS_KEY(i),
149: get(USER_TACLETS_OPTIONS_KEY(i)));
150: }
151:
152: public Object clone() {
153: final Properties p = (Properties) super .clone();
154: final StrategyProperties sp = new StrategyProperties();
155: sp.putAll(p);
156: return sp;
157: }
158:
159: }
|