This commit merges in the changes from branches/arithmetic/refactor0

- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work.
- Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver.
- Fix to an assertion in CDQueue.
- Implements a CDArithVarSet using a vector of booleans and CDList.
- Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.

1 files changed, 3 insertions, 7 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e6bdbfba0..929ef1173 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -24,9 +24,10 @@
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
+#include "context/cdqueue.h"
 #include "expr/node.h"
 
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/arithvar_set.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
@@ -161,18 +162,13 @@ private:
   /**
    * Queue of Integer variables that are known to be equal to a constant.
    */
-  context::CDList<ArithVar> d_constantIntegerVariables;
-  /** Iterator over d_constantIntegerVariables. */
-  context::CDO<unsigned int> d_CivIterator;
+  context::CDQueue<ArithVar> d_constantIntegerVariables;
 
   Node callDioSolver();
   Node dioCutting();
 
   Comparison mkIntegerEqualityFromAssignment(ArithVar v);
 
-  //TODO Replace with a more efficient check
-  CDArithVarSet d_varsInDioSolver;
-
   /**
    * If ArithVar v maps to the node n in d_removednode,
    * then n = (= asNode(v) rhs) where rhs is a term that