Merge from decision branch (ITE support)

Major changes from last merge
* ITEs supported
* Don't share theory lemmas to DE, only assertions

Should probably be noted that 'make regress' doesn't quite
pass with --decision=justification. Throws off search in couple
of arith benchmarks.

No serious performance changes expected. Keep an eye.

1 files changed, 39 insertions, 18 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 7c8718370..1d4f2fd42 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -26,13 +26,15 @@ using namespace std;
 
 namespace CVC4 {
 
-DecisionEngine::DecisionEngine(context::Context *c) :
+  DecisionEngine::DecisionEngine(context::Context *sc,
+                                 context::Context *uc) :
   d_enabledStrategies(),
-  d_needSimplifiedPreITEAssertions(),
+  d_needIteSkolemMap(),
   d_assertions(),
   d_cnfStream(NULL),
   d_satSolver(NULL),
-  d_satContext(c),
+  d_satContext(sc),
+  d_userContext(uc),
   d_result(SAT_VALUE_UNKNOWN)
 {
   const Options* options = Options::current();
@@ -42,37 +44,56 @@ DecisionEngine::DecisionEngine(context::Context *c) :
 
   if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { }
   if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) {
-    DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext);
+    ITEDecisionStrategy* ds = 
+      new decision::JustificationHeuristic(this, d_satContext);
     enableStrategy(ds);
+    d_needIteSkolemMap.push_back(ds);
   }
 }
 
 void DecisionEngine::enableStrategy(DecisionStrategy* ds)
 {
   d_enabledStrategies.push_back(ds);
-  if( ds->needSimplifiedPreITEAssertions() )
-    d_needSimplifiedPreITEAssertions.push_back(ds);
 }
 
-void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions)
+
+void DecisionEngine::addAssertions(const vector<Node> &assertions)
+{
+  Assert(false);  // doing this so that we revisit what to do
+                  // here. Currently not being used.
+
+  // d_result = SAT_VALUE_UNKNOWN;
+  // d_assertions.reserve(assertions.size());
+  // for(unsigned i = 0; i < assertions.size(); ++i)
+  //   d_assertions.push_back(assertions[i]); 
+}
+
+void DecisionEngine::addAssertions
+  (const vector<Node> &assertions,
+   int assertionsEnd,
+   IteSkolemMap iteSkolemMap) 
 {
+  // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
+  
   d_assertions.reserve(assertions.size());
   for(unsigned i = 0; i < assertions.size(); ++i)
     d_assertions.push_back(assertions[i]);
-  for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
-    d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
+  
+  for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
+    d_needIteSkolemMap[i]->
+      addAssertions(assertions, assertionsEnd, iteSkolemMap);
 }
 
-void DecisionEngine::addAssertion(Node n)
-{
-  d_result = SAT_VALUE_UNKNOWN;
-  if(needSimplifiedPreITEAssertions()) {
-    d_assertions.push_back(n);
-  }
-  for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i)
-    d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable();
-}
+// void DecisionEngine::addAssertion(Node n)
+// {
+//   d_result = SAT_VALUE_UNKNOWN;
+//   if(needIteSkolemMap()) {
+//     d_assertions.push_back(n);
+//   }
+//   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
+//     d_needIteSkolemMap[i]->notifyAssertionsAvailable();
+// }
   
 
 }/* CVC4 namespace */