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, 8 insertions, 1 deletions

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)
 {}