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, 16 insertions, 1 deletions

diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 6746b13cc..6ee583ec2 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -20,6 +20,7 @@
 #define __CVC4__DECISION__DECISION_STRATEGY_H
 
 #include "prop/sat_solver_types.h"
+#include "util/ite_removal.h"
 
 namespace CVC4 {
 
@@ -43,11 +44,25 @@ public:
 
   virtual prop::SatLiteral getNext(bool&) = 0;
   
-  virtual bool needSimplifiedPreITEAssertions() { return false; }
+  virtual bool needIteSkolemMap() { return false; }
   
   virtual void notifyAssertionsAvailable() { return; }
 };
 
+class ITEDecisionStrategy : public DecisionStrategy {
+public:
+  ITEDecisionStrategy(DecisionEngine* de, context::Context *c) :
+    DecisionStrategy(de, c) {
+  }
+
+
+  bool needIteSkolemMap() { return true; }
+
+  virtual void addAssertions(const std::vector<Node> &assertions,
+                             unsigned assertionsEnd,
+                             IteSkolemMap iteSkolemMap) = 0;
+};
+
 }/* decision namespace */
 }/* CVC4 namespace */