branches/arith-indexed-variables merged into the main trunk.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index d2c07900d..4ae0e44ef 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -24,11 +24,27 @@
 
 #include "util/rational.h"
 #include "expr/node.h"
+#include "expr/attribute.h"
+#include <stdint.h>
+#include <limits>
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+
+typedef uint64_t ArithVar;
+//static const ArithVar ARITHVAR_SENTINEL = std::numeric_limits<ArithVar>::max();
+#define ARITHVAR_SENTINEL std::numeric_limits<ArithVar>::max()
+
+struct ArithVarAttrID{};
+typedef expr::Attribute<ArithVarAttrID,ArithVar> ArithVarAttr;
+
+inline ArithVar asArithVar(TNode x){
+  Assert(x.hasAttribute(ArithVarAttr()));
+  return x.getAttribute(ArithVarAttr());
+}
+
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }