Migrate some documentation about attributes (#5390)

From old wiki.

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 ===========================================================
 
 /**