This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:

- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager

2 files changed, 66 insertions, 0 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index d0c2b9783..13a151ffc 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -23,5 +23,6 @@ libcontext_la_SOURCES = \
 	cdcirclist.h \
 	cdcirclist_forward.h \
 	cdvector.h \
+	cdmaybe.h \
 	stacking_map.h \
 	stacking_vector.h
diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h
new file mode 100644
index 000000000..3c95ab126
--- /dev/null
+++ b/src/context/cdmaybe.h
@@ -0,0 +1,65 @@
+/**
+ * This implements a CDMaybe.
+ * This has either been set in the context or it has not.
+ * T must have a default constructor and support assignment.
+ */
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "context/cdo.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace context {
+
+class CDRaised {
+private:
+  context::CDO<bool> d_flag;
+
+public:
+ CDRaised(context::Context* c)
+ : d_flag(c, false)
+ {}
+
+
+  bool isRaised() const {
+    return d_flag.get();
+  }
+
+  void raise(){
+    Assert(!isRaised());
+    d_flag.set(true);
+  }
+
+}; /* class CDRaised */
+
+template <class T>
+class CDMaybe {
+private:
+  typedef std::pair<bool, T> BoolTPair;
+  context::CDO<BoolTPair> d_data;
+
+public:
+  CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T()))
+  {}
+
+  bool isSet() const {
+    return d_data.get().first;
+  }
+
+  void set(const T& d){
+    Assert(!isSet());
+    d_data.set(std::make_pair(true, d));
+  }
+
+  const T& get() const{
+    Assert(isSet());
+    return d_data.get().second;
+  }
+}; /* class CDMaybe<T> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+