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, 34 insertions, 9 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 3ec6aaf2a..ea516aa54 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -27,6 +27,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat_solver_types.h"
+#include "util/ite_removal.h"
 #include "util/output.h"
 
 using namespace std;
@@ -38,7 +39,7 @@ namespace CVC4 {
 class DecisionEngine {
 
   vector <DecisionStrategy* > d_enabledStrategies;
-  vector <DecisionStrategy* > d_needSimplifiedPreITEAssertions;
+  vector <ITEDecisionStrategy* > d_needIteSkolemMap;
 
   vector <Node> d_assertions;
 
@@ -47,13 +48,16 @@ class DecisionEngine {
   DPLLSatSolverInterface* d_satSolver;
 
   context::Context* d_satContext;
+  context::Context* d_userContext;
   SatValue d_result;
 
+  // Disable creating decision engine without required parameters
+  DecisionEngine() {}
 public:
   // Necessary functions
 
   /** Constructor, enables decision stragies based on options */
-  DecisionEngine(context::Context *c);
+  DecisionEngine(context::Context *sc, context::Context *uc);
 
   /** Destructor, currently does nothing */
   ~DecisionEngine() {
@@ -88,6 +92,11 @@ public:
 
   /** Gets the next decision based on strategies that are enabled */
   SatLiteral getNext(bool &stopSearch) {
+    Assert(d_cnfStream != NULL,
+           "Forgot to set cnfStream for decision engine?");
+    Assert(d_satSolver != NULL,
+           "Forgot to set satSolver for decision engine?");
+
     SatLiteral ret = undefSatLiteral;
     for(unsigned i = 0; 
         i < d_enabledStrategies.size() 
@@ -113,7 +122,7 @@ public:
     case SAT_VALUE_TRUE: return Result(Result::SAT);
     case SAT_VALUE_FALSE: return Result(Result::UNSAT);
     case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    default: Assert(false);
+    default: Assert(false, "d_result is garbage");
     }
     return Result();
   }
@@ -137,11 +146,24 @@ public:
   // 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);
+  /* bool needIteSkolemMap() { */
+  /*   return d_needIteSkolemMap.size() > 0; */
+  /* } */
 
+  /* add a set of assertions */
+  void addAssertions(const vector<Node> &assertions);
+
+  /**
+   * add a set of assertions, while providing a mapping between skolem
+   * variables and corresponding assertions. It is assumed that all
+   * assertions after assertionEnd were generated by ite
+   * removal. Hence, iteSkolemMap maps into only these.
+   */
+  void addAssertions(const vector<Node> &assertions,
+                     int assertionsEnd,
+                     IteSkolemMap iteSkolemMap);
+
+  /* add a single assertion */
   void addAssertion(Node n);
 
   // Interface for Strategies to use stuff stored in Decision Engine
@@ -157,15 +179,18 @@ public:
 
   // Interface for Strategies to get information about External World
 
-  bool hasSatLiteral(Node n) {
+  bool hasSatLiteral(TNode n) {
     return d_cnfStream->hasLiteral(n);
   }
-  SatLiteral getSatLiteral(Node n) {
+  SatLiteral getSatLiteral(TNode n) {
     return d_cnfStream->getLiteral(n);
   }
   SatValue getSatValue(SatLiteral l) {
     return d_satSolver->value(l);
   }
+  SatValue getSatValue(TNode n) {
+    return getSatValue(getSatLiteral(n));
+  }
   Node getNode(SatLiteral l) {
     return d_cnfStream->getNode(l);
   }