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

1 files changed, 2 insertions, 8 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 4a5c398bd..3ed1d1941 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -38,7 +38,7 @@
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/dio_solver.h"
-#include "theory/arith/difference_manager.h"
+#include "theory/arith/congruence_manager.h"
 
 #include "theory/arith/constraint.h"
 
@@ -241,14 +241,8 @@ private:
    */
   Tableau d_smallTableauCopy;
 
-  /**
-   * The atom database keeps track of the atoms that have been preregistered.
-   * Used to add unate propagations.
-   */
-  //ArithAtomDatabase d_atomDatabase;
-
   /** This keeps track of difference equalities. Mostly for sharing. */
-  DifferenceManager d_differenceManager;
+  ArithCongruenceManager d_congruenceManager;
 
   /** This implements the Simplex decision procedure. */
   SimplexDecisionProcedure d_simplex;