1 files changed, 150 insertions, 0 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
new file mode 100644
index 000000000..d4037acff
--- /dev/null
+++ b/src/decision/decision_engine.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file decision_engine.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 engine
+ **
+ ** Decision engine
+ **/
+
+#ifndef __CVC4__DECISION__DECISION_ENGINE_H
+#define __CVC4__DECISION__DECISION_ENGINE_H
+
+#include <vector>
+
+#include "decision/decision_strategy.h"
+
+#include "expr/node.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/sat_solver_types.h"
+#include "util/output.h"
+
+using namespace std;
+using namespace CVC4::prop;
+using namespace CVC4::decision;
+
+namespace CVC4 {
+
+class DecisionEngine {
+
+  vector <DecisionStrategy* > d_enabledStrategies;
+  vector <DecisionStrategy* > d_needSimplifiedPreITEAssertions;
+
+  vector <Node> d_assertions;
+
+  // PropEngine* d_propEngine;
+  CnfStream* d_cnfStream;
+  DPLLSatSolverInterface* d_satSolver;
+public:
+  // Necessary functions
+
+  /** Constructor, enables decision stragies based on options */
+  DecisionEngine();
+
+  /** Destructor, currently does nothing */
+  ~DecisionEngine() {
+    Trace("decision") << "Destroying decision engine" << std::endl;
+  }
+  
+  // void setPropEngine(PropEngine* pe) {
+  //   // setPropEngine should not be called more than once
+  //   Assert(d_propEngine == NULL);
+  //   Assert(pe != NULL);
+  //   d_propEngine = pe;
+  // }
+
+  void setSatSolver(DPLLSatSolverInterface* ss) {
+    // setPropEngine should not be called more than once
+    Assert(d_satSolver == NULL);
+    Assert(ss != NULL);
+    d_satSolver = ss;
+  }
+
+  void setCnfStream(CnfStream* cs) {
+    // setPropEngine should not be called more than once
+    Assert(d_cnfStream == NULL);
+    Assert(cs != NULL);
+    d_cnfStream = cs;
+  }
+
+
+  // Interface for External World to use our services
+
+  /** Gets the next decision based on strategies that are enabled */
+  SatLiteral getNext() {
+    SatLiteral ret = undefSatLiteral;
+    for(unsigned i = 0; i < d_enabledStrategies.size() 
+          and ret == undefSatLiteral; ++i) {
+      ret = d_enabledStrategies[i]->getNext();
+    }
+    return ret;
+  }
+
+  /**
+   * This is called by SmtEngine, at shutdown time, just before
+   * destruction.  It is important because there are destruction
+   * ordering issues between some parts of the system.  For now,
+   * there's nothing to do here in the DecisionEngine.
+   */
+  void shutdown() {
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+  }
+
+
+  // External World helping us help the Strategies
+
+  /** If one of the enabled strategies needs them  */
+  bool needSimplifiedPreITEAssertions() {
+    return d_needSimplifiedPreITEAssertions.size() > 0;
+  }
+  void informSimplifiedPreITEAssertions(const vector<Node> &assertions);
+
+
+  // Interface for Strategies to use stuff stored in Decision Engine
+  // (which was possibly requested by them on initialization)
+
+  /**
+   * Get the assertions. Strategies are notified when these are available. 
+   */
+  const vector<Node>& getAssertions() {
+    return d_assertions;
+  }
+
+
+  // Interface for Strategies to get information about External World
+
+  bool hasSatLiteral(Node n) {
+    return d_cnfStream->hasLiteral(n);
+  }
+  SatLiteral getSatLiteral(Node n) {
+    return d_cnfStream->getLiteral(n);
+  }
+  SatValue getSatValue(SatLiteral l) {
+    return d_satSolver->value(l);
+  }
+  Node getNode(SatLiteral l) {
+    return d_cnfStream->getNode(l);
+  }
+
+private:
+  /**
+   * Enable a particular decision strategy, also updating
+   * corresponding vector<DecisionStrategy*>-s is the engine
+   */
+  void enableStrategy(DecisionStrategy* ds);
+
+};/* DecisionEngine class */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__DECISION__DECISION_ENGINE_H */