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

5 files changed, 36 insertions, 8 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index abe22cb48..848c63a18 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): barrett, taking, cconway
+ ** Minor contributors (to current version): barrett, taking, 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
@@ -22,6 +22,7 @@
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 
+#include "decision/decision_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
 #include "util/Assert.h"
@@ -61,9 +62,10 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te, Context* context) :
+PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) :
   d_inCheckSat(false),
   d_theoryEngine(te),
+  d_decisionEngine(de),
   d_context(context),
   d_satSolver(NULL),
   d_cnfStream(NULL),
@@ -77,7 +79,10 @@ PropEngine::PropEngine(TheoryEngine* te, Context* context) :
   theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar, Options::current()->threads > 1);
 
-  d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_context, d_cnfStream));
+  d_satSolver->initialize(d_context, new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream));
+
+  d_decisionEngine->setSatSolver(d_satSolver);
+  d_decisionEngine->setCnfStream(d_cnfStream);
 }
 
 PropEngine::~PropEngine() {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 93c35bbf3..3d114db3a 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: taking, dejan
- ** Minor contributors (to current version): cconway, barrett
+ ** Minor contributors (to current version): cconway, barrett, 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
@@ -31,6 +31,7 @@
 
 namespace CVC4 {
 
+class DecisionEngine;
 class TheoryEngine;
 
 namespace prop {
@@ -127,6 +128,9 @@ class PropEngine {
   /** The theory engine we will be using */
   TheoryEngine *d_theoryEngine;
 
+  /** The decision engine we will be using */
+  DecisionEngine *d_decisionEngine;
+
   /** The context */
   context::Context* d_context;
 
@@ -153,7 +157,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*, context::Context*);
+  PropEngine(TheoryEngine*, DecisionEngine*, context::Context*);
 
   /**
    * Destructor.
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 406782468..0da4d7a6a 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -26,6 +26,9 @@
 
 #include "cvc4_private.h"
 
+#include <string>
+#include <sstream>
+
 namespace CVC4 {
 namespace prop {
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 43f7f75af..f024dccf3 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: dejan, taking, mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): 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
@@ -24,6 +24,8 @@
 #include "theory/theory_engine.h"
 #include "theory/rewriter.h"
 #include "expr/expr_stream.h"
+#include "decision/decision_engine.h"
+
 
 namespace CVC4 {
 namespace prop {
@@ -73,7 +75,14 @@ void TheoryProxy::enqueueTheoryLiteral(const SatLiteral& l) {
 
 SatLiteral TheoryProxy::getNextDecisionRequest() {
   TNode n = d_theoryEngine->getNextDecisionRequest();
-  return n.isNull() ? undefSatLiteral : d_cnfStream->getLiteral(n);
+  if(not n.isNull())
+    return d_cnfStream->getLiteral(n);
+  
+  // If theory doesn't give us a deicsion ask the decision engine. It
+  // may return in undefSatLiteral in which case the sat solver figure
+  // it out something
+  Assert(d_decisionEngine != NULL);
+  return d_decisionEngine->getNext();
 }
 
 bool TheoryProxy::theoryNeedCheck() const {
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 8b585710f..ceb328d90 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: taking, cconway, dejan
- ** Minor contributors (to current version): barrett
+ ** Minor contributors (to current version): barrett, 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
@@ -33,6 +33,7 @@
 
 namespace CVC4 {
 
+class DecisionEngine;
 class TheoryEngine;
 
 namespace prop {
@@ -51,6 +52,9 @@ class TheoryProxy {
   /** The CNF engine we are using */
   CnfStream* d_cnfStream;
 
+  /** The decision engine we are using */
+  DecisionEngine* d_decisionEngine;
+
   /** The theory engine we are using */
   TheoryEngine* d_theoryEngine;
 
@@ -66,6 +70,7 @@ class TheoryProxy {
 public:
   TheoryProxy(PropEngine* propEngine,
               TheoryEngine* theoryEngine,
+              DecisionEngine* decisionEngine,
               context::Context* context,
               CnfStream* cnfStream);
 
@@ -113,10 +118,12 @@ public:
 
 inline TheoryProxy::TheoryProxy(PropEngine* propEngine,
                                 TheoryEngine* theoryEngine,
+                                DecisionEngine* decisionEngine,
                                 context::Context* context,
                                 CnfStream* cnfStream) :
   d_propEngine(propEngine),
   d_cnfStream(cnfStream),
+  d_decisionEngine(decisionEngine),
   d_theoryEngine(theoryEngine),
   d_context(context)
 {}