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, 66 insertions, 10 deletions

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