This commit:

* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
  assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
  currently get around by not destucting stuff in driver

2 files changed, 30 insertions, 15 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index b38b3c1e0..937099e38 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -27,7 +27,7 @@ using namespace std;
 
 namespace CVC4 {
 
-  DecisionEngine::DecisionEngine(context::Context *sc,
+DecisionEngine::DecisionEngine(context::Context *sc,
                                  context::Context *uc) :
   d_enabledStrategies(),
   d_needIteSkolemMap(),
@@ -37,11 +37,18 @@ namespace CVC4 {
   d_satSolver(NULL),
   d_satContext(sc),
   d_userContext(uc),
-  d_result(sc, SAT_VALUE_UNKNOWN)
+  d_result(sc, SAT_VALUE_UNKNOWN),
+  d_engineState(0)
 {
-  const Options* options = Options::current();
   Trace("decision") << "Creating decision engine" << std::endl;
+}
+
+void DecisionEngine::init()
+{
+  Assert(d_engineState == 0);
+  d_engineState = 1;
 
+  const Options* options = Options::current();
   if(options->incrementalSolving) return;
 
   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
@@ -60,6 +67,7 @@ namespace CVC4 {
   }
 }
 
+
 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
 {
   d_enabledStrategies.push_back(ds);
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index e19307170..6b878ecd0 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -56,10 +56,13 @@ class DecisionEngine {
 
   // Disable creating decision engine without required parameters
   DecisionEngine() : d_result(NULL) {}
+
+  // init/shutdown state
+  unsigned d_engineState;    // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
 public:
   // Necessary functions
 
-  /** Constructor, enables decision stragies based on options */
+  /** Constructor */
   DecisionEngine(context::Context *sc, context::Context *uc);
 
   /** Destructor, currently does nothing */
@@ -90,6 +93,21 @@ public:
     d_cnfStream = cs;
   }
 
+  /* enables decision stragies based on options */
+  void init();
+
+  /**
+   * 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() {
+    Assert(d_engineState == 1);
+    d_engineState = 2;
+
+    Trace("decision") << "Shutting down decision engine" << std::endl;
+  }
 
   // Interface for External World to use our services
 
@@ -144,17 +162,6 @@ public:
     d_result = val;
   }
 
-  /**
-   * 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  */