diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-09 20:09:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-09 20:09:02 -0600 |
commit | 0df0954069d56e3323a225ffa72c5913d0333ac2 (patch) | |
tree | 398d3497f59fda8d511104224386ca9b59644116 /src/expr/attribute.h | |
parent | b5eb623ea33eeb257d61a18c44e9aa1b2aafabbb (diff) |
Migrate some documentation about attributes (#5390)
From old wiki.
Diffstat (limited to 'src/expr/attribute.h')
-rw-r--r-- | src/expr/attribute.h | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index fcaa47f15..2aa5c2fbc 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -37,6 +37,44 @@ namespace CVC4 { namespace expr { namespace attr { +/** + * Attributes are roughly speaking [almost] global hash tables from Nodes + * (TNodes) to data. Attributes can be thought of as additional fields used to + * extend NodeValues. Attributes are mutable and come in both sat + * context-dependent and non-context dependent varieties. Attributes live only + * as long as the node itself does. If a Node is garbage-collected, Attributes + * associated with it will automatically be garbage collected. (Being in the + * domain of an Attribute does not increase a Node's reference count.) To + * achieve this special relationship with Nodes, Attributes are mapped by hash + * tables (AttrHash<> and CDAttrHash<>) that live in the AttributeManager. The + * AttributeManager is owned by the NodeManager. + * + * Example: + * + * Attributes tend to be defined in a fixed pattern: + * + * ``` + * struct InstLevelAttributeId {}; + * typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; + * ``` + * + * To get the value of an Attribute InstLevelAttribute on a Node n, use + * ``` + * n.getAttribute(InstLevelAttribute()); + * ``` + * + * To check whether the attribute has been set: + * ``` + * n.hasAttribute(InstLevelAttribute()); + * ``` + * + * To separate Attributes of the same type in the same table, each of the + * structures `struct InstLevelAttributeId {};` is given a different unique value + * at load time. An example is the empty struct InstLevelAttributeId. These + * should be unique for each Attribute. Then via some template messiness when + * InstLevelAttribute() is passed as the argument to getAttribute(...) the load + * time id is instantiated. + */ // ATTRIBUTE MANAGER =========================================================== /** |