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 */