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, 8 insertions, 4 deletions

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 */