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

1 files changed, 55 insertions, 0 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
new file mode 100644
index 000000000..936ac8e73
--- /dev/null
+++ b/src/decision/decision_engine.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file decision_engine.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Decision engine
+ **
+ ** Decision engine
+ **/
+
+#include "decision/decision_engine.h"
+#include "decision/justification_heuristic.h"
+
+#include "expr/node.h"
+#include "util/options.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+DecisionEngine::DecisionEngine() : d_needSimplifiedPreITEAssertions() {
+  const Options* options = Options::current();
+  Trace("decision") << "Creating decision engine" << std::endl;
+  if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
+  if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
+    DecisionStrategy* ds = new decision::JustificationHeuristic(this);
+    enableStrategy(ds);
+  }
+}
+
+void DecisionEngine::enableStrategy(DecisionStrategy* ds)
+{
+  d_enabledStrategies.push_back(ds);
+  if( ds->needSimplifiedPreITEAssertions() )
+    d_needSimplifiedPreITEAssertions.push_back(ds);
+}
+
+void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
+{
+  d_assertions.reserve(assertions.size());
+  for(unsigned i = 0; i < assertions.size(); ++i)
+    d_assertions.push_back(assertions[i]);
+  for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
+    d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
+}
+
+}/* CVC4 namespace */