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.gui;
011:
012: import java.util.Iterator;
013: import java.util.LinkedList;
014: import java.util.Properties;
015:
016: import de.uka.ilkd.key.gui.configuration.Settings;
017: import de.uka.ilkd.key.gui.configuration.SettingsListener;
018: import de.uka.ilkd.key.unittest.ModelGenerator;
019:
020: /** This class encapsulates the information which
021: * decision procedure should be used.
022: */
023: public class DecisionProcedureSettings implements Settings {
024:
025: private static final String DECISION_PROCEDURE = "[DecisionProcedure]";
026: private static final String DECISION_PROCEDURE_FOR_TEST = "[DecisionProcedureForTest]";
027: private static final String SMT_BENCHMARK_ARCHIVING = "[DecisionProcedure]SmtBenchmarkArchiving";
028: private static final String SMT_ZIP_PROBLEM_DIR = "[DecisionProcedure]SmtZipProblemDir";
029: private static final String SMT_USE_QUANTIFIERS = "[DecisionProcedure]SmtUseQuantifiers";
030: public static final String SIMPLIFY = "SIMPLIFY";
031: public static final String ICS = "ICS";
032: public static final String CVCLite = "CVCLite";
033: public static final String CVC3 = "CVC3";
034: public static final String SVC = "SVC";
035: public static final String YICES = "YICES";
036: public static final String SMT = "Dummy SMT Translation";
037: // only used for test generation
038: public static final String COGENT = "Cogent";
039:
040: private String decision_procedure = SIMPLIFY;
041: private String decision_procedure_for_test = COGENT;
042: private boolean smt_benchmark_archiving = false;
043: private boolean smt_zip_problem_dir = false;
044: private boolean smt_use_quantifiers = true;
045:
046: private LinkedList listenerList = new LinkedList();
047:
048: // getter
049: public String getDecisionProcedure() {
050: return decision_procedure;
051: }
052:
053: // setter
054: public void setDecisionProcedure(String s) {
055: if (!s.equals(decision_procedure)) {
056: decision_procedure = s;
057: fireSettingsChanged();
058: }
059: }
060:
061: // getter
062: public String getDecisionProcedureForTest() {
063: return decision_procedure_for_test;
064: }
065:
066: // setter
067: public void setDecisionProcedureForTest(String s) {
068: if (!s.equals(decision_procedure_for_test)) {
069: decision_procedure_for_test = s;
070: fireSettingsChanged();
071: }
072: }
073:
074: /** Enables archiving of SMT benchmarks (which were translated from sequents) during execution
075: * of SMT compliant external decision procedures
076: * @param b if set to <tt>true</tt>, the benchmarks will be archived
077: */
078: public void setDoBenchmarkArchiving(boolean b) {
079: smt_benchmark_archiving = b;
080: fireSettingsChanged();
081: }
082:
083: /** Enables zipping of archived problem directories during SMT benchmark archiving
084: * @param b if set to <tt>true</tt>, the problem dirs will be zipped
085: */
086: public void setDoZipProblemDir(boolean b) {
087: smt_zip_problem_dir = b;
088: fireSettingsChanged();
089: }
090:
091: /** Enables translation of quantified terms during SMT translation
092: * @param b if set to <tt>true</tt>, quantifiers will be translated
093: */
094: public void setUseQuantifier(boolean b) {
095: smt_use_quantifiers = b;
096: fireSettingsChanged();
097: }
098:
099: public boolean useSimplifyForTest() {
100: return decision_procedure_for_test.equals(SIMPLIFY);
101: }
102:
103: public boolean useCogentForTest() {
104: return decision_procedure_for_test.equals(COGENT);
105: }
106:
107: public boolean useSimplify() {
108: return decision_procedure.equals(SIMPLIFY);
109: }
110:
111: public boolean useICS() {
112: return decision_procedure.equals(ICS);
113: }
114:
115: public boolean useCVCLite() {
116: return decision_procedure.equals(CVCLite);
117: }
118:
119: public boolean useCVC3() {
120: return decision_procedure.equals(CVC3);
121: }
122:
123: public boolean useSVC() {
124: return decision_procedure.equals(SVC);
125: }
126:
127: public boolean useYices() {
128: return decision_procedure.equals(YICES);
129: }
130:
131: public boolean useSMT_Translation() {
132: return decision_procedure.equals(SMT);
133: }
134:
135: /** @return <tt>true</tt> if SMT benchmark archiving is enabled */
136: public boolean doBenchmarkArchiving() {
137: return smt_benchmark_archiving;
138: }
139:
140: /** @return <tt>true</tt> if problem directories will be zipped during SMT benchmark archiving */
141: public boolean doZipProblemDir() {
142: return smt_zip_problem_dir;
143: }
144:
145: /** @return <tt>true</tt> if quantifiers will be translated in SMT translation */
146: public boolean useQuantifiers() {
147: return smt_use_quantifiers;
148: }
149:
150: /** gets a Properties object and has to perform the necessary
151: * steps in order to change this object in a way that it
152: * represents the stored settings
153: */
154: public void readSettings(Properties props) {
155: String dec_proc_string = props.getProperty(DECISION_PROCEDURE);
156:
157: if (dec_proc_string == null || dec_proc_string.equals(SIMPLIFY))
158: decision_procedure = SIMPLIFY;
159: else if (dec_proc_string.equals(ICS))
160: decision_procedure = ICS;
161: else if (dec_proc_string.equals(CVCLite))
162: decision_procedure = CVCLite;
163: else if (dec_proc_string.equals(CVC3))
164: decision_procedure = CVC3;
165: else if (dec_proc_string.equals(SVC))
166: decision_procedure = SVC;
167: else if (dec_proc_string.equals(YICES))
168: decision_procedure = YICES;
169: else if (dec_proc_string.equals(SMT))
170: decision_procedure = SMT;
171: else
172: decision_procedure = SIMPLIFY;
173:
174: String dec_proc_for_test_string = props
175: .getProperty(DECISION_PROCEDURE_FOR_TEST);
176: if (dec_proc_for_test_string == null
177: || dec_proc_for_test_string.equals(SIMPLIFY))
178: decision_procedure_for_test = SIMPLIFY;
179: else if (dec_proc_for_test_string.equals(COGENT))
180: decision_procedure_for_test = COGENT;
181: else
182: decision_procedure_for_test = SIMPLIFY;
183:
184: ModelGenerator.decProdForTestGen = useSimplifyForTest() ? ModelGenerator.SIMPLIFY
185: : ModelGenerator.COGENT;
186:
187: String val = props.getProperty(SMT_BENCHMARK_ARCHIVING);
188: if (val != null)
189: smt_benchmark_archiving = Boolean.valueOf(val)
190: .booleanValue();
191: else
192: smt_benchmark_archiving = false;
193:
194: val = props.getProperty(SMT_ZIP_PROBLEM_DIR);
195: if (val != null)
196: smt_zip_problem_dir = Boolean.valueOf(val).booleanValue();
197: else
198: smt_zip_problem_dir = false;
199:
200: val = props.getProperty(SMT_USE_QUANTIFIERS);
201: if (val != null)
202: smt_use_quantifiers = Boolean.valueOf(val).booleanValue();
203: else
204: smt_use_quantifiers = true;
205: }
206:
207: /** implements the method required by the Settings interface. The
208: * settings are written to the given Properties object. Only entries of the form
209: * <key> = <value> (,<value>)* are allowed.
210: * @param props the Properties object where to write the settings as (key, value) pair
211: */
212: public void writeSettings(Properties props) {
213: props.setProperty(DECISION_PROCEDURE, getDecisionProcedure());
214: props.setProperty(DECISION_PROCEDURE_FOR_TEST,
215: getDecisionProcedureForTest());
216: props.setProperty(SMT_BENCHMARK_ARCHIVING, ""
217: + smt_benchmark_archiving);
218: props
219: .setProperty(SMT_ZIP_PROBLEM_DIR, ""
220: + smt_zip_problem_dir);
221: props
222: .setProperty(SMT_USE_QUANTIFIERS, ""
223: + smt_use_quantifiers);
224: }
225:
226: /** sends the message that the state of this setting has been
227: * changed to its registered listeners (not thread-safe)
228: */
229: protected void fireSettingsChanged() {
230: Iterator it = listenerList.iterator();
231: while (it.hasNext()) {
232: ((SettingsListener) it.next())
233: .settingsChanged(new GUIEvent(this ));
234: }
235: }
236:
237: /** adds a listener to the settings object
238: * @param l the listener
239: */
240: public void addSettingsListener(SettingsListener l) {
241: listenerList.add(l);
242: }
243:
244: }
|