Refactor and update copyright headers. (#6316)

1 files changed, 132 insertions, 133 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 95e91bb52..dd9a41146 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,136 +1,135 @@
-/*********************                                                        */
-/*! \file node_builder.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief A builder interface for Nodes.
- **
- ** A builder interface for Nodes.
- **
- ** The idea is to permit a flexible and efficient (in the common
- ** case) interface for building Nodes.  The general pattern of use is
- ** to create a NodeBuilder, set its kind, append children to it, then
- ** "extract" the resulting Node.  This resulting Node may be one that
- ** already exists (the NodeManager keeps a table of all Nodes in the
- ** system), or may be entirely new.
- **
- ** This implementation gets a bit hairy for a handful of reasons.  We
- ** want a user-supplied "in-line" buffer (probably on the stack, see
- ** below) to hold the children, but then the number of children must
- ** be known ahead of time.  Therefore, if this buffer is overrun, we
- ** need to heap-allocate a new buffer to hold the children.
- **
- ** Note that as children are added to a NodeBuilder, they are stored
- ** as raw pointers-to-NodeValue.  However, their reference counts are
- ** carefully maintained.
- **
- ** When the "in-line" buffer "d_inlineNv" is superceded by a
- ** heap-allocated buffer, we allocate the new buffer (a NodeValue
- ** large enough to hold more children), copy the elements to it, and
- ** mark d_inlineNv as having zero children.  We do this last bit so
- ** that we don't have to modify any child reference counts.  The new
- ** heap-allocated buffer "takes over" the reference counts of the old
- ** "in-line" buffer.  (If we didn't mark it as having zero children,
- ** the destructor may improperly decrement the children's reference
- ** counts.)
- **
- ** There are then four normal cases at the end of a NodeBuilder's
- ** life cycle:
- **
- **   0. We have a VARIABLE-kinded Node.  These are special (they have
- **      no children and are all distinct by definition).  They are
- **      really a subcase of 1(b), below.
- **   1. d_nv points to d_inlineNv: it is the backing store supplied
- **      by the user (or derived class).
- **      (a) The Node under construction already exists in the
- **          NodeManager's pool.
- **      (b) The Node under construction is NOT already in the
- **          NodeManager's pool.
- **   2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer
- **      that was heap-allocated by this NodeBuilder.
- **      (a) The Node under construction already exists in the
- **          NodeManager's pool.
- **      (b) The Node under construction is NOT already in the
- **          NodeManager's pool.
- **
- ** When a Node is extracted, we convert the NodeBuilder to a Node and
- ** make sure the reference counts are properly maintained.  That
- ** means we must ensure there are no reference-counting errors among
- ** the node's children, that the children aren't re-decremented on
- ** clear() or NodeBuilder destruction, and that the returned Node
- ** wraps a NodeValue with a reference count of 1.
- **
- **   0.    If a VARIABLE, treat similarly to 1(b), except that we
- **         know there are no children (no reference counts to reason
- **         about) and we don't keep VARIABLE-kinded Nodes in the
- **         NodeManager pool.
- **
- **   1(a). Reference-counts for all children in d_inlineNv must be
- **         decremented, and the NodeBuilder must be marked as "used"
- **         and the number of children set to zero so that we don't
- **         decrement them again on destruction.  The existing
- **         NodeManager pool entry is returned.
- **
- **   1(b). A new heap-allocated NodeValue must be constructed and all
- **         settings and children from d_inlineNv copied into it.
- **         This new NodeValue is put into the NodeManager's pool.
- **         The NodeBuilder is marked as "used" and the number of
- **         children in d_inlineNv set to zero so that we don't
- **         decrement child reference counts on destruction (the child
- **         reference counts have been "taken over" by the new
- **         NodeValue).  We return a Node wrapper for this new
- **         NodeValue, which increments its reference count.
- **
- **   2(a). Reference counts for all children in d_nv must be
- **         decremented.  The NodeBuilder is marked as "used" and the
- **         heap-allocated d_nv deleted.  d_nv is repointed to
- **         d_inlineNv so that destruction of the NodeBuilder doesn't
- **         cause any problems.  The existing NodeManager pool entry
- **         is returned.
- **
- **   2(b). The heap-allocated d_nv is "cropped" to the correct size
- **         (based on the number of children it _actually_ has).  d_nv
- **         is repointed to d_inlineNv so that destruction of the
- **         NodeBuilder doesn't cause any problems, and the (old)
- **         value it had is placed into the NodeManager's pool and
- **         returned in a Node wrapper.
- **
- ** NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
- ** temporary for the NodeValue in the NodeBuilder::operator Node()
- ** member function.  If we create a temporary (for example by writing
- ** Debug("builder") << Node(nv) << endl), the NodeValue will have its
- ** reference count incremented from zero to one, then decremented,
- ** which makes it eligible for collection before the builder has even
- ** returned it!  So this is a no-no.
- **
- ** There are also two cases when the NodeBuilder is clear()'ed:
- **
- **   1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
- **      backing store): all d_inlineNv children have their reference
- **      counts decremented, d_inlineNv.d_nchildren is set to zero,
- **      and its kind is set to UNDEFINED_KIND.
- **
- **   2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
- **      d_nv children have their reference counts decremented, d_nv
- **      is deallocated, and d_nv is set to &d_inlineNv.  d_inlineNv's
- **      kind is set to UNDEFINED_KIND.
- **
- ** ... destruction is similar:
- **
- **   1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
- **      backing store): all d_inlineNv children have their reference
- **      counts decremented.
- **
- **   2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
- **      d_nv children have their reference counts decremented, and
- **      d_nv is deallocated.
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Andres Noetzli, Dejan Jovanovic
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A builder interface for Nodes.
+ *
+ * The idea is to permit a flexible and efficient (in the common
+ * case) interface for building Nodes.  The general pattern of use is
+ * to create a NodeBuilder, set its kind, append children to it, then
+ * "extract" the resulting Node.  This resulting Node may be one that
+ * already exists (the NodeManager keeps a table of all Nodes in the
+ * system), or may be entirely new.
+ *
+ * This implementation gets a bit hairy for a handful of reasons.  We
+ * want a user-supplied "in-line" buffer (probably on the stack, see
+ * below) to hold the children, but then the number of children must
+ * be known ahead of time.  Therefore, if this buffer is overrun, we
+ * need to heap-allocate a new buffer to hold the children.
+ *
+ * Note that as children are added to a NodeBuilder, they are stored
+ * as raw pointers-to-NodeValue.  However, their reference counts are
+ * carefully maintained.
+ *
+ * When the "in-line" buffer "d_inlineNv" is superceded by a
+ * heap-allocated buffer, we allocate the new buffer (a NodeValue
+ * large enough to hold more children), copy the elements to it, and
+ * mark d_inlineNv as having zero children.  We do this last bit so
+ * that we don't have to modify any child reference counts.  The new
+ * heap-allocated buffer "takes over" the reference counts of the old
+ * "in-line" buffer.  (If we didn't mark it as having zero children,
+ * the destructor may improperly decrement the children's reference
+ * counts.)
+ *
+ * There are then four normal cases at the end of a NodeBuilder's
+ * life cycle:
+ *
+ *   0. We have a VARIABLE-kinded Node.  These are special (they have
+ *      no children and are all distinct by definition).  They are
+ *      really a subcase of 1(b), below.
+ *   1. d_nv points to d_inlineNv: it is the backing store supplied
+ *      by the user (or derived class).
+ *      (a) The Node under construction already exists in the
+ *          NodeManager's pool.
+ *      (b) The Node under construction is NOT already in the
+ *          NodeManager's pool.
+ *   2. d_nv does NOT point to d_inlineNv: it is a new, larger buffer
+ *      that was heap-allocated by this NodeBuilder.
+ *      (a) The Node under construction already exists in the
+ *          NodeManager's pool.
+ *      (b) The Node under construction is NOT already in the
+ *          NodeManager's pool.
+ *
+ * When a Node is extracted, we convert the NodeBuilder to a Node and
+ * make sure the reference counts are properly maintained.  That
+ * means we must ensure there are no reference-counting errors among
+ * the node's children, that the children aren't re-decremented on
+ * clear() or NodeBuilder destruction, and that the returned Node
+ * wraps a NodeValue with a reference count of 1.
+ *
+ *   0.    If a VARIABLE, treat similarly to 1(b), except that we
+ *         know there are no children (no reference counts to reason
+ *         about) and we don't keep VARIABLE-kinded Nodes in the
+ *         NodeManager pool.
+ *
+ *   1(a). Reference-counts for all children in d_inlineNv must be
+ *         decremented, and the NodeBuilder must be marked as "used"
+ *         and the number of children set to zero so that we don't
+ *         decrement them again on destruction.  The existing
+ *         NodeManager pool entry is returned.
+ *
+ *   1(b). A new heap-allocated NodeValue must be constructed and all
+ *         settings and children from d_inlineNv copied into it.
+ *         This new NodeValue is put into the NodeManager's pool.
+ *         The NodeBuilder is marked as "used" and the number of
+ *         children in d_inlineNv set to zero so that we don't
+ *         decrement child reference counts on destruction (the child
+ *         reference counts have been "taken over" by the new
+ *         NodeValue).  We return a Node wrapper for this new
+ *         NodeValue, which increments its reference count.
+ *
+ *   2(a). Reference counts for all children in d_nv must be
+ *         decremented.  The NodeBuilder is marked as "used" and the
+ *         heap-allocated d_nv deleted.  d_nv is repointed to
+ *         d_inlineNv so that destruction of the NodeBuilder doesn't
+ *         cause any problems.  The existing NodeManager pool entry
+ *         is returned.
+ *
+ *   2(b). The heap-allocated d_nv is "cropped" to the correct size
+ *         (based on the number of children it _actually_ has).  d_nv
+ *         is repointed to d_inlineNv so that destruction of the
+ *         NodeBuilder doesn't cause any problems, and the (old)
+ *         value it had is placed into the NodeManager's pool and
+ *         returned in a Node wrapper.
+ *
+ * NOTE IN 1(b) AND 2(b) THAT we can NOT create Node wrapper
+ * temporary for the NodeValue in the NodeBuilder::operator Node()
+ * member function.  If we create a temporary (for example by writing
+ * Debug("builder") << Node(nv) << endl), the NodeValue will have its
+ * reference count incremented from zero to one, then decremented,
+ * which makes it eligible for collection before the builder has even
+ * returned it!  So this is a no-no.
+ *
+ * There are also two cases when the NodeBuilder is clear()'ed:
+ *
+ *   1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
+ *      backing store): all d_inlineNv children have their reference
+ *      counts decremented, d_inlineNv.d_nchildren is set to zero,
+ *      and its kind is set to UNDEFINED_KIND.
+ *
+ *   2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
+ *      d_nv children have their reference counts decremented, d_nv
+ *      is deallocated, and d_nv is set to &d_inlineNv.  d_inlineNv's
+ *      kind is set to UNDEFINED_KIND.
+ *
+ * ... destruction is similar:
+ *
+ *   1. d_nv == &d_inlineNv (NodeBuilder using the user-supplied
+ *      backing store): all d_inlineNv children have their reference
+ *      counts decremented.
+ *
+ *   2. d_nv != &d_inlineNv (d_nv heap-allocated by NodeBuilder): all
+ *      d_nv children have their reference counts decremented, and
+ *      d_nv is deallocated.
+ */
 
 #include "cvc4_private.h"