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