Merging the unate-propagator branch into the trunk. This is a big update so expect a little turbulence. This commit will not compile. There will be a second commit that fixes this in a moment. I am delaying a change to avoid svn whining about a conflict.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index aff60f651..c76923bee 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -30,6 +30,7 @@
 #include "theory/arith/tableau.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/partial_model.h"
+#include "theory/arith/arith_propagator.h"
 
 #include "util/stats.h"
 
@@ -96,6 +97,7 @@ private:
    */
   ArithRewriter d_rewriter;
 
+  ArithUnatePropagator d_propagator;
 
 public:
   TheoryArith(context::Context* c, OutputChannel& out);
@@ -115,8 +117,8 @@ public:
   void registerTerm(TNode n);
 
   void check(Effort e);
-  void propagate(Effort e) { Unimplemented(); }
-  void explain(TNode n, Effort e) { Unimplemented(); }
+  void propagate(Effort e);
+  void explain(TNode n, Effort e);
 
   void shutdown(){ }
 
@@ -242,6 +244,7 @@ private:
     IntStat d_statAssertLowerConflicts, d_statUpdateConflicts;
 
     Statistics();
+    ~Statistics();
   };
 
   Statistics d_statistics;