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, 50 insertions, 0 deletions

diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
new file mode 100644
index 000000000..abcbbaace
--- /dev/null
+++ b/src/decision/decision_strategy.h
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file decision_strategy.h
+ ** \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 stategy
+ **
+ ** Decision strategy
+ **/
+
+#ifndef __CVC4__DECISION__DECISION_STRATEGY_H
+#define __CVC4__DECISION__DECISION_STRATEGY_H
+
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+
+class DecisionEngine;
+
+namespace decision {
+
+class DecisionStrategy {
+protected:
+   DecisionEngine* d_decisionEngine;
+public:
+  DecisionStrategy(DecisionEngine* de) :
+    d_decisionEngine(de) {
+  }
+
+  virtual ~DecisionStrategy() { }
+
+  virtual prop::SatLiteral getNext() = 0;
+  
+  virtual bool needSimplifiedPreITEAssertions() { return false; }
+  
+  virtual void notifyAssertionsAvailable() { return; }
+};
+
+}/* decision namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DECISION__DECISION_STRATEGY_H */