1 /********************* */ 2 /*! \file attribute.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King, Dejan Jovanovic 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing 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 24 #ifndef __CVC4__EXPR__ATTRIBUTE_H 25 #define __CVC4__EXPR__ATTRIBUTE_H 26 27 #include <string> 28 #include <stdint.h> 29 #include "expr/attribute_unique_id.h" 30 31 // include supporting templates 32 #define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H 33 #include "expr/attribute_internals.h" 34 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H 35 36 namespace CVC4 { 37 namespace expr { 38 namespace attr { 39 40 // ATTRIBUTE MANAGER =========================================================== 41 42 /** 43 * A container for the main attribute tables of the system. There's a 44 * one-to-one NodeManager : AttributeManager correspondence. 45 */ 46 class AttributeManager { 47 48 template <class T> 49 void deleteFromTable(AttrHash<T>& table, NodeValue* nv); 50 51 template <class T> 52 void deleteAllFromTable(AttrHash<T>& table); 53 54 template <class T> 55 void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids); 56 57 template <class T> 58 void reconstructTable(AttrHash<T>& table); 59 60 /** 61 * getTable<> is a helper template that gets the right table from an 62 * AttributeManager given its type. 63 */ 64 template <class T, bool context_dep> 65 friend struct getTable; 66 67 bool d_inGarbageCollection; 68 69 void clearDeleteAllAttributesBuffer(); 70 71 public: 72 73 /** Construct an attribute manager. */ 74 AttributeManager(); 75 76 // IF YOU ADD ANY TABLES, don't forget to add them also to the 77 // implementation of deleteAllAttributes(). 78 79 /** Underlying hash table for boolean-valued attributes */ 80 AttrHash<bool> d_bools; 81 /** Underlying hash table for integral-valued attributes */ 82 AttrHash<uint64_t> d_ints; 83 /** Underlying hash table for node-valued attributes */ 84 AttrHash<TNode> d_tnodes; 85 /** Underlying hash table for node-valued attributes */ 86 AttrHash<Node> d_nodes; 87 /** Underlying hash table for types attributes */ 88 AttrHash<TypeNode> d_types; 89 /** Underlying hash table for string-valued attributes */ 90 AttrHash<std::string> d_strings; 91 92 /** 93 * Get a particular attribute on a particular node. 94 * 95 * @param nv the node about which to inquire 96 * @param attr the attribute kind to get 97 * @return the attribute value, if set, or a default-constructed 98 * AttrKind::value_type if not. 99 */ 100 template <class AttrKind> 101 typename AttrKind::value_type getAttribute(NodeValue* nv, 102 const AttrKind& attr) const; 103 104 /** 105 * Determine if a particular attribute exists for a particular node. 106 * 107 * @param nv the node about which to inquire 108 * @param attr the attribute kind to inquire about 109 * @return true if the given node has the given attribute 110 */ 111 template <class AttrKind> 112 bool hasAttribute(NodeValue* nv, 113 const AttrKind& attr) const; 114 115 /** 116 * Determine if a particular attribute exists for a particular node, 117 * and get it if it does. 118 * 119 * @param nv the node about which to inquire 120 * @param attr the attribute kind to inquire about 121 * @param ret a pointer to a return value, set in case the node has 122 * the attribute 123 * @return true if the given node has the given attribute 124 */ 125 template <class AttrKind> 126 bool getAttribute(NodeValue* nv, 127 const AttrKind& attr, 128 typename AttrKind::value_type& ret) const; 129 130 /** 131 * Set a particular attribute on a particular node. 132 * 133 * @param nv the node for which to set the attribute 134 * @param attr the attribute kind to set 135 * @param value a pointer to a return value, set in case the node has 136 * the attribute 137 * @return true if the given node has the given attribute 138 */ 139 template <class AttrKind> 140 void setAttribute(NodeValue* nv, 141 const AttrKind& attr, 142 const typename AttrKind::value_type& value); 143 144 /** 145 * Remove all attributes associated to the given node. 146 * 147 * @param nv the node from which to delete attributes 148 */ 149 void deleteAllAttributes(NodeValue* nv); 150 151 /** 152 * Remove all attributes from the tables. 153 */ 154 void deleteAllAttributes(); 155 156 /** 157 * Returns true if a table is currently being deleted. 158 */ 159 bool inGarbageCollection() const ; 160 161 /** 162 * Determines the AttrTableId of an attribute. 163 * 164 * @param attr the attribute 165 * @return the id of the attribute table. 166 */ 167 template <class AttrKind> 168 static AttributeUniqueId getAttributeId(const AttrKind& attr); 169 170 /** A list of attributes. */ 171 typedef std::vector< const AttributeUniqueId* > AttrIdVec; 172 173 /** Deletes a list of attributes. */ 174 void deleteAttributes(const AttrIdVec& attributeIds); 175 176 /** 177 * debugHook() is an empty function for the purpose of debugging 178 * the AttributeManager without recompiling all of CVC4. 179 * Formally this is a nop. 180 */ 181 void debugHook(int debugFlag); 182 }; 183 184 }/* CVC4::expr::attr namespace */ 185 186 // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER =============== 187 188 namespace attr { 189 190 /** 191 * The getTable<> template provides (static) access to the 192 * AttributeManager field holding the table. 193 */ 194 template <class T, bool context_dep> 195 struct getTable; 196 197 /** Access the "d_bools" member of AttributeManager. */ 198 template <> 199 struct getTable<bool, false> { 200 static const AttrTableId id = AttrTableBool; 201 typedef AttrHash<bool> table_type; 202 static inline table_type& get(AttributeManager& am) { 203 return am.d_bools; 204 } 205 static inline const table_type& get(const AttributeManager& am) { 206 return am.d_bools; 207 } 208 }; 209 210 /** Access the "d_ints" member of AttributeManager. */ 211 template <> 212 struct getTable<uint64_t, false> { 213 static const AttrTableId id = AttrTableUInt64; 214 typedef AttrHash<uint64_t> table_type; 215 static inline table_type& get(AttributeManager& am) { 216 return am.d_ints; 217 } 218 static inline const table_type& get(const AttributeManager& am) { 219 return am.d_ints; 220 } 221 }; 222 223 /** Access the "d_tnodes" member of AttributeManager. */ 224 template <> 225 struct getTable<TNode, false> { 226 static const AttrTableId id = AttrTableTNode; 227 typedef AttrHash<TNode> table_type; 228 static inline table_type& get(AttributeManager& am) { 229 return am.d_tnodes; 230 } 231 static inline const table_type& get(const AttributeManager& am) { 232 return am.d_tnodes; 233 } 234 }; 235 236 /** Access the "d_nodes" member of AttributeManager. */ 237 template <> 238 struct getTable<Node, false> { 239 static const AttrTableId id = AttrTableNode; 240 typedef AttrHash<Node> table_type; 241 static inline table_type& get(AttributeManager& am) { 242 return am.d_nodes; 243 } 244 static inline const table_type& get(const AttributeManager& am) { 245 return am.d_nodes; 246 } 247 }; 248 249 /** Access the "d_types" member of AttributeManager. */ 250 template <> 251 struct getTable<TypeNode, false> { 252 static const AttrTableId id = AttrTableTypeNode; 253 typedef AttrHash<TypeNode> table_type; 254 static inline table_type& get(AttributeManager& am) { 255 return am.d_types; 256 } 257 static inline const table_type& get(const AttributeManager& am) { 258 return am.d_types; 259 } 260 }; 261 262 /** Access the "d_strings" member of AttributeManager. */ 263 template <> 264 struct getTable<std::string, false> { 265 static const AttrTableId id = AttrTableString; 266 typedef AttrHash<std::string> table_type; 267 static inline table_type& get(AttributeManager& am) { 268 return am.d_strings; 269 } 270 static inline const table_type& get(const AttributeManager& am) { 271 return am.d_strings; 272 } 273 }; 274 275 }/* CVC4::expr::attr namespace */ 276 277 // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== 278 279 namespace attr { 280 281 // implementation for AttributeManager::getAttribute() 282 template <class AttrKind> 283 typename AttrKind::value_type 284 AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const { 285 typedef typename AttrKind::value_type value_type; 286 typedef KindValueToTableValueMapping<value_type> mapping; 287 typedef typename getTable<value_type, AttrKind::context_dependent>:: 288 table_type table_type; 289 290 const table_type& ah = 291 getTable<value_type, AttrKind::context_dependent>::get(*this); 292 typename table_type::const_iterator i = 293 ah.find(std::make_pair(AttrKind::getId(), nv)); 294 295 if(i == ah.end()) { 296 return typename AttrKind::value_type(); 297 } 298 299 return mapping::convertBack((*i).second); 300 } 301 302 /* Helper template class for hasAttribute(), specialized based on 303 * whether AttrKind has a "default value" that all Nodes implicitly 304 * have or not. */ 305 template <bool has_default, class AttrKind> 306 struct HasAttribute; 307 308 /** 309 * Specialization of HasAttribute<> helper template for AttrKinds 310 * with a default value. 311 */ 312 template <class AttrKind> 313 struct HasAttribute<true, AttrKind> { 314 /** This implementation is simple; it's always true. */ 315 static inline bool hasAttribute(const AttributeManager* am, 316 NodeValue* nv) { 317 return true; 318 } 319 320 /** 321 * This implementation returns the AttrKind's default value if the 322 * Node doesn't have the given attribute. 323 */ 324 static inline bool getAttribute(const AttributeManager* am, 325 NodeValue* nv, 326 typename AttrKind::value_type& ret) { 327 typedef typename AttrKind::value_type value_type; 328 typedef KindValueToTableValueMapping<value_type> mapping; 329 typedef typename getTable<value_type, 330 AttrKind::context_dependent>::table_type 331 table_type; 332 333 const table_type& ah = 334 getTable<value_type, AttrKind::context_dependent>::get(*am); 335 typename table_type::const_iterator i = 336 ah.find(std::make_pair(AttrKind::getId(), nv)); 337 338 if(i == ah.end()) { 339 ret = AttrKind::default_value; 340 } else { 341 ret = mapping::convertBack((*i).second); 342 } 343 344 return true; 345 } 346 }; 347 348 /** 349 * Specialization of HasAttribute<> helper template for AttrKinds 350 * without a default value. 351 */ 352 template <class AttrKind> 353 struct HasAttribute<false, AttrKind> { 354 static inline bool hasAttribute(const AttributeManager* am, 355 NodeValue* nv) { 356 typedef typename AttrKind::value_type value_type; 357 //typedef KindValueToTableValueMapping<value_type> mapping; 358 typedef typename getTable<value_type, AttrKind::context_dependent>:: 359 table_type table_type; 360 361 const table_type& ah = 362 getTable<value_type, AttrKind::context_dependent>::get(*am); 363 typename table_type::const_iterator i = 364 ah.find(std::make_pair(AttrKind::getId(), nv)); 365 366 if(i == ah.end()) { 367 return false; 368 } 369 370 return true; 371 } 372 373 static inline bool getAttribute(const AttributeManager* am, 374 NodeValue* nv, 375 typename AttrKind::value_type& ret) { 376 typedef typename AttrKind::value_type value_type; 377 typedef KindValueToTableValueMapping<value_type> mapping; 378 typedef typename getTable<value_type, AttrKind::context_dependent>:: 379 table_type table_type; 380 381 const table_type& ah = 382 getTable<value_type, AttrKind::context_dependent>::get(*am); 383 typename table_type::const_iterator i = 384 ah.find(std::make_pair(AttrKind::getId(), nv)); 385 386 if(i == ah.end()) { 387 return false; 388 } 389 390 ret = mapping::convertBack((*i).second); 391 392 return true; 393 } 394 }; 395 396 template <class AttrKind> 397 bool AttributeManager::hasAttribute(NodeValue* nv, 398 const AttrKind&) const { 399 return HasAttribute<AttrKind::has_default_value, AttrKind>:: 400 hasAttribute(this, nv); 401 } 402 403 template <class AttrKind> 404 bool AttributeManager::getAttribute(NodeValue* nv, 405 const AttrKind&, 406 typename AttrKind::value_type& ret) const { 407 return HasAttribute<AttrKind::has_default_value, AttrKind>:: 408 getAttribute(this, nv, ret); 409 } 410 411 template <class AttrKind> 412 inline void 413 AttributeManager::setAttribute(NodeValue* nv, 414 const AttrKind&, 415 const typename AttrKind::value_type& value) { 416 typedef typename AttrKind::value_type value_type; 417 typedef KindValueToTableValueMapping<value_type> mapping; 418 typedef typename getTable<value_type, AttrKind::context_dependent>:: 419 table_type table_type; 420 421 table_type& ah = 422 getTable<value_type, AttrKind::context_dependent>::get(*this); 423 ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value); 424 } 425 426 /** Search for the NodeValue in all attribute tables and remove it. */ 427 template <class T> 428 inline void AttributeManager::deleteFromTable(AttrHash<T>& table, 429 NodeValue* nv) { 430 // This cannot use nv as anything other than a pointer! 431 const uint64_t last = attr::LastAttributeId<T, false>::getId(); 432 for (uint64_t id = 0; id < last; ++id) 433 { 434 table.erase(std::make_pair(id, nv)); 435 } 436 } 437 438 /** Remove all attributes from the table. */ 439 template <class T> 440 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) { 441 Assert(!d_inGarbageCollection); 442 d_inGarbageCollection = true; 443 table.clear(); 444 d_inGarbageCollection = false; 445 Assert(!d_inGarbageCollection); 446 } 447 448 template <class AttrKind> 449 AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){ 450 typedef typename AttrKind::value_type value_type; 451 AttrTableId tableId = getTable<value_type, 452 AttrKind::context_dependent>::id; 453 return AttributeUniqueId(tableId, attr.getId()); 454 } 455 456 template <class T> 457 void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){ 458 d_inGarbageCollection = true; 459 typedef AttrHash<T> hash_t; 460 461 typename hash_t::iterator it = table.begin(); 462 typename hash_t::iterator tmp; 463 typename hash_t::iterator it_end = table.end(); 464 465 std::vector<uint64_t>::const_iterator begin_ids = ids.begin(); 466 std::vector<uint64_t>::const_iterator end_ids = ids.end(); 467 468 size_t initialSize = table.size(); 469 while (it != it_end){ 470 uint64_t id = (*it).first.first; 471 472 if(std::binary_search(begin_ids, end_ids, id)){ 473 tmp = it; 474 ++it; 475 table.erase(tmp); 476 }else{ 477 ++it; 478 } 479 } 480 d_inGarbageCollection = false; 481 static const size_t ReconstructShrinkRatio = 8; 482 if(initialSize/ReconstructShrinkRatio > table.size()){ 483 reconstructTable(table); 484 } 485 } 486 487 template <class T> 488 void AttributeManager::reconstructTable(AttrHash<T>& table){ 489 d_inGarbageCollection = true; 490 typedef AttrHash<T> hash_t; 491 hash_t cpy; 492 cpy.insert(table.begin(), table.end()); 493 cpy.swap(table); 494 d_inGarbageCollection = false; 495 } 496 497 498 }/* CVC4::expr::attr namespace */ 499 }/* CVC4::expr namespace */ 500 501 template <class AttrKind> 502 inline typename AttrKind::value_type 503 NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const { 504 return d_attrManager->getAttribute(nv, AttrKind()); 505 } 506 507 template <class AttrKind> 508 inline bool NodeManager::hasAttribute(expr::NodeValue* nv, 509 const AttrKind&) const { 510 return d_attrManager->hasAttribute(nv, AttrKind()); 511 } 512 513 template <class AttrKind> 514 inline bool 515 NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&, 516 typename AttrKind::value_type& ret) const { 517 return d_attrManager->getAttribute(nv, AttrKind(), ret); 518 } 519 520 template <class AttrKind> 521 inline void 522 NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&, 523 const typename AttrKind::value_type& value) { 524 d_attrManager->setAttribute(nv, AttrKind(), value); 525 } 526 527 template <class AttrKind> 528 inline typename AttrKind::value_type 529 NodeManager::getAttribute(TNode n, const AttrKind&) const { 530 return d_attrManager->getAttribute(n.d_nv, AttrKind()); 531 } 532 533 template <class AttrKind> 534 inline bool 535 NodeManager::hasAttribute(TNode n, const AttrKind&) const { 536 return d_attrManager->hasAttribute(n.d_nv, AttrKind()); 537 } 538 539 template <class AttrKind> 540 inline bool 541 NodeManager::getAttribute(TNode n, const AttrKind&, 542 typename AttrKind::value_type& ret) const { 543 return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret); 544 } 545 546 template <class AttrKind> 547 inline void 548 NodeManager::setAttribute(TNode n, const AttrKind&, 549 const typename AttrKind::value_type& value) { 550 d_attrManager->setAttribute(n.d_nv, AttrKind(), value); 551 } 552 553 template <class AttrKind> 554 inline typename AttrKind::value_type 555 NodeManager::getAttribute(TypeNode n, const AttrKind&) const { 556 return d_attrManager->getAttribute(n.d_nv, AttrKind()); 557 } 558 559 template <class AttrKind> 560 inline bool 561 NodeManager::hasAttribute(TypeNode n, const AttrKind&) const { 562 return d_attrManager->hasAttribute(n.d_nv, AttrKind()); 563 } 564 565 template <class AttrKind> 566 inline bool 567 NodeManager::getAttribute(TypeNode n, const AttrKind&, 568 typename AttrKind::value_type& ret) const { 569 return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret); 570 } 571 572 template <class AttrKind> 573 inline void 574 NodeManager::setAttribute(TypeNode n, const AttrKind&, 575 const typename AttrKind::value_type& value) { 576 d_attrManager->setAttribute(n.d_nv, AttrKind(), value); 577 } 578 579 }/* CVC4 namespace */ 580 581 #endif /* __CVC4__EXPR__ATTRIBUTE_H */ 582