A dummy decision engine. Expected performance impact: none.

Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.

Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin

2 files changed, 19 insertions, 0 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index b6a306ee0..0bd02f308 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -80,6 +80,8 @@ Options::Options() :
   printWinner(false),
   simplificationMode(SIMPLIFICATION_MODE_BATCH),
   simplificationModeSetByUser(false),
+  decisionMode(DECISION_STRATEGY_INTERNAL),
+  decisionModeSetByUser(false),
   doStaticLearning(true),
   interactive(false),
   interactiveSetByUser(false),
diff --git a/src/util/options.h b/src/util/options.h
index c7fbcd896..6205c7543 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -126,6 +126,23 @@ struct CVC4_PUBLIC Options {
   /** Whether the user set the nonclausal simplification mode. */
   bool simplificationModeSetByUser;
 
+  /** Enumeration of decision strategies */
+  typedef enum {
+    /**
+     * Decision engine doesn't do anything. Use sat solver's internal
+     * heuristics
+     */
+    DECISION_STRATEGY_INTERNAL,
+    /**
+     * Use the justification heuristic
+     */
+    DECISION_STRATEGY_JUSTIFICATION
+  } DecisionMode;
+  /** When/whether to use any decision strategies */
+  DecisionMode decisionMode;
+  /** Whether the user set the decision strategy */
+  bool decisionModeSetByUser;
+
   /** Whether to perform the static learning pass. */
   bool doStaticLearning;