src/expr/attribute.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** attribute.h
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Node attributes.
  14  **
  15  ** Attribute structures:
  16  **
  17  ** An attribute structure looks like the following:
  18  **
  19  ** struct VarNameAttr {
  20  **
  21  **   // the value type for this attribute
  22  **   typedef std::string value_type;
  23  **
  24  **   // an extra hash value (to avoid same-value-type collisions)
  25  **   enum { hash_value = 1 };
  26  **
  27  **   // cleanup routine when the Node goes away
  28  **   static inline void cleanup(const std::string&) {
  29  **   }
  30  ** }
  31  **/
  32
  33 /* There are strong constraints on ordering of declarations of
  34  * attributes and nodes due to template use */
  35 #include "expr/node.h"
  36
  37 #ifndef __CVC4__EXPR__ATTRIBUTE_H
  38 #define __CVC4__EXPR__ATTRIBUTE_H
  39
  40 #include <stdint.h>
  41
  42 #include <string>
  43 #include <ext/hash_map>
  44
  45 #include "config.h"
  46 #include "context/context.h"
  47 #include "expr/soft_node.h"
  48 #include "expr/type.h"
  49
  50 #include "util/output.h"
  51
  52 namespace CVC4 {
  53 namespace expr {
  54
  55 // ATTRIBUTE HASH FUNCTIONS ====================================================
  56
  57 struct AttrHashFcn {
  58   enum { LARGE_PRIME = 1 };
  59   std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
  60     return p.first * LARGE_PRIME + p.second.hash();
  61   }
  62 };
  63
  64 struct AttrHashBoolFcn {
  65   std::size_t operator()(const SoftNode& n) const {
  66     return n.hash();
  67   }
  68 };
  69
  70 // ATTRIBUTE TYPE MAPPINGS =====================================================
  71
  72 template <class T>
  73 struct KindValueToTableValueMapping {
  74   typedef T table_value_type;
  75   inline static T convert(const T& t) { return t; }
  76   inline static T convertBack(const T& t) { return t; }
  77 };
  78
  79 template <>
  80 struct KindValueToTableValueMapping<bool> {
  81   typedef uint64_t table_value_type;
  82   inline static uint64_t convert(const bool& t) { return t; }
  83   inline static bool convertBack(const uint64_t& t) { return t; }
  84 };
  85
  86 template <class T>
  87 struct KindValueToTableValueMapping<T*> {
  88   typedef void* table_value_type;
  89   inline static void* convert(const T*& t) {
  90     return reinterpret_cast<void*>(t);
  91   }
  92   inline static T* convertBack(void*& t) {
  93     return reinterpret_cast<T*>(t);
  94   }
  95 };
  96
  97 template <class T>
  98 struct KindValueToTableValueMapping<const T*> {
  99   typedef void* table_value_type;
 100   inline static void* convert(const T* const& t) {
 101     return reinterpret_cast<void*>(const_cast<T*>(t));
 102   }
 103   inline static const T* convertBack(const void*& t) {
 104     return reinterpret_cast<const T*>(t);
 105   }
 106 };
 107
 108 template <class AttrKind, class T>
 109 struct OwnTable;
 110
 111 template <class AttrKind, class T>
 112 struct KindValueToTableValueMapping<OwnTable<AttrKind, T> > {
 113   typedef typename KindValueToTableValueMapping<T>::table_value_type table_value_type;
 114 };
 115
 116 template <class AttrKind>
 117 struct KindTableMapping {
 118   typedef typename AttrKind::value_type table_identifier;
 119 };
 120
 121 // ATTRIBUTE HASH TABLES =======================================================
 122
 123 // use a TAG to indicate which table it should be in
 124 template <class value_type>
 125 struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
 126
 127 template <>
 128 class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
 129
 130   typedef __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> super;
 131
 132   class BitAccessor {
 133
 134     uint64_t& d_word;
 135
 136     unsigned d_bit;
 137
 138   public:
 139
 140     BitAccessor(uint64_t& word, unsigned bit) :
 141       d_word(word),
 142       d_bit(bit) {
 143     }
 144
 145     BitAccessor& operator=(bool b) {
 146       if(b) {
 147         // set the bit
 148         d_word |= (1 << d_bit);
 149       } else {
 150         // clear the bit
 151         d_word &= ~(1 << d_bit);
 152       }
 153
 154       return *this;
 155     }
 156
 157     operator bool() const {
 158       return (d_word & (1 << d_bit)) ? true : false;
 159     }
 160   };
 161
 162   class BitIterator {
 163
 164     std::pair<const SoftNode, uint64_t>* d_entry;
 165
 166     unsigned d_bit;
 167
 168   public:
 169
 170     BitIterator() :
 171       d_entry(NULL),
 172       d_bit(0) {
 173     }
 174
 175     BitIterator(std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
 176       d_entry(&entry),
 177       d_bit(bit) {
 178     }
 179
 180     std::pair<const SoftNode, BitAccessor> operator*() {
 181       return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
 182     }
 183
 184     bool operator==(const BitIterator& b) {
 185       return d_entry == b.d_entry && d_bit == b.d_bit;
 186     }
 187   };
 188
 189   class ConstBitIterator {
 190
 191     const std::pair<const SoftNode, uint64_t>* d_entry;
 192
 193     unsigned d_bit;
 194
 195   public:
 196
 197     ConstBitIterator() :
 198       d_entry(NULL),
 199       d_bit(0) {
 200     }
 201
 202     ConstBitIterator(const std::pair<const SoftNode, uint64_t>& entry, unsigned bit) :
 203       d_entry(&entry),
 204       d_bit(bit) {
 205     }
 206
 207     std::pair<const SoftNode, bool> operator*() {
 208       return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
 209     }
 210
 211     bool operator==(const ConstBitIterator& b) {
 212       return d_entry == b.d_entry && d_bit == b.d_bit;
 213     }
 214   };
 215
 216 public:
 217
 218   typedef std::pair<unsigned, SoftNode> key_type;
 219   typedef bool data_type;
 220   typedef std::pair<const key_type, data_type> value_type;
 221
 222   typedef BitIterator iterator;
 223   typedef ConstBitIterator const_iterator;
 224
 225   BitIterator find(const std::pair<unsigned, SoftNode>& k) {
 226     super::iterator i = super::find(k.second);
 227     if(i == super::end()) {
 228       return BitIterator();
 229     }
 230     Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
 231     return BitIterator(*i, k.first);
 232   }
 233
 234   BitIterator end() {
 235     return BitIterator();
 236   }
 237
 238   ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const {
 239     super::const_iterator i = super::find(k.second);
 240     if(i == super::end()) {
 241       return ConstBitIterator();
 242     }
 243     Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
 244     return ConstBitIterator(*i, k.first);
 245   }
 246
 247   ConstBitIterator end() const {
 248     return ConstBitIterator();
 249   }
 250
 251   BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
 252     uint64_t& word = super::operator[](k.second);
 253     return BitAccessor(word, k.first);
 254   }
 255 };/* class AttrHash<bool> */
 256
 257 // ATTRIBUTE PATTERN ===========================================================
 258
 259 /**
 260  * An "attribute type" structure.
 261  */
 262 template <class T, class value_t>
 263 struct Attribute {
 264
 265   /** the value type for this attribute */
 266   typedef value_t value_type;
 267
 268   /** cleanup routine when the Node goes away */
 269   static inline void cleanup(const value_t&) {}
 270
 271   static inline unsigned getId() { return s_id; }
 272   static inline unsigned getHashValue() { return s_hashValue; }
 273
 274   static const bool has_default_value = false;
 275
 276 private:
 277
 278   /** an id */
 279   static const unsigned s_id;
 280
 281   /** an extra hash value (to avoid same-value-type collisions) */
 282   static const unsigned s_hashValue;
 283 };
 284
 285 /**
 286  * An "attribute type" structure for boolean flags (special).
 287  */
 288 template <class T>
 289 struct Attribute<T, bool> {
 290
 291   /** the value type for this attribute */
 292   typedef bool value_type;
 293
 294   /** cleanup routine when the Node goes away */
 295   static inline void cleanup(const bool&) {}
 296
 297   static inline unsigned getId() { return s_id; }
 298   static inline unsigned getHashValue() { return s_hashValue; }
 299
 300   static const bool has_default_value = true;
 301   static const bool default_value = false;
 302
 303   static inline unsigned checkID(unsigned id) {
 304     AlwaysAssert(id <= 63,
 305                  "Too many boolean node attributes registered during initialization !");
 306     return id;
 307   }
 308
 309 private:
 310
 311   /** a bit assignment */
 312   static const unsigned s_id;
 313
 314   /** an extra hash value (to avoid same-value-type collisions) */
 315   static const unsigned s_hashValue;
 316 };
 317
 318 // SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
 319
 320 namespace attr {
 321   struct VarName {};
 322   struct Type {};
 323
 324   template <class T>
 325   struct LastAttributeId {
 326     static unsigned s_id;
 327   };
 328
 329   template <class T>
 330   unsigned LastAttributeId<T>::s_id = 0;
 331 }/* CVC4::expr::attr namespace */
 332
 333 typedef Attribute<attr::VarName, std::string> VarNameAttr;
 334 typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
 335
 336 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 337
 338 template <class T, class value_t>
 339 const unsigned Attribute<T, value_t>::s_id =
 340   attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
 341 template <class T, class value_t>
 342 const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
 343
 344 template <class T>
 345 const unsigned Attribute<T, bool>::s_id =
 346   Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
 347 template <class T>
 348 const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
 349
 350 class AttributeManager;
 351
 352 template <class T>
 353 struct getTable {
 354   //inline AttrHash<KindTableValueMapping<T> >& get(AttributeManager& am);
 355 };
 356
 357 // ATTRIBUTE MANAGER ===========================================================
 358
 359 class AttributeManager {
 360   NodeManager* d_nm;
 361
 362   AttrHash<bool>    d_bools;
 363   AttrHash<uint64_t>    d_ints;
 364   AttrHash<SoftNode>    d_exprs;
 365   AttrHash<std::string> d_strings;
 366   AttrHash<void*>       d_ptrs;
 367
 368   template <class T>
 369   friend struct getTable;
 370
 371 public:
 372   AttributeManager(NodeManager* nm) : d_nm(nm) {}
 373
 374   template <class AttrKind>
 375   typename AttrKind::value_type getAttribute(const Node& n,
 376                                              const AttrKind&);
 377
 378   template <class AttrKind>
 379   bool hasAttribute(const Node& n,
 380                     const AttrKind&);
 381
 382   template <class AttrKind>
 383   bool hasAttribute(const Node& n,
 384                     const AttrKind&,
 385                     typename AttrKind::value_type*);
 386
 387   template <class AttrKind>
 388   void setAttribute(const Node& n,
 389                     const AttrKind&,
 390                     const typename AttrKind::value_type& value);
 391 };
 392
 393 // MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
 394
 395 template <>
 396 struct getTable<bool> {
 397   typedef AttrHash<bool> table_type;
 398   static inline table_type& get(AttributeManager& am) {
 399     return am.d_bools;
 400   }
 401 };
 402
 403 template <>
 404 struct getTable<uint64_t> {
 405   typedef AttrHash<uint64_t> table_type;
 406   static inline table_type& get(AttributeManager& am) {
 407     return am.d_ints;
 408   }
 409 };
 410
 411 template <>
 412 struct getTable<Node> {
 413   typedef AttrHash<SoftNode> table_type;
 414   static inline table_type& get(AttributeManager& am) {
 415     return am.d_exprs;
 416   }
 417 };
 418
 419 template <>
 420 struct getTable<std::string> {
 421   typedef AttrHash<std::string> table_type;
 422   static inline table_type& get(AttributeManager& am) {
 423     return am.d_strings;
 424   }
 425 };
 426
 427 template <class T>
 428 struct getTable<T*> {
 429   typedef AttrHash<void*> table_type;
 430   static inline table_type& get(AttributeManager& am) {
 431     return am.d_ptrs;
 432   }
 433 };
 434
 435 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
 436
 437 template <class AttrKind>
 438 typename AttrKind::value_type AttributeManager::getAttribute(const Node& n,
 439                                                              const AttrKind&) {
 440
 441   typedef typename AttrKind::value_type value_type;
 442   typedef KindValueToTableValueMapping<value_type> mapping;
 443   typedef typename getTable<value_type>::table_type table_type;
 444
 445   table_type& ah = getTable<value_type>::get(*this);
 446   typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
 447
 448   if(i == ah.end()) {
 449     return typename AttrKind::value_type();
 450   }
 451
 452   return mapping::convertBack((*i).second);
 453 }
 454
 455 /* helper template class for hasAttribute(), specialized based on
 456  * whether AttrKind has a "default value" that all Nodes implicitly
 457  * have or not. */
 458 template <bool has_default, class AttrKind>
 459 struct HasAttribute;
 460
 461 template <class AttrKind>
 462 struct HasAttribute<true, AttrKind> {
 463   static inline bool hasAttribute(AttributeManager* am,
 464                                   const Node& n) {
 465     return true;
 466   }
 467
 468   static inline bool hasAttribute(AttributeManager* am,
 469                                   const Node& n,
 470                                   typename AttrKind::value_type* ret) {
 471     if(ret != NULL) {
 472       typedef typename AttrKind::value_type value_type;
 473       typedef KindValueToTableValueMapping<value_type> mapping;
 474       typedef typename getTable<value_type>::table_type table_type;
 475
 476       table_type& ah = getTable<value_type>::get(*am);
 477       typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
 478
 479       if(i == ah.end()) {
 480         *ret = AttrKind::default_value;
 481       } else {
 482         *ret = mapping::convertBack((*i).second);
 483       }
 484     }
 485
 486     return true;
 487   }
 488 };
 489
 490 template <class AttrKind>
 491 struct HasAttribute<false, AttrKind> {
 492   static inline bool hasAttribute(AttributeManager* am,
 493                                   const Node& n) {
 494     typedef typename AttrKind::value_type value_type;
 495     typedef KindValueToTableValueMapping<value_type> mapping;
 496     typedef typename getTable<value_type>::table_type table_type;
 497
 498     table_type& ah = getTable<value_type>::get(*am);
 499     typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
 500
 501     if(i == ah.end()) {
 502       return false;
 503     }
 504
 505     return true;
 506   }
 507
 508   static inline bool hasAttribute(AttributeManager* am,
 509                                   const Node& n,
 510                                   typename AttrKind::value_type* ret) {
 511     typedef typename AttrKind::value_type value_type;
 512     typedef KindValueToTableValueMapping<value_type> mapping;
 513     typedef typename getTable<value_type>::table_type table_type;
 514
 515     table_type& ah = getTable<value_type>::get(*am);
 516     typename table_type::iterator i = ah.find(std::make_pair(AttrKind::getId(), n));
 517
 518     if(i == ah.end()) {
 519       return false;
 520     }
 521
 522     if(ret != NULL) {
 523       *ret = mapping::convertBack((*i).second);
 524     }
 525
 526     return true;
 527   }
 528 };
 529
 530 template <class AttrKind>
 531 bool AttributeManager::hasAttribute(const Node& n,
 532                                     const AttrKind&) {
 533   return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n);
 534 }
 535
 536 template <class AttrKind>
 537 bool AttributeManager::hasAttribute(const Node& n,
 538                                     const AttrKind&,
 539                                     typename AttrKind::value_type* ret) {
 540   return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, n, ret);
 541 }
 542
 543 template <class AttrKind>
 544 inline void AttributeManager::setAttribute(const Node& n,
 545                                            const AttrKind&,
 546                                            const typename AttrKind::value_type& value) {
 547
 548   typedef typename AttrKind::value_type value_type;
 549   typedef KindValueToTableValueMapping<value_type> mapping;
 550   typedef typename getTable<value_type>::table_type table_type;
 551
 552   table_type& ah = getTable<value_type>::get(*this);
 553   ah[std::make_pair(AttrKind::getId(), n)] = mapping::convert(value);
 554 }
 555
 556 }/* CVC4::expr namespace */
 557 }/* CVC4 namespace */
 558
 559 #endif /* __CVC4__EXPR__ATTRIBUTE_H */