src/expr/attribute.h

   1 /*********************                                                        */
   2 /*! \file attribute.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Tim King
   6  ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Node attributes.
  13  **
  14  ** Node attributes.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 /* There are strong constraints on ordering of declarations of
  20  * attributes and nodes due to template use */
  21 #include "expr/node.h"
  22 #include "expr/type_node.h"
  23 #include "context/context.h"
  24
  25 #ifndef __CVC4__EXPR__ATTRIBUTE_H
  26 #define __CVC4__EXPR__ATTRIBUTE_H
  27
  28 #include <string>
  29 #include <stdint.h>
  30 #include "expr/attribute_unique_id.h"
  31
  32 // include supporting templates
  33 #define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
  34 #include "expr/attribute_internals.h"
  35 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
  36
  37 namespace CVC4 {
  38
  39 class SmtEngine;
  40
  41 namespace smt {
  42   extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
  43 }/* CVC4::smt namespace */
  44
  45 namespace expr {
  46 namespace attr {
  47
  48 // ATTRIBUTE MANAGER ===========================================================
  49
  50 struct SmtAttributes {
  51   SmtAttributes(context::Context*);
  52
  53   // IF YOU ADD ANY TABLES, don't forget to add them also to the
  54   // implementation of deleteAllAttributes().
  55
  56   /** Underlying hash table for context-dependent boolean-valued attributes */
  57   CDAttrHash<bool> d_cdbools;
  58   /** Underlying hash table for context-dependent integral-valued attributes */
  59   CDAttrHash<uint64_t> d_cdints;
  60   /** Underlying hash table for context-dependent node-valued attributes */
  61   CDAttrHash<TNode> d_cdtnodes;
  62   /** Underlying hash table for context-dependent node-valued attributes */
  63   CDAttrHash<Node> d_cdnodes;
  64   /** Underlying hash table for context-dependent string-valued attributes */
  65   CDAttrHash<std::string> d_cdstrings;
  66   /** Underlying hash table for context-dependent pointer-valued attributes */
  67   CDAttrHash<void*> d_cdptrs;
  68
  69   /** Delete all attributes of given node */
  70   void deleteAllAttributes(TNode n);
  71
  72   template <class T>
  73   void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv);
  74
  75 };/* struct SmtAttributes */
  76
  77 /**
  78  * A container for the main attribute tables of the system.  There's a
  79  * one-to-one NodeManager : AttributeManager correspondence.
  80  */
  81 class AttributeManager {
  82
  83   template <class T>
  84   void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
  85
  86   template <class T>
  87   void deleteAllFromTable(AttrHash<T>& table);
  88
  89   template <class T>
  90   void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids);
  91
  92   template <class T>
  93   void reconstructTable(AttrHash<T>& table);
  94
  95   /**
  96    * getTable<> is a helper template that gets the right table from an
  97    * AttributeManager given its type.
  98    */
  99   template <class T, bool context_dep>
 100   friend struct getTable;
 101
 102   bool d_inGarbageCollection;
 103
 104   void clearDeleteAllAttributesBuffer();
 105
 106   SmtAttributes& getSmtAttributes(SmtEngine*);
 107   const SmtAttributes& getSmtAttributes(SmtEngine*) const;
 108
 109 public:
 110
 111   /** Construct an attribute manager. */
 112   AttributeManager();
 113
 114   // IF YOU ADD ANY TABLES, don't forget to add them also to the
 115   // implementation of deleteAllAttributes().
 116
 117   /** Underlying hash table for boolean-valued attributes */
 118   AttrHash<bool> d_bools;
 119   /** Underlying hash table for integral-valued attributes */
 120   AttrHash<uint64_t> d_ints;
 121   /** Underlying hash table for node-valued attributes */
 122   AttrHash<TNode> d_tnodes;
 123   /** Underlying hash table for node-valued attributes */
 124   AttrHash<Node> d_nodes;
 125   /** Underlying hash table for types attributes */
 126   AttrHash<TypeNode> d_types;
 127   /** Underlying hash table for string-valued attributes */
 128   AttrHash<std::string> d_strings;
 129   /** Underlying hash table for pointer-valued attributes */
 130   AttrHash<void*> d_ptrs;
 131
 132   /**
 133    * Get a particular attribute on a particular node.
 134    *
 135    * @param nv the node about which to inquire
 136    * @param attr the attribute kind to get
 137    * @return the attribute value, if set, or a default-constructed
 138    * AttrKind::value_type if not.
 139    */
 140   template <class AttrKind>
 141   typename AttrKind::value_type getAttribute(NodeValue* nv,
 142                                              const AttrKind& attr) const;
 143
 144   /**
 145    * Determine if a particular attribute exists for a particular node.
 146    *
 147    * @param nv the node about which to inquire
 148    * @param attr the attribute kind to inquire about
 149    * @return true if the given node has the given attribute
 150    */
 151   template <class AttrKind>
 152   bool hasAttribute(NodeValue* nv,
 153                     const AttrKind& attr) const;
 154
 155   /**
 156    * Determine if a particular attribute exists for a particular node,
 157    * and get it if it does.
 158    *
 159    * @param nv the node about which to inquire
 160    * @param attr the attribute kind to inquire about
 161    * @param ret a pointer to a return value, set in case the node has
 162    * the attribute
 163    * @return true if the given node has the given attribute
 164    */
 165   template <class AttrKind>
 166   bool getAttribute(NodeValue* nv,
 167                     const AttrKind& attr,
 168                     typename AttrKind::value_type& ret) const;
 169
 170   /**
 171    * Set a particular attribute on a particular node.
 172    *
 173    * @param nv the node for which to set the attribute
 174    * @param attr the attribute kind to set
 175    * @param value a pointer to a return value, set in case the node has
 176    * the attribute
 177    * @return true if the given node has the given attribute
 178    */
 179   template <class AttrKind>
 180   void setAttribute(NodeValue* nv,
 181                     const AttrKind& attr,
 182                     const typename AttrKind::value_type& value);
 183
 184   /**
 185    * Remove all attributes associated to the given node.
 186    *
 187    * @param nv the node from which to delete attributes
 188    */
 189   void deleteAllAttributes(NodeValue* nv);
 190
 191   /**
 192    * Remove all attributes from the tables.
 193    */
 194   void deleteAllAttributes();
 195
 196   /**
 197    * Returns true if a table is currently being deleted.
 198    */
 199   bool inGarbageCollection() const ;
 200
 201   /**
 202    * Determines the AttrTableId of an attribute.
 203    *
 204    * @param attr the attribute
 205    * @return the id of the attribute table.
 206    */
 207   template <class AttrKind>
 208   static AttributeUniqueId getAttributeId(const AttrKind& attr);
 209
 210   /** A list of attributes. */
 211   typedef std::vector< const AttributeUniqueId* > AttrIdVec;
 212
 213   /** Deletes a list of attributes. */
 214   void deleteAttributes(const AttrIdVec& attributeIds);
 215
 216   /**
 217    * debugHook() is an empty function for the purpose of debugging
 218    * the AttributeManager without recompiling all of CVC4.
 219    * Formally this is a nop.
 220    */
 221   void debugHook(int debugFlag);
 222 };
 223
 224 }/* CVC4::expr::attr namespace */
 225
 226 // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
 227
 228 namespace attr {
 229
 230 /**
 231  * The getTable<> template provides (static) access to the
 232  * AttributeManager field holding the table.
 233  */
 234 template <class T, bool context_dep>
 235 struct getTable;
 236
 237 /** Access the "d_bools" member of AttributeManager. */
 238 template <>
 239 struct getTable<bool, false> {
 240   static const AttrTableId id = AttrTableBool;
 241   typedef AttrHash<bool> table_type;
 242   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 243     return am.d_bools;
 244   }
 245   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 246     return am.d_bools;
 247   }
 248 };
 249
 250 /** Access the "d_ints" member of AttributeManager. */
 251 template <>
 252 struct getTable<uint64_t, false> {
 253   static const AttrTableId id = AttrTableUInt64;
 254   typedef AttrHash<uint64_t> table_type;
 255   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 256     return am.d_ints;
 257   }
 258   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 259     return am.d_ints;
 260   }
 261 };
 262
 263 /** Access the "d_tnodes" member of AttributeManager. */
 264 template <>
 265 struct getTable<TNode, false> {
 266   static const AttrTableId id = AttrTableTNode;
 267   typedef AttrHash<TNode> table_type;
 268   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 269     return am.d_tnodes;
 270   }
 271   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 272     return am.d_tnodes;
 273   }
 274 };
 275
 276 /** Access the "d_nodes" member of AttributeManager. */
 277 template <>
 278 struct getTable<Node, false> {
 279   static const AttrTableId id = AttrTableNode;
 280   typedef AttrHash<Node> table_type;
 281   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 282     return am.d_nodes;
 283   }
 284   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 285     return am.d_nodes;
 286   }
 287 };
 288
 289 /** Access the "d_types" member of AttributeManager. */
 290 template <>
 291 struct getTable<TypeNode, false> {
 292   static const AttrTableId id = AttrTableTypeNode;
 293   typedef AttrHash<TypeNode> table_type;
 294   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 295     return am.d_types;
 296   }
 297   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 298     return am.d_types;
 299   }
 300 };
 301
 302 /** Access the "d_strings" member of AttributeManager. */
 303 template <>
 304 struct getTable<std::string, false> {
 305   static const AttrTableId id = AttrTableString;
 306   typedef AttrHash<std::string> table_type;
 307   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 308     return am.d_strings;
 309   }
 310   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 311     return am.d_strings;
 312   }
 313 };
 314
 315 /** Access the "d_ptrs" member of AttributeManager. */
 316 template <class T>
 317 struct getTable<T*, false> {
 318   static const AttrTableId id = AttrTablePointer;
 319   typedef AttrHash<void*> table_type;
 320   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 321     return am.d_ptrs;
 322   }
 323   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 324     return am.d_ptrs;
 325   }
 326 };
 327
 328 /** Access the "d_ptrs" member of AttributeManager. */
 329 template <class T>
 330 struct getTable<const T*, false> {
 331   static const AttrTableId id = AttrTablePointer;
 332   typedef AttrHash<void*> table_type;
 333   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 334     return am.d_ptrs;
 335   }
 336   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 337     return am.d_ptrs;
 338   }
 339 };
 340
 341 /** Access the "d_cdbools" member of AttributeManager. */
 342 template <>
 343 struct getTable<bool, true> {
 344   static const AttrTableId id = AttrTableCDBool;
 345   typedef CDAttrHash<bool> table_type;
 346   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 347     return am.getSmtAttributes(smt).d_cdbools;
 348   }
 349   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 350     return am.getSmtAttributes(smt).d_cdbools;
 351   }
 352 };
 353
 354 /** Access the "d_cdints" member of AttributeManager. */
 355 template <>
 356 struct getTable<uint64_t, true> {
 357   static const AttrTableId id = AttrTableCDUInt64;
 358   typedef CDAttrHash<uint64_t> table_type;
 359   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 360     return am.getSmtAttributes(smt).d_cdints;
 361   }
 362   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 363     return am.getSmtAttributes(smt).d_cdints;
 364   }
 365 };
 366
 367 /** Access the "d_tnodes" member of AttributeManager. */
 368 template <>
 369 struct getTable<TNode, true> {
 370   static const AttrTableId id = AttrTableCDTNode;
 371   typedef CDAttrHash<TNode> table_type;
 372   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 373     return am.getSmtAttributes(smt).d_cdtnodes;
 374   }
 375   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 376     return am.getSmtAttributes(smt).d_cdtnodes;
 377   }
 378 };
 379
 380 /** Access the "d_cdnodes" member of AttributeManager. */
 381 template <>
 382 struct getTable<Node, true> {
 383   static const AttrTableId id = AttrTableCDNode;
 384   typedef CDAttrHash<Node> table_type;
 385   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 386     return am.getSmtAttributes(smt).d_cdnodes;
 387   }
 388   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 389     return am.getSmtAttributes(smt).d_cdnodes;
 390   }
 391 };
 392
 393 /** Access the "d_cdstrings" member of AttributeManager. */
 394 template <>
 395 struct getTable<std::string, true> {
 396   static const AttrTableId id = AttrTableCDString;
 397   typedef CDAttrHash<std::string> table_type;
 398   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 399     return am.getSmtAttributes(smt).d_cdstrings;
 400   }
 401   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 402     return am.getSmtAttributes(smt).d_cdstrings;
 403   }
 404 };
 405
 406 /** Access the "d_cdptrs" member of AttributeManager. */
 407 template <class T>
 408 struct getTable<T*, true> {
 409   static const AttrTableId id = AttrTableCDPointer;
 410   typedef CDAttrHash<void*> table_type;
 411   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 412     return am.getSmtAttributes(smt).d_cdptrs;
 413   }
 414   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 415     return am.getSmtAttributes(smt).d_cdptrs;
 416   }
 417 };
 418
 419 /** Access the "d_cdptrs" member of AttributeManager. */
 420 template <class T>
 421 struct getTable<const T*, true> {
 422   static const AttrTableId id = AttrTableCDPointer;
 423   typedef CDAttrHash<void*> table_type;
 424   static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
 425     return am.getSmtAttributes(smt).d_cdptrs;
 426   }
 427   static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
 428     return am.getSmtAttributes(smt).d_cdptrs;
 429   }
 430 };
 431
 432 }/* CVC4::expr::attr namespace */
 433
 434 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
 435
 436 namespace attr {
 437
 438 // implementation for AttributeManager::getAttribute()
 439 template <class AttrKind>
 440 typename AttrKind::value_type
 441 AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
 442   typedef typename AttrKind::value_type value_type;
 443   typedef KindValueToTableValueMapping<value_type> mapping;
 444   typedef typename getTable<value_type, AttrKind::context_dependent>::
 445             table_type table_type;
 446
 447   const table_type& ah =
 448     getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
 449   typename table_type::const_iterator i =
 450     ah.find(std::make_pair(AttrKind::getId(), nv));
 451
 452   if(i == ah.end()) {
 453     return typename AttrKind::value_type();
 454   }
 455
 456   return mapping::convertBack((*i).second);
 457 }
 458
 459 /* Helper template class for hasAttribute(), specialized based on
 460  * whether AttrKind has a "default value" that all Nodes implicitly
 461  * have or not. */
 462 template <bool has_default, class AttrKind>
 463 struct HasAttribute;
 464
 465 /**
 466  * Specialization of HasAttribute<> helper template for AttrKinds
 467  * with a default value.
 468  */
 469 template <class AttrKind>
 470 struct HasAttribute<true, AttrKind> {
 471   /** This implementation is simple; it's always true. */
 472   static inline bool hasAttribute(const AttributeManager* am,
 473                                   NodeValue* nv) {
 474     return true;
 475   }
 476
 477   /**
 478    * This implementation returns the AttrKind's default value if the
 479    * Node doesn't have the given attribute.
 480    */
 481   static inline bool getAttribute(const AttributeManager* am,
 482                                   NodeValue* nv,
 483                                   typename AttrKind::value_type& ret) {
 484     typedef typename AttrKind::value_type value_type;
 485     typedef KindValueToTableValueMapping<value_type> mapping;
 486     typedef typename getTable<value_type,
 487                               AttrKind::context_dependent>::table_type
 488       table_type;
 489
 490     const table_type& ah =
 491       getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
 492     typename table_type::const_iterator i =
 493       ah.find(std::make_pair(AttrKind::getId(), nv));
 494
 495     if(i == ah.end()) {
 496       ret = AttrKind::default_value;
 497     } else {
 498       ret = mapping::convertBack((*i).second);
 499     }
 500
 501     return true;
 502   }
 503 };
 504
 505 /**
 506  * Specialization of HasAttribute<> helper template for AttrKinds
 507  * without a default value.
 508  */
 509 template <class AttrKind>
 510 struct HasAttribute<false, AttrKind> {
 511   static inline bool hasAttribute(const AttributeManager* am,
 512                                   NodeValue* nv) {
 513     typedef typename AttrKind::value_type value_type;
 514     //typedef KindValueToTableValueMapping<value_type> mapping;
 515     typedef typename getTable<value_type, AttrKind::context_dependent>::
 516               table_type table_type;
 517
 518     const table_type& ah =
 519       getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
 520     typename table_type::const_iterator i =
 521       ah.find(std::make_pair(AttrKind::getId(), nv));
 522
 523     if(i == ah.end()) {
 524       return false;
 525     }
 526
 527     return true;
 528   }
 529
 530   static inline bool getAttribute(const AttributeManager* am,
 531                                   NodeValue* nv,
 532                                   typename AttrKind::value_type& ret) {
 533     typedef typename AttrKind::value_type value_type;
 534     typedef KindValueToTableValueMapping<value_type> mapping;
 535     typedef typename getTable<value_type, AttrKind::context_dependent>::
 536               table_type table_type;
 537
 538     const table_type& ah =
 539       getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
 540     typename table_type::const_iterator i =
 541       ah.find(std::make_pair(AttrKind::getId(), nv));
 542
 543     if(i == ah.end()) {
 544       return false;
 545     }
 546
 547     ret = mapping::convertBack((*i).second);
 548
 549     return true;
 550   }
 551 };
 552
 553 template <class AttrKind>
 554 bool AttributeManager::hasAttribute(NodeValue* nv,
 555                                     const AttrKind&) const {
 556   return HasAttribute<AttrKind::has_default_value, AttrKind>::
 557            hasAttribute(this, nv);
 558 }
 559
 560 template <class AttrKind>
 561 bool AttributeManager::getAttribute(NodeValue* nv,
 562                                     const AttrKind&,
 563                                     typename AttrKind::value_type& ret) const {
 564   return HasAttribute<AttrKind::has_default_value, AttrKind>::
 565            getAttribute(this, nv, ret);
 566 }
 567
 568 template <class AttrKind>
 569 inline void
 570 AttributeManager::setAttribute(NodeValue* nv,
 571                                const AttrKind&,
 572                                const typename AttrKind::value_type& value) {
 573   typedef typename AttrKind::value_type value_type;
 574   typedef KindValueToTableValueMapping<value_type> mapping;
 575   typedef typename getTable<value_type, AttrKind::context_dependent>::
 576             table_type table_type;
 577
 578   table_type& ah =
 579     getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
 580   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 581 }
 582
 583 /**
 584  * Search for the NodeValue in all attribute tables and remove it,
 585  * calling the cleanup function if one is defined.
 586  *
 587  * This cannot use nv as anything other than a pointer!
 588  */
 589 template <class T>
 590 inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
 591                                               NodeValue* nv) {
 592   for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) {
 593     typedef AttributeTraits<T, false> traits_t;
 594     typedef AttrHash<T> hash_t;
 595     std::pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
 596     if(traits_t::getCleanup()[id] != NULL) {
 597       typename hash_t::iterator i = table.find(pr);
 598       if(i != table.end()) {
 599         traits_t::getCleanup()[id]((*i).second);
 600         table.erase(pr);
 601       }
 602     } else {
 603       table.erase(pr);
 604     }
 605   }
 606 }
 607
 608 /**
 609  * Obliterate a NodeValue from a (context-dependent) attribute table.
 610  */
 611 template <class T>
 612 inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table,
 613                                            NodeValue* nv) {
 614   for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) {
 615     table.obliterate(std::make_pair(id, nv));
 616   }
 617 }
 618
 619 /**
 620  * Remove all attributes from the table calling the cleanup function
 621  * if one is defined.
 622  */
 623 template <class T>
 624 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
 625   Assert(!d_inGarbageCollection);
 626   d_inGarbageCollection = true;
 627
 628   bool anyRequireClearing = false;
 629   typedef AttributeTraits<T, false> traits_t;
 630   typedef AttrHash<T> hash_t;
 631   for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) {
 632     if(traits_t::getCleanup()[id] != NULL) {
 633       anyRequireClearing = true;
 634     }
 635   }
 636
 637   if(anyRequireClearing) {
 638     typename hash_t::iterator it = table.begin();
 639     typename hash_t::iterator it_end = table.end();
 640
 641     while (it != it_end){
 642       uint64_t id = (*it).first.first;
 643       /*
 644       Debug("attrgc") << "id " << id
 645                       << " node_value: " << ((*it).first.second)
 646                       << std::endl;
 647       */
 648       if(traits_t::getCleanup()[id] != NULL) {
 649         traits_t::getCleanup()[id]((*it).second);
 650       }
 651       ++it;
 652     }
 653   }
 654   table.clear();
 655   d_inGarbageCollection = false;
 656   Assert(!d_inGarbageCollection);
 657 }
 658
 659 template <class AttrKind>
 660 AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
 661   typedef typename AttrKind::value_type value_type;
 662   AttrTableId tableId = getTable<value_type,
 663                                  AttrKind::context_dependent>::id;
 664   return AttributeUniqueId(tableId, attr.getId());
 665 }
 666
 667 template <class T>
 668 void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
 669   d_inGarbageCollection = true;
 670   typedef AttributeTraits<T, false> traits_t;
 671   typedef AttrHash<T> hash_t;
 672
 673   typename hash_t::iterator it = table.begin();
 674   typename hash_t::iterator tmp;
 675   typename hash_t::iterator it_end = table.end();
 676
 677   std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
 678   std::vector<uint64_t>::const_iterator end_ids = ids.end();
 679
 680   size_t initialSize = table.size();
 681   while (it != it_end){
 682     uint64_t id = (*it).first.first;
 683
 684     if(std::binary_search(begin_ids, end_ids, id)){
 685       tmp = it;
 686       ++it;
 687       if(traits_t::getCleanup()[id] != NULL) {
 688         traits_t::getCleanup()[id]((*tmp).second);
 689       }
 690       table.erase(tmp);
 691     }else{
 692       ++it;
 693     }
 694   }
 695   d_inGarbageCollection = false;
 696   static const size_t ReconstructShrinkRatio = 8;
 697   if(initialSize/ReconstructShrinkRatio > table.size()){
 698     reconstructTable(table);
 699   }
 700 }
 701
 702 template <class T>
 703 void AttributeManager::reconstructTable(AttrHash<T>& table){
 704   d_inGarbageCollection = true;
 705   typedef AttrHash<T> hash_t;
 706   hash_t cpy;
 707   cpy.insert(table.begin(), table.end());
 708   cpy.swap(table);
 709   d_inGarbageCollection = false;
 710 }
 711
 712
 713 }/* CVC4::expr::attr namespace */
 714 }/* CVC4::expr namespace */
 715
 716 template <class AttrKind>
 717 inline typename AttrKind::value_type
 718 NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
 719   return d_attrManager->getAttribute(nv, AttrKind());
 720 }
 721
 722 template <class AttrKind>
 723 inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
 724                                       const AttrKind&) const {
 725   return d_attrManager->hasAttribute(nv, AttrKind());
 726 }
 727
 728 template <class AttrKind>
 729 inline bool
 730 NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
 731                           typename AttrKind::value_type& ret) const {
 732   return d_attrManager->getAttribute(nv, AttrKind(), ret);
 733 }
 734
 735 template <class AttrKind>
 736 inline void
 737 NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
 738                           const typename AttrKind::value_type& value) {
 739   d_attrManager->setAttribute(nv, AttrKind(), value);
 740 }
 741
 742 template <class AttrKind>
 743 inline typename AttrKind::value_type
 744 NodeManager::getAttribute(TNode n, const AttrKind&) const {
 745   return d_attrManager->getAttribute(n.d_nv, AttrKind());
 746 }
 747
 748 template <class AttrKind>
 749 inline bool
 750 NodeManager::hasAttribute(TNode n, const AttrKind&) const {
 751   return d_attrManager->hasAttribute(n.d_nv, AttrKind());
 752 }
 753
 754 template <class AttrKind>
 755 inline bool
 756 NodeManager::getAttribute(TNode n, const AttrKind&,
 757                           typename AttrKind::value_type& ret) const {
 758   return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
 759 }
 760
 761 template <class AttrKind>
 762 inline void
 763 NodeManager::setAttribute(TNode n, const AttrKind&,
 764                           const typename AttrKind::value_type& value) {
 765   d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
 766 }
 767
 768 template <class AttrKind>
 769 inline typename AttrKind::value_type
 770 NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
 771   return d_attrManager->getAttribute(n.d_nv, AttrKind());
 772 }
 773
 774 template <class AttrKind>
 775 inline bool
 776 NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
 777   return d_attrManager->hasAttribute(n.d_nv, AttrKind());
 778 }
 779
 780 template <class AttrKind>
 781 inline bool
 782 NodeManager::getAttribute(TypeNode n, const AttrKind&,
 783                           typename AttrKind::value_type& ret) const {
 784   return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
 785 }
 786
 787 template <class AttrKind>
 788 inline void
 789 NodeManager::setAttribute(TypeNode n, const AttrKind&,
 790                           const typename AttrKind::value_type& value) {
 791   d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
 792 }
 793
 794 }/* CVC4 namespace */
 795
 796 #endif /* __CVC4__EXPR__ATTRIBUTE_H */