* Add support for --decision=justification + incremental (bug 437)

 - Fix a destruction order issue this triggered in DE

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 22c70eb6d3ebde67b3557e9ac67d0021a6998a1c..9e8add7520168020dc92a3f85bdb183f1b35ced6 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -33,7 +33,7 @@ DecisionEngine::DecisionEngine(context::Context *sc,
   d_enabledStrategies(),
   d_needIteSkolemMap(),
   d_relevancyStrategy(NULL),
-  d_assertions(),
+  d_assertions(uc),
   d_cnfStream(NULL),
   d_satSolver(NULL),
   d_satContext(sc),
@@ -50,18 +50,6 @@ void DecisionEngine::init()
   d_engineState = 1;
 
   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
-  if(options::incrementalSolving()) {
-    if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) {
-      if(options::decisionMode.wasSetByUser()) {
-        Warning() << "Ignorning decision option since using incremental mode (currently not supported together)"
-                  << std::endl;
-      } else {
-        Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)"
-                 << std::endl;
-      }
-    }
-    return;
-  }
   Trace("decision-init") << " * options->decisionMode: " 
                          << options::decisionMode() << std:: endl;
   Trace("decision-init") << " * options->decisionStopOnly: "
@@ -70,11 +58,16 @@ void DecisionEngine::init()
   if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
   if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
     ITEDecisionStrategy* ds = 
-      new decision::JustificationHeuristic(this, d_satContext);
+      new decision::JustificationHeuristic(this, d_userContext, d_satContext);
     enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
   }
   if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) {
+    if(options::incrementalSolving()) {
+      Warning() << "Relevancy decision heuristic and incremental not supported together"
+                << std::endl;
+      return; // Currently not supported with incremental
+    }
     RelevancyStrategy* ds = 
       new decision::Relevancy(this, d_satContext);
     enableStrategy(ds);
@@ -137,7 +130,7 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions,
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
   
-  d_assertions.reserve(assertions.size());
+  // d_assertions.reserve(assertions.size());
   for(unsigned i = 0; i < assertions.size(); ++i)
     d_assertions.push_back(assertions[i]);
   

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 4d354af2a8335d193a43b3be356a40c76a738674..ea16cec16443307fbac838bb9c21f86fed72a194 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -42,7 +42,8 @@ class DecisionEngine {
   vector <ITEDecisionStrategy* > d_needIteSkolemMap;
   RelevancyStrategy* d_relevancyStrategy;
 
-  vector <Node> d_assertions;
+  typedef context::CDList<Node> AssertionsList;
+  AssertionsList d_assertions;
 
   // PropEngine* d_propEngine;
   CnfStream* d_cnfStream;
@@ -55,7 +56,7 @@ class DecisionEngine {
   context::CDO<SatValue> d_result;
 
   // Disable creating decision engine without required parameters
-  DecisionEngine() : d_result(NULL) {}
+  DecisionEngine();
 
   // init/shutdown state
   unsigned d_engineState;    // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
@@ -68,8 +69,6 @@ public:
   /** Destructor, currently does nothing */
   ~DecisionEngine() {
     Trace("decision") << "Destroying decision engine" << std::endl;
-    for(unsigned i = 0; i < d_enabledStrategies.size(); ++i)
-      delete d_enabledStrategies[i];
   }
   
   // void setPropEngine(PropEngine* pe) {
@@ -99,14 +98,15 @@ public:
   /**
    * 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.
+   * ordering issues between some parts of the system.
    */
   void shutdown() {
     Assert(d_engineState == 1);
     d_engineState = 2;
 
     Trace("decision") << "Shutting down decision engine" << std::endl;
+    for(unsigned i = 0; i < d_enabledStrategies.size(); ++i)
+      delete d_enabledStrategies[i];
   }
 
   // Interface for External World to use our services
@@ -191,7 +191,7 @@ public:
   /**
    * Get the assertions. Strategies are notified when these are available. 
    */
-  const vector<Node>& getAssertions() {
+  AssertionsList& getAssertions() {
     return d_assertions;
   }
 

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index ba8ab91b7b299707b7feeb64d4195834b683caa3..494da72bf3e38b19c20cfb09ab097be954a54e73 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -73,7 +73,7 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l)
   for(unsigned i=0; i<n.getNumChildren(); ++i) {
     SkolemMap::iterator it2 = d_iteAssertions.find(n[i]);
     if(it2 != d_iteAssertions.end()) {
-      l.push_back(make_pair(n[i], it2->second));
+      l.push_back(make_pair(n[i], (*it2).second));
       Assert(n[i].getNumChildren() == 0);
     }
     computeITEs(n[i], l);
@@ -98,6 +98,15 @@ bool JustificationHeuristic::findSplitterRec(TNode node,
                                              SatValue desiredVal,
                                              SatLiteral* litDecision)
 {
+  /**
+   * Main idea
+   *
+   * Given a boolean formula "node", the goal is to try to make it
+   * evaluate to "desiredVal" (true/false). for instance if "node" is a AND
+   * formula we want to make it evaluate to true, we'd like one of the
+   * children to be true. this is done recursively.
+   */
+
   Trace("jh-findSplitterRec") 
     << "findSplitterRec(" << node << ", " 
     << desiredVal << ", .. )" << std::endl; 

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a3b05b1bb29d4c6bfddf553237b046200e102cd4..adccc0d55cec60bf35ab89403430980b1c91acd1 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -27,6 +27,8 @@
 #include "decision_strategy.h"
 
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
+#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "prop/sat_solver_types.h"
 
@@ -44,7 +46,7 @@ public:
 class JustificationHeuristic : public ITEDecisionStrategy {
   typedef std::vector<pair<TNode,TNode> > IteList;
   typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
-  typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
+  typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
 
   // being 'justified' is monotonic with respect to decisions
   typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
@@ -59,7 +61,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * A copy of the assertions that need to be justified
    * directly. Doesn't have ones introduced during during ITE-removal.
    */
-  std::vector<TNode> d_assertions;   
+  context::CDList<TNode> d_assertions;
   //TNode is fine since decisionEngine has them too
 
   /** map from ite-rewrite skolem to a boolean-ite assertion */
@@ -77,13 +79,17 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    */
   hash_set<TNode,TNodeHashFunction> d_visited;
 public:
-  JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c):
+  JustificationHeuristic(CVC4::DecisionEngine* de,
+                         context::Context *uc,
+                         context::Context *c):
     ITEDecisionStrategy(de, c),
     d_justified(c),
     d_prvsIndex(c, 0),
     d_helfulness("decision::jh::helpfulness", 0),
     d_giveup("decision::jh::giveup", 0),
-    d_timestat("decision::jh::time") {
+    d_timestat("decision::jh::time"),
+    d_assertions(uc),
+    d_iteAssertions(uc) {
     StatisticsRegistry::registerStat(&d_helfulness);
     StatisticsRegistry::registerStat(&d_giveup);
     StatisticsRegistry::registerStat(&d_timestat);
@@ -91,6 +97,7 @@ public:
   }
   ~JustificationHeuristic() {
     StatisticsRegistry::unregisterStat(&d_helfulness);
+    StatisticsRegistry::unregisterStat(&d_giveup);
     StatisticsRegistry::unregisterStat(&d_timestat);
   }
   prop::SatLiteral getNext(bool &stopSearch) {