diff options
Diffstat (limited to 'src/theory/arith/basic.h')
-rw-r--r-- | src/theory/arith/basic.h | 42 |
1 files changed, 26 insertions, 16 deletions
diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h index 11f0f71f0..c52e0881d 100644 --- a/src/theory/arith/basic.h +++ b/src/theory/arith/basic.h @@ -29,22 +29,32 @@ namespace CVC4 { namespace theory { namespace arith { -struct IsBasicAttrID; - -typedef expr::Attribute<IsBasicAttrID, bool> IsBasic; - - -inline bool isBasic(TNode x){ - return x.getAttribute(IsBasic()); -} - -inline void makeBasic(TNode x){ - return x.setAttribute(IsBasic(), true); -} - -inline void makeNonbasic(TNode x){ - return x.setAttribute(IsBasic(), false); -} +class IsBasicManager { +private: + std::vector<bool> d_basic; + +public: + IsBasicManager() : d_basic() {} + + void init(ArithVar var, bool value){ + Assert(var == d_basic.size()); + d_basic.push_back(value); + } + + bool isBasic(ArithVar x) const{ + return d_basic[x]; + } + + void makeBasic(ArithVar x){ + Assert(!isBasic(x)); + d_basic[x] = true; + } + + void makeNonbasic(ArithVar x){ + Assert(isBasic(x)); + d_basic[x] = false; + } +}; }; /* namespace arith */ }; /* namespace theory */ |