This merges in the branch cvc4/branches/arithmetic/matrix into trunk.

- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
 

2 files changed, 105 insertions, 1 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index 13a151ffc..d979a9c16 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -25,4 +25,5 @@ libcontext_la_SOURCES = \
 	cdvector.h \
 	cdmaybe.h \
 	stacking_map.h \
-	stacking_vector.h
+	stacking_vector.h \
+	cddense_set.h
\ No newline at end of file
diff --git a/src/context/cddense_set.h b/src/context/cddense_set.h
new file mode 100644
index 000000000..592925705
--- /dev/null
+++ b/src/context/cddense_set.h
@@ -0,0 +1,103 @@
+/*********************                                                        */
+/*! \file cddense_set.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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 This is an abstraction of a set of unsigned integers.
+ **
+ ** This is an abstraction of a set of unsigned integers.
+ ** This class is designed to provide constant time insertion, element_of,
+ ** and fast iteration. This is done by storing backing vectors of size greater than
+ ** the maximum key.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+
+#include "context/context.h"
+#include "context/cdlist_forward.h"
+#include "context/cdlist.h"
+
+#include "util/index.h"
+
+namespace CVC4 {
+namespace context {
+
+template <class CleanUp = DefaultCleanUp<Index> >
+class CDDenseSet {
+public:
+  typedef Index Element;
+
+private:
+
+  class RemoveIntCleanup {
+  private:
+    std::vector<bool>& d_set;
+
+    /**
+     * The CleanUp functor.
+     */
+    CleanUp d_cleanUp;
+  public:
+    RemoveIntCleanup(std::vector<bool>& set, const CleanUp& cleanup)
+      : d_set(set), d_cleanUp(cleanup)
+    {}
+
+    void operator()(Element* p){
+      d_cleanup(p);
+
+      ArithVar x = *p;
+      Assert(d_set[x]);
+      d_set[x] = false;
+    }
+  };
+
+  typedef CDList<Element, RemoveIntCleanup> ElementList;
+  ElementList d_list;
+
+  std::vector<bool> d_set;
+
+public:
+  typedef ElementList::const_iterator const_iterator;
+
+  CDDenseSet(context::Context* c, const CleanUp& cleanup = CleanUp())
+    : d_set(), d_list(c, true, RemoveIntCleanup(d_set, cleanup))
+  { }
+
+  /** This cannot be const as garbage collection is done lazily. */
+  bool contains(Element x) const{
+    if(x < d_set.size()){
+      return d_set[x];
+    }else{
+      return false;
+    }
+  }
+
+  void insert(Element x){
+    Assert(!contains(x));
+    if(x >= d_set.size()){
+      d_set.resize(x+1, false);
+    }
+    d_list.push_back(x);
+    d_set[x] = true;
+  }
+
+  const_iterator begin() const { return d_list.begin(); }
+  const_iterator end() const { return d_list.end(); }
+
+};/* class CDDenseSet<> */
+
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */