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.

23 files changed, 213 insertions, 120 deletions

diff --git a/src/context/cdqueue.h b/src/context/cdqueue.h
index f84b66349..d733e0b1c 100644
--- a/src/context/cdqueue.h
+++ b/src/context/cdqueue.h
@@ -122,7 +122,7 @@ public:
       // Some elements have been enqueued and dequeued in the same
       // context and now the queue is empty we can destruct them.
       CDList<T>::truncateList(d_lastsave);
-      Assert(d_size ==  d_lastsave);
+      Assert(CDList<T>::d_size ==  d_lastsave);
       d_iter = d_lastsave;
     }
   }
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 7934140a0..4cff4a782 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -7,6 +7,7 @@ noinst_LTLIBRARIES = libarith.la
 
 libarith_la_SOURCES = \
 	theory_arith_type_rules.h \
+	arithvar.h \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
 	arith_static_learner.h \
diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h
index 1e7e3460b..8c7069975 100644
--- a/src/theory/arith/arith_priority_queue.h
+++ b/src/theory/arith/arith_priority_queue.h
@@ -23,7 +23,7 @@
 #ifndef __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
 #define __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
 
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp
index 4b52133da..dc9b0ddb9 100644
--- a/src/theory/arith/arith_prop_manager.cpp
+++ b/src/theory/arith/arith_prop_manager.cpp
@@ -26,13 +26,14 @@
 #include "context/cdhashmap.h"
 #include "context/cdo.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
 using namespace CVC4::kind;
 using namespace std;
 
 
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
 bool ArithPropManager::isAsserted(TNode n) const{
   Node satValue = d_valuation.getSatValue(n);
   if(satValue.isNull()){
@@ -166,3 +167,7 @@ ArithPropManager::Statistics::~Statistics()
   StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode);
   StatisticsRegistry::unregisterStat(&d_addedPropagation);
 }
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
index 2bac21437..900a0ed58 100644
--- a/src/theory/arith/arith_prop_manager.h
+++ b/src/theory/arith/arith_prop_manager.h
@@ -23,7 +23,7 @@
 #define __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H
 
 #include "theory/valuation.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/atom_database.h"
 #include "theory/arith/delta_rational.h"
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index c0ef02ec4..ca0aa4d14 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -26,14 +26,18 @@
 #include <set>
 #include <stack>
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+namespace CVC4 {
+namespace theory {
+namespace arith {
 
 bool isVariable(TNode t){
   return t.getMetaKind() == kind::metakind::VARIABLE;
 }
 
+bool ArithRewriter::isAtom(TNode n) {
+  return arith::isRelationOperator(n.getKind());
+}
+
 RewriteResponse ArithRewriter::rewriteConstant(TNode t){
   Assert(t.getMetaKind() == kind::metakind::CONSTANT);
   Node val = coerceToRationalNode(t);
@@ -364,3 +368,7 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){
     return RewriteResponse(REWRITE_AGAIN, mult);
   }
 }
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 822514f38..07c009b2e 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -11,10 +11,10 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Rewriter for arithmetic.
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Rewriter for the theory of arithmetic.  This rewrites to the normal form for
+ ** arithmetic. See theory/arith/normal_form.h for more information.
  **/
 
 #include "cvc4_private.h"
@@ -23,9 +23,6 @@
 #define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/theory.h"
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/normal_form.h"
-
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -33,6 +30,18 @@ namespace theory {
 namespace arith {
 
 class ArithRewriter {
+public:
+
+  static RewriteResponse preRewrite(TNode n);
+  static RewriteResponse postRewrite(TNode n);
+  static Node rewriteEquality(TNode equality) {
+    // Arithmetic owns the domain, so this is totally ok
+    return Rewriter::rewrite(equality);
+  }
+
+  static void init() { }
+
+  static void shutdown() { }
 
 private:
 
@@ -59,24 +68,7 @@ private:
   static RewriteResponse postRewriteAtom(TNode t);
   static RewriteResponse postRewriteAtomConstantRHS(TNode t);
 
-public:
-
-  static RewriteResponse preRewrite(TNode n);
-  static RewriteResponse postRewrite(TNode n);
-  static Node rewriteEquality(TNode equality) {
-    // Arithmetic owns the domain, so this is totally ok
-    return Rewriter::rewrite(equality);
-  }
-
-  static void init() { }
-
-  static void shutdown() { }
-
-private:
-
-  static inline bool isAtom(TNode n) {
-    return arith::isRelationOperator(n.getKind());
-  }
+  static bool isAtom(TNode n);
 
   static inline bool isTerm(TNode n) {
     return !isAtom(n);
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index d4d495486..2f4f6e32b 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -30,11 +30,11 @@
 #include <vector>
 
 using namespace std;
-
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
 
 
 ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) :
@@ -495,3 +495,7 @@ void ArithStaticLearner::addBound(TNode n) {
     break;
   }
 }
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 44b55440e..a5d94ec40 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -11,10 +11,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Arith utilities are common inline functions for dealing with nodes.
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Arith utilities are common functions for dealing with nodes.
  **/
 
 #include "cvc4_private.h"
@@ -23,41 +22,21 @@
 #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
 #include "util/rational.h"
+#include "util/integer.h"
 #include "expr/node.h"
-#include "expr/attribute.h"
 #include "theory/arith/delta_rational.h"
 #include "context/cdhashset.h"
-#include <vector>
-#include <stdint.h>
-#include <limits>
 #include <ext/hash_map>
+#include <vector>
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
-typedef uint32_t ArithVar;
-//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
-#define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
-
-//Maps from Nodes -> ArithVars, and vice versa
-typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
-typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
-
 //Sets of Nodes
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
 
-typedef context::CDHashSet<ArithVar> CDArithVarSet;
-
-class ArithVarCallBack {
-public:
-  virtual void callback(ArithVar x) = 0;
-};
-
-
-
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
@@ -126,7 +105,7 @@ inline bool isRelationOperator(Kind k){
  * Given a relational kind, k, return the kind k' s.t.
  * swapping the lefthand and righthand side is equivalent.
  *
- * The following equivalence should hold, 
+ * The following equivalence should hold,
  *   (k l r) <=> (k' r l)
  */
 inline Kind reverseRelationKind(Kind k){
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
new file mode 100644
index 000000000..52dc9fd6a
--- /dev/null
+++ b/src/theory/arith/arithvar.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file arithvar.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Defines ArithVar which is the internal representation of variables in arithmetic
+ **
+ ** This defines ArithVar which is the internal representation of variables in
+ ** arithmetic. This is a typedef from uint32_t to ArithVar.
+ ** This file also provides utilities for ArithVars.
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__ARITHVAR_H
+#define __CVC4__THEORY__ARITH__ARITHVAR_H
+
+#include <limits>
+#include <stdint.h>
+#include <ext/hash_map>
+#include "expr/node.h"
+#include "context/cdhashset.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+typedef uint32_t ArithVar;
+const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+
+//Maps from Nodes -> ArithVars, and vice versa
+typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
+typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
+
+/**
+ * ArithVarCallBack provides a mechanism for agreeing on callbacks while
+ * breaking mutual recursion inclusion order problems.
+ */
+class ArithVarCallBack {
+public:
+  virtual void callback(ArithVar x) = 0;
+};
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
+
+#endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index 1dc8ddf38..e8428850d 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -23,7 +23,7 @@
 #define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
 
 
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdhashmap.h"
diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index 68937acc4..b502849fd 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -23,7 +23,10 @@
 #define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H
 
 #include <vector>
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
+#include "context/context.h"
+#include "context/cdlist.h"
+
 
 namespace CVC4 {
 namespace theory {
@@ -244,15 +247,6 @@ public:
     }
   }
 
-  /** Invalidates iterators */
-  /* void init(ArithVar x, bool val) { */
-  /*   Assert(x >= allocated()); */
-  /*   increaseSize(x); */
-  /*   if(val){ */
-  /*     add(x); */
-  /*   } */
-  /* } */
-
   /**
    * Invalidates iterators.
    */
@@ -325,6 +319,68 @@ public:
   }
 };
 
+class CDArithVarSet {
+private:
+
+  class RemoveIntWrapper{
+  private:
+    ArithVar d_var;
+    ArithVarCallBack& d_onDestruction;
+
+  public:
+    RemoveIntWrapper(ArithVar v, ArithVarCallBack& onDestruction):
+      d_var(v), d_onDestruction(onDestruction)
+    {}
+
+    ~RemoveIntWrapper(){
+      d_onDestruction.callback(d_var);
+    }
+  };
+
+  std::vector<bool> d_set;
+  context::CDList<RemoveIntWrapper> d_list;
+
+  class OnDestruction : public ArithVarCallBack {
+  private:
+    std::vector<bool>& d_set;
+  public:
+    OnDestruction(std::vector<bool>& set):
+      d_set(set)
+    {}
+
+    void callback(ArithVar x){
+      Assert(x < d_set.size());
+      d_set[x] = false;
+    }
+  };
+
+  OnDestruction d_callback;
+
+public:
+  CDArithVarSet(context::Context* c) :
+    d_list(c), d_callback(d_set)
+  { }
+
+  /** This cannot be const as garbage collection is done lazily. */
+  bool contains(ArithVar x) const{
+    if(x < d_set.size()){
+      return d_set[x];
+    }else{
+      return false;
+    }
+  }
+
+  void insert(ArithVar x){
+    Assert(!contains(x));
+    if(x >= d_set.size()){
+      d_set.resize(x+1, false);
+    }
+    d_list.push_back(RemoveIntWrapper(x, d_callback));
+    d_set[x] = true;
+  }
+};
+
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/atom_database.cpp b/src/theory/arith/atom_database.cpp
index 774d0eb22..3476eb8f5 100644
--- a/src/theory/arith/atom_database.cpp
+++ b/src/theory/arith/atom_database.cpp
@@ -22,13 +22,12 @@
 
 #include <list>
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
-
+using namespace std;
 using namespace CVC4::kind;
 
-using namespace std;
+namespace CVC4 {
+namespace theory {
+namespace arith {
 
 ArithAtomDatabase::ArithAtomDatabase(context::Context* cxt, OutputChannel& out) :
   d_arithOut(out), d_setsMap()
@@ -537,3 +536,7 @@ Node ArithAtomDatabase::getWeakerImpliedLowerBound(TNode lowerBound) const {
   Debug("arith::unate") << lowerBound <<" -> " << result << std::endl;
   return result;
 }
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h
index 46b070651..c6e7f314d 100644
--- a/src/theory/arith/difference_manager.h
+++ b/src/theory/arith/difference_manager.h
@@ -5,7 +5,7 @@
 #ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
 #define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
 
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/uf/equality_engine.h"
 #include "context/cdo.h"
 #include "context/cdlist.h"
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index da41d94cd..677040615 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -25,7 +25,6 @@
 
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/arith_utilities.h"
 #include "util/rational.h"
 
 #include "util/stats.h"
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index aa8a49238..4d1d917b3 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -33,7 +33,7 @@
 #define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H
 
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
 
diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h
index e3eebae5c..8887daa8d 100644
--- a/src/theory/arith/ordered_set.h
+++ b/src/theory/arith/ordered_set.h
@@ -109,13 +109,6 @@ typedef std::map<Rational, BoundValueEntry> BoundValueSet;
 
 typedef std::set<TNode, RightHandRationalLT> EqualValueSet;
 
-// struct SetCleanupStrategy{
-//   static void cleanup(OrderedSet* l){
-//     Debug("arithgc") << "cleaning up  " << l << "\n";
-//     delete l;
-//   }
-// };
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index f113c4d34..65b0083d9 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -23,9 +23,10 @@
 
 using namespace std;
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
 
 
 bool ArithPartialModel::boundsAreEqual(ArithVar x){
@@ -395,3 +396,7 @@ void ArithPartialModel::computeDelta(){
   }
   d_deltaIsSafe = true;
 }
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index d9fa51d8d..7a2a97726 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -21,7 +21,7 @@
 
 #include "context/context.h"
 #include "context/cdvector.h"
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "expr/attribute.h"
 #include "expr/node.h"
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d69de3756..39c0bc20b 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -50,7 +50,7 @@
 #ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
 #define __CVC4__THEORY__ARITH__SIMPLEX_H
 
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/arith_priority_queue.h"
 #include "theory/arith/arithvar_set.h"
 #include "theory/arith/delta_rational.h"
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 321f66c5f..1fcbdf13d 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/attribute.h"
 
-#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
 #include "theory/arith/arithvar_set.h"
 #include "theory/arith/normal_form.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index bea87fdde..a1d57af66 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -47,14 +47,13 @@
 #include <stdint.h>
 
 using namespace std;
-
-using namespace CVC4;
 using namespace CVC4::kind;
 
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+namespace CVC4 {
+namespace theory {
+namespace arith {
 
-static const uint32_t RESET_START = 2;
+const uint32_t RESET_START = 2;
 
 
 TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
@@ -64,8 +63,6 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_learner(d_pbSubstitutions),
   d_nextIntegerCheckVar(0),
   d_constantIntegerVariables(c),
-  d_CivIterator(c,0),
-  d_varsInDioSolver(c),
   d_diseq(c),
   d_partialModel(c, d_differenceManager),
   d_tableau(),
@@ -167,7 +164,7 @@ Node TheoryArith::AssertLower(ArithVar x_i, DeltaRational& c_i, TNode original){
   }
 
   //TODO Relax to less than?
-  if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
+  if(d_partialModel.lessThanLowerBound(x_i, c_i)){
     return Node::null();
   }
 
@@ -225,7 +222,7 @@ Node TheoryArith::AssertUpper(ArithVar x_i, DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
+  if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
     return Node::null(); //sat
   }
 
@@ -763,21 +760,15 @@ Node TheoryArith::dioCutting(){
 }
 
 Node TheoryArith::callDioSolver(){
-  while(d_CivIterator < d_constantIntegerVariables.size()){
-    ArithVar v = d_constantIntegerVariables[d_CivIterator];
-    d_CivIterator = d_CivIterator + 1;
+  while(!d_constantIntegerVariables.empty()){
+    ArithVar v = d_constantIntegerVariables.front();
+    d_constantIntegerVariables.pop();
 
     Debug("arith::dio")  << v << endl;
 
     Assert(isInteger(v));
     Assert(d_partialModel.boundsAreEqual(v));
 
-    if(d_varsInDioSolver.find(v) != d_varsInDioSolver.end()){
-      continue;
-    }else{
-      d_varsInDioSolver.insert(v);
-    }
-
     TNode lb = d_partialModel.getLowerConstraint(v);
     TNode ub = d_partialModel.getUpperConstraint(v);
 
@@ -1491,3 +1482,7 @@ void TheoryArith::propagateCandidates(){
     propagateCandidate(candidate);
   }
 }
+
+}; /* namesapce arith */
+}; /* namespace theory */
+}; /* namespace CVC4 */
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