1 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 7cb6c6e99..95614a011 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -22,24 +22,23 @@
 #ifndef __CVC4__THEORY__ARITH__ARITHVAR_H
 #define __CVC4__THEORY__ARITH__ARITHVAR_H
 
-#include <limits>
 #include <ext/hash_map>
 #include "expr/node.h"
 #include "context/cdhashset.h"
-#include "context/cdhashset.h"
 
 #include "util/index.h"
+#include "util/dense_map.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
 typedef Index ArithVar;
-const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+extern const ArithVar ARITHVAR_SENTINEL;
 
 //Maps from Nodes -> ArithVars, and vice versa
 typedef __gnu_cxx::hash_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
-typedef __gnu_cxx::hash_map<ArithVar, Node> ArithVarToNodeMap;
+typedef DenseMap<Node> ArithVarToNodeMap;
 
 /**
  * ArithVarCallBack provides a mechanism for agreeing on callbacks while
@@ -50,6 +49,16 @@ public:
   virtual void operator()(ArithVar x) = 0;
 };
 
+/**
+ * Requests arithmetic variables for internal use,
+ * and releases arithmetic variables that are no longer being used.
+ */
+class ArithVarMalloc {
+public:
+  virtual ArithVar request() = 0;
+  virtual void release(ArithVar v) = 0;
+};
+
 class TNodeCallBack {
 public:
   virtual void operator()(TNode n) = 0;