diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-04 01:19:43 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-04 01:19:43 +0000 |
commit | 738114852c81e7203fda105d5386dc26187fcb87 (patch) | |
tree | 90d2d41dc0c7916ec164d97cfd437e0afa76375e /src/theory/arith/arith_utilities.h | |
parent | c0558a1625887f4761cfbad371e07af06a49b38b (diff) |
Fix to bug 211. ArithVar is now typedefed to uint32_t.
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 4ae0e44ef..f099e77b9 100644 --- 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); } |