Context-dependent expr attributes are now attached to a specific SmtEngine, and the SAT context is owned by the SmtEngine.

1 files changed, 96 insertions, 77 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 0bca760ef..432fbbac9 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -20,6 +20,7 @@
  * attributes and nodes due to template use */
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "context/context.h"
 
 #ifndef __CVC4__EXPR__ATTRIBUTE_H
 #define __CVC4__EXPR__ATTRIBUTE_H
@@ -34,34 +35,20 @@
 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 
 namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+  extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
+}/* CVC4::smt namespace */
+
 namespace expr {
 namespace attr {
 
 // ATTRIBUTE MANAGER ===========================================================
 
-/**
- * A container for the main attribute tables of the system.  There's a
- * one-to-one NodeManager : AttributeManager correspondence.
- */
-class AttributeManager {
-
-  // IF YOU ADD ANY TABLES, don't forget to add them also to the
-  // implementation of deleteAllAttributes().
-
-  /** Underlying hash table for boolean-valued attributes */
-  AttrHash<bool> d_bools;
-  /** Underlying hash table for integral-valued attributes */
-  AttrHash<uint64_t> d_ints;
-  /** Underlying hash table for node-valued attributes */
-  AttrHash<TNode> d_tnodes;
-  /** Underlying hash table for node-valued attributes */
-  AttrHash<Node> d_nodes;
-  /** Underlying hash table for types attributes */
-  AttrHash<TypeNode> d_types;
-  /** Underlying hash table for string-valued attributes */
-  AttrHash<std::string> d_strings;
-  /** Underlying hash table for pointer-valued attributes */
-  AttrHash<void*> d_ptrs;
+struct SmtAttributes {
+  SmtAttributes(context::Context*);
 
   // IF YOU ADD ANY TABLES, don't forget to add them also to the
   // implementation of deleteAllAttributes().
@@ -79,12 +66,23 @@ class AttributeManager {
   /** Underlying hash table for context-dependent pointer-valued attributes */
   CDAttrHash<void*> d_cdptrs;
 
-  template <class T>
-  void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
+  /** Delete all attributes of given node */
+  void deleteAllAttributes(TNode n);
 
   template <class T>
   void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv);
 
+};/* struct SmtAttributes */
+
+/**
+ * A container for the main attribute tables of the system.  There's a
+ * one-to-one NodeManager : AttributeManager correspondence.
+ */
+class AttributeManager {
+
+  template <class T>
+  void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
+
   template <class T>
   void deleteAllFromTable(AttrHash<T>& table);
 
@@ -105,10 +103,31 @@ class AttributeManager {
 
   void clearDeleteAllAttributesBuffer();
 
+  SmtAttributes& getSmtAttributes(SmtEngine*);
+  const SmtAttributes& getSmtAttributes(SmtEngine*) const;
+
 public:
 
   /** Construct an attribute manager. */
-  AttributeManager(context::Context* ctxt);
+  AttributeManager();
+
+  // IF YOU ADD ANY TABLES, don't forget to add them also to the
+  // implementation of deleteAllAttributes().
+
+  /** Underlying hash table for boolean-valued attributes */
+  AttrHash<bool> d_bools;
+  /** Underlying hash table for integral-valued attributes */
+  AttrHash<uint64_t> d_ints;
+  /** Underlying hash table for node-valued attributes */
+  AttrHash<TNode> d_tnodes;
+  /** Underlying hash table for node-valued attributes */
+  AttrHash<Node> d_nodes;
+  /** Underlying hash table for types attributes */
+  AttrHash<TypeNode> d_types;
+  /** Underlying hash table for string-valued attributes */
+  AttrHash<std::string> d_strings;
+  /** Underlying hash table for pointer-valued attributes */
+  AttrHash<void*> d_ptrs;
 
   /**
    * Get a particular attribute on a particular node.
@@ -220,10 +239,10 @@ template <>
 struct getTable<bool, false> {
   static const AttrTableId id = AttrTableBool;
   typedef AttrHash<bool> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_bools;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_bools;
   }
 };
@@ -233,10 +252,10 @@ template <>
 struct getTable<uint64_t, false> {
   static const AttrTableId id = AttrTableUInt64;
   typedef AttrHash<uint64_t> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_ints;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_ints;
   }
 };
@@ -246,10 +265,10 @@ template <>
 struct getTable<TNode, false> {
   static const AttrTableId id = AttrTableTNode;
   typedef AttrHash<TNode> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_tnodes;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_tnodes;
   }
 };
@@ -259,10 +278,10 @@ template <>
 struct getTable<Node, false> {
   static const AttrTableId id = AttrTableNode;
   typedef AttrHash<Node> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_nodes;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_nodes;
   }
 };
@@ -272,10 +291,10 @@ template <>
 struct getTable<TypeNode, false> {
   static const AttrTableId id = AttrTableTypeNode;
   typedef AttrHash<TypeNode> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_types;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_types;
   }
 };
@@ -285,10 +304,10 @@ template <>
 struct getTable<std::string, false> {
   static const AttrTableId id = AttrTableString;
   typedef AttrHash<std::string> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_strings;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_strings;
   }
 };
@@ -298,10 +317,10 @@ template <class T>
 struct getTable<T*, false> {
   static const AttrTableId id = AttrTablePointer;
   typedef AttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_ptrs;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_ptrs;
   }
 };
@@ -311,10 +330,10 @@ template <class T>
 struct getTable<const T*, false> {
   static const AttrTableId id = AttrTablePointer;
   typedef AttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am) {
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
     return am.d_ptrs;
   }
-  static inline const table_type& get(const AttributeManager& am) {
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
     return am.d_ptrs;
   }
 };
@@ -324,11 +343,11 @@ template <>
 struct getTable<bool, true> {
   static const AttrTableId id = AttrTableCDBool;
   typedef CDAttrHash<bool> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdbools;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdbools;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdbools;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdbools;
   }
 };
 
@@ -337,11 +356,11 @@ template <>
 struct getTable<uint64_t, true> {
   static const AttrTableId id = AttrTableCDUInt64;
   typedef CDAttrHash<uint64_t> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdints;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdints;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdints;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdints;
   }
 };
 
@@ -350,11 +369,11 @@ template <>
 struct getTable<TNode, true> {
   static const AttrTableId id = AttrTableCDTNode;
   typedef CDAttrHash<TNode> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdtnodes;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdtnodes;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdtnodes;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdtnodes;
   }
 };
 
@@ -363,11 +382,11 @@ template <>
 struct getTable<Node, true> {
   static const AttrTableId id = AttrTableCDNode;
   typedef CDAttrHash<Node> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdnodes;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdnodes;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdnodes;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdnodes;
   }
 };
 
@@ -376,11 +395,11 @@ template <>
 struct getTable<std::string, true> {
   static const AttrTableId id = AttrTableCDString;
   typedef CDAttrHash<std::string> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdstrings;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdstrings;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdstrings;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdstrings;
   }
 };
 
@@ -389,11 +408,11 @@ template <class T>
 struct getTable<T*, true> {
   static const AttrTableId id = AttrTableCDPointer;
   typedef CDAttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdptrs;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdptrs;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdptrs;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdptrs;
   }
 };
 
@@ -402,11 +421,11 @@ template <class T>
 struct getTable<const T*, true> {
   static const AttrTableId id = AttrTableCDPointer;
   typedef CDAttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am) {
-    return am.d_cdptrs;
+  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdptrs;
   }
-  static inline const table_type& get(const AttributeManager& am) {
-    return am.d_cdptrs;
+  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+    return am.getSmtAttributes(smt).d_cdptrs;
   }
 };
 
@@ -426,7 +445,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
             table_type table_type;
 
   const table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this);
+    getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
   typename table_type::const_iterator i =
     ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -469,7 +488,7 @@ struct HasAttribute<true, AttrKind> {
       table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am);
+      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -497,7 +516,7 @@ struct HasAttribute<false, AttrKind> {
               table_type table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am);
+      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -517,7 +536,7 @@ struct HasAttribute<false, AttrKind> {
               table_type table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am);
+      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -557,7 +576,7 @@ AttributeManager::setAttribute(NodeValue* nv,
             table_type table_type;
 
   table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this);
+    getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
@@ -590,8 +609,8 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
  * Obliterate a NodeValue from a (context-dependent) attribute table.
  */
 template <class T>
-inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
-                                              NodeValue* nv) {
+inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table,
+                                           NodeValue* nv) {
   for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) {
     table.obliterate(std::make_pair(id, nv));
   }