diff options
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 265 |
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" |