Fix to bug 211. ArithVar is now typedefed to uint32_t.

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 4ae0e44efdd63f94bc3993b6a965fc661d274eae..f099e77b96c00a9c7c17ff6847c5fbd2919a9e60 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -33,18 +33,28 @@ namespace theory {
 namespace arith {
 
 
-typedef uint64_t ArithVar;
+typedef uint32_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;
+typedef expr::Attribute<ArithVarAttrID,uint64_t> ArithVarAttr;
+
+inline bool hasArithVar(TNode x){
+  return x.hasAttribute(ArithVarAttr());
+}
 
 inline ArithVar asArithVar(TNode x){
-  Assert(x.hasAttribute(ArithVarAttr()));
+  Assert(hasArithVar(x));
+  Assert(x.getAttribute(ArithVarAttr()) <= ARITHVAR_SENTINEL);
   return x.getAttribute(ArithVarAttr());
 }
 
+inline void setArithVar(TNode x, ArithVar a){
+  Assert(!hasArithVar(x));
+  return x.setAttribute(ArithVarAttr(), (uint64_t)a);
+}
+
 inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index be40472b68241839364103bd60a9f954942feaba..4440a8e15cc905f3c37461b863e0ce6f2289bfc4 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -232,13 +232,12 @@ bool TheoryArith::isTheoryLeaf(TNode x) const{
 
 ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
   Assert(isTheoryLeaf(x));
-  Assert(!x.hasAttribute(ArithVarAttr()));
+  Assert(!hasArithVar(x));
 
   ArithVar varX = d_variables.size();
   d_variables.push_back(Node(x));
 
-  x.setAttribute(ArithVarAttr(), varX);
-
+  setArithVar(x,varX);
 
   d_activityMonitor.initActivity(varX);
   d_basicManager.init(varX, basic);
@@ -257,9 +256,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v
     Node n = variable.getNode();
 
     Assert(isTheoryLeaf(n));
-    Assert(n.hasAttribute(ArithVarAttr()));
+    Assert(hasArithVar(n));
 
-    ArithVar av = n.getAttribute(ArithVarAttr());
+    ArithVar av = asArithVar(n);
 
     coeffs.push_back(constant.getValue());
     variables.push_back(av);
@@ -362,7 +361,7 @@ void TheoryArith::registerTerm(TNode tn){
 /* procedure AssertUpper( x_i <= c_i) */
 bool TheoryArith::AssertUpper(TNode n, TNode original){
   TNode nodeX_i = n[0];
-  ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
+  ArithVar x_i = asArithVar(nodeX_i);
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
 
@@ -403,7 +402,7 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
 /* procedure AssertLower( x_i >= c_i ) */
 bool TheoryArith::AssertLower(TNode n, TNode original){
   TNode nodeX_i = n[0];
-  ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
+  ArithVar x_i = asArithVar(nodeX_i);
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
 
@@ -444,7 +443,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
 bool TheoryArith::AssertEquality(TNode n, TNode original){
   Assert(n.getKind() == EQUAL);
   TNode nodeX_i = n[0];
-  ArithVar x_i = nodeX_i.getAttribute(ArithVarAttr());
+  ArithVar x_i = asArithVar(nodeX_i);
   DeltaRational c_i(n[1].getConst<Rational>());
 
   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;