#210, add TreeAutomizerSettings

trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TaMinimization.java

@@ -0,0 +1,11 @@
+package de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer;
+
+/**
+ * Types of minimizations that can be used by TreeAutomizer.
+ *
+ * @author Alexander Nutz ([email protected])
+ *
+ */
+public enum TaMinimization {
+	NONE, NAIVE, HOPCROFT;
+}

trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/TreeAutomizerSettings.java

@@ -0,0 +1,34 @@
+package de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer;
+
+public class TreeAutomizerSettings {
+
+	/**
+	 * Use the class Difference or LazyDifference?
+	 * Difference: naive difference algorithm
+	 * LazyDifference: smart totalization of right hand side automaton, take only reachable states into consideration.
+	 */
+	public static final boolean USE_NAIVE_DIFFERENCE = false;
+
+	/**
+	 * Introduce edges to the interpolant automaton during or before the difference operation (in refineAbstraction)?
+	 */
+	public static final boolean GENERALIZE_INTERPOLANT_AUTOMATON_UPFRONT = true;
+
+	/**
+	 *
+	 * If this is true and GENERALIZE_INTERPOLANT_AUTOMATON_UPFRONT, no generalization of the interpolant automaton is
+	 * done (and we thus might not terminate, even with good interpolants).
+	 */
+	public static final boolean USE_RAW_INTERPOLANT_AUTOMATON = false;
+
+	/**
+	 * Upper bound for iterations of CEGAR loop, choose negative value for no bound.
+	 */
+	public static final int ITERATIONS_BOUND = -1;
+
+	/**
+	 * Apply minimization to current abstraction at the end of every CEGAR iteration?
+	 */
+	public static final TaMinimization MINIMIZATION = TaMinimization.HOPCROFT;
+
+}

trunk/source/TreeAutomizer/src/de/uni_freiburg/informatik/ultimate/plugins/generator/treeautomizer/graph/TreeAutomizerCEGAR.java

@@ -70,6 +70,7 @@
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.preferences.TAPreferences;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.PredicateUnifier;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer.Activator;
+import de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer.TreeAutomizerSettings;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer.parsing.HornAnnot;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.treeautomizer.preferences.TreeAutomizerPreferenceInitializer;
 
@@ -165,10 +166,10 @@ public IResult iterate() throws AutomataLibraryException {
 
 		mLogger.debug("Abstraction tree automaton before iteration #" + (mIteration + 1));
 		mLogger.debug(mAbstraction);
-		final int mITERATIONS = 10;
 
 		while (mServices.getProgressMonitorService().continueProcessing()
-				&& (mITERATIONS == -1 || mIteration < mITERATIONS)) {
+				&& (TreeAutomizerSettings.ITERATIONS_BOUND <= -1
+					|| mIteration < TreeAutomizerSettings.ITERATIONS_BOUND)) {
 			mLogger.debug("Iteration #" + (mIteration + 1));
 			final TreeRun<HornClause, IPredicate> counterExample = isAbstractionCorrect();
 			if (counterExample == null) {