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, 20 insertions, 6 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 97407a425..a41def821 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): cconway
+ ** Minor contributors (to current version): cconway, kshitij
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -27,6 +27,7 @@
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
 #include "context/context.h"
+#include "decision/decision_engine.h"
 #include "expr/command.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
@@ -223,6 +224,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_userContext(new UserContext()),
   d_exprManager(em),
   d_nodeManager(d_exprManager->getNodeManager()),
+  d_decisionEngine(NULL),
   d_theoryEngine(NULL),
   d_propEngine(NULL),
   d_definedFunctions(NULL),
@@ -262,8 +264,10 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
     d_theoryEngine->addTheory<theory::TheoryTraits<THEORY>::theory_class>(THEORY);
   CVC4_FOR_EACH_THEORY;
 
-  d_propEngine = new PropEngine(d_theoryEngine, d_context);
+  d_decisionEngine = new DecisionEngine();
+  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
   d_theoryEngine->setPropEngine(d_propEngine);
+  // d_decisionEngine->setPropEngine(d_propEngine);
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
@@ -309,6 +313,7 @@ void SmtEngine::shutdown() {
 
   d_propEngine->shutdown();
   d_theoryEngine->shutdown();
+  d_decisionEngine->shutdown();
 }
 
 SmtEngine::~SmtEngine() throw() {
@@ -917,9 +922,6 @@ void SmtEnginePrivate::simplifyAssertions()
       staticLearning();
     }
 
-    // Remove ITEs
-    removeITEs();
-
   } catch(TypeCheckingExceptionPrivate& tcep) {
     // Calls to this function should have already weeded out any
     // typechecking exceptions via (e.g.) ensureBoolean().  But a
@@ -1004,6 +1006,15 @@ void SmtEnginePrivate::processAssertions() {
   // Simplify the assertions
   simplifyAssertions();
 
+  if(d_smt.d_decisionEngine->needSimplifiedPreITEAssertions()) {
+    d_smt.d_decisionEngine->informSimplifiedPreITEAssertions(d_assertionsToCheck);
+  }
+
+  // Remove ITEs
+  removeITEs();                 // This may need to be in a try-catch
+                                // block. make regress is passing, so
+                                // skipping for now --K
+
   Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5149ed2e9..abd07538b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): cconway
+ ** Minor contributors (to current version): cconway, kshitij
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -50,6 +50,7 @@ typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
 
+class DecisionEngine;
 class TheoryEngine;
 
 class StatisticsRegistry;
@@ -109,6 +110,8 @@ class CVC4_PUBLIC SmtEngine {
   /** Our internal expression/node manager */
   NodeManager* d_nodeManager;
   /** The decision engine */
+  DecisionEngine* d_decisionEngine;
+  /** The theory engine */
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */
   prop::PropEngine* d_propEngine;