diff options
99 files changed, 1208 insertions, 1562 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 463fe74df..53242f077 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -46,6 +46,7 @@ #include "expr/metakind.h" #include "expr/node.h" #include "expr/node_algorithm.h" +#include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/sequence.h" #include "expr/type_node.h" @@ -3960,7 +3961,7 @@ Term Grammar::purifySygusGTerm( if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED) { // it's an indexed operator so we should provide the op - NodeBuilder<> nb(term.d_node->getKind()); + NodeBuilder nb(term.d_node->getKind()); nb << term.d_node->getOperator(); nb.append(Term::termVectorToNodes(pchildren)); nret = nb.constructNode(); @@ -4348,7 +4349,7 @@ Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const const cvc5::Kind int_kind = extToIntKind(op.d_kind); std::vector<Node> echildren = Term::termVectorToNodes(children); - NodeBuilder<> nb(int_kind); + NodeBuilder nb(int_kind); nb << *op.d_node; nb.append(echildren); Node res = nb.constructNode(); @@ -5547,7 +5548,7 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts, Sort s = mkTupleSortHelper(sorts); Datatype dt = s.getDatatype(); - NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR)); + NodeBuilder nb(extToIntKind(APPLY_CONSTRUCTOR)); nb << *dt[0].getConstructorTerm().d_node; nb.append(args); Node res = nb.constructNode(); diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 3e8717986..1161d1b70 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -38,6 +38,7 @@ libcvc4_add_sources( node.h node_algorithm.cpp node_algorithm.h + node_builder.cpp node_builder.h node_manager.cpp node_manager.h diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index 59b870897..ce15c7ede 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -655,7 +655,7 @@ TypeNode DTypeConstructor::doParametricSubstitution( } } } - NodeBuilder<> nb(range.getKind()); + NodeBuilder nb(range.getKind()); for (size_t i = 0, csize = children.size(); i < csize; ++i) { nb << children[i]; diff --git a/src/expr/node.h b/src/expr/node.h index 29bfaa157..fb3cf1478 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -196,7 +196,6 @@ class NodeTemplate { friend class TypeNode; friend class NodeManager; - template <unsigned nchild_thresh> friend class NodeBuilder; friend class ::cvc5::expr::attr::AttributeManager; @@ -1291,7 +1290,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, } // otherwise compute - NodeBuilder<> nb(getKind()); + NodeBuilder nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator if(getOperator() == node) { @@ -1359,7 +1358,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, cache[*this] = *this; return *this; } else { - NodeBuilder<> nb(getKind()); + NodeBuilder nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator nb << getOperator().substitute(nodesBegin, nodesEnd, @@ -1421,7 +1420,7 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, cache[*this] = *this; return *this; } else { - NodeBuilder<> nb(getKind()); + NodeBuilder nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache); diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index bcf74a944..1fb1a5220 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -624,7 +624,7 @@ Node substituteCaptureAvoiding(TNode n, else if (it->second.isNull()) { // build node - NodeBuilder<> nb(curr.getKind()); + NodeBuilder nb(curr.getKind()); if (curr.getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp new file mode 100644 index 000000000..72b7dd4dc --- /dev/null +++ b/src/expr/node_builder.cpp @@ -0,0 +1,717 @@ +/********************* */ +/*! \file node_builder.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** 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. + **/ + +#include "expr/node_builder.h" + +#include <memory> + +namespace cvc5 { + +NodeBuilder::NodeBuilder() + : d_nv(&d_inlineNv), + d_nm(NodeManager::currentNM()), + d_nvMaxChildren(default_nchild_thresh) +{ + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_nchildren = 0; +} + +NodeBuilder::NodeBuilder(Kind k) + : d_nv(&d_inlineNv), + d_nm(NodeManager::currentNM()), + d_nvMaxChildren(default_nchild_thresh) +{ + Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND) + << "illegal Node-building kind"; + + d_inlineNv.d_id = 1; // have a kind already + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; +} + +NodeBuilder::NodeBuilder(NodeManager* nm) + : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh) +{ + d_inlineNv.d_id = 0; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); + d_inlineNv.d_nchildren = 0; +} + +NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) + : d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(default_nchild_thresh) +{ + Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND) + << "illegal Node-building kind"; + + d_inlineNv.d_id = 1; // have a kind already + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + d_inlineNv.d_nchildren = 0; +} + +NodeBuilder::NodeBuilder(const NodeBuilder& nb) + : d_nv(&d_inlineNv), d_nm(nb.d_nm), d_nvMaxChildren(default_nchild_thresh) +{ + d_inlineNv.d_id = nb.d_nv->d_id; + d_inlineNv.d_rc = 0; + d_inlineNv.d_kind = nb.d_nv->d_kind; + d_inlineNv.d_nchildren = 0; + + internalCopy(nb); +} + +NodeBuilder::~NodeBuilder() +{ + if (__builtin_expect((nvIsAllocated()), false)) + { + dealloc(); + } + else if (__builtin_expect((!isUsed()), false)) + { + decrRefCounts(); + } +} + +Kind NodeBuilder::getKind() const +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + return d_nv->getKind(); +} + +kind::MetaKind NodeBuilder::getMetaKind() const +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "The metakind of a NodeBuilder is undefined " + "until a Kind is set"; + return d_nv->getMetaKind(); +} + +unsigned NodeBuilder::getNumChildren() const +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "The number of children of a NodeBuilder is undefined " + "until a Kind is set"; + return d_nv->getNumChildren(); +} + +Node NodeBuilder::getOperator() const +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "NodeBuilder operator access is not permitted " + "until a Kind is set"; + Assert(getMetaKind() == kind::metakind::PARAMETERIZED) + << "NodeBuilder operator access is only permitted " + "on parameterized kinds, not `" + << getKind() << "'"; + return Node(d_nv->getOperator()); +} + +Node NodeBuilder::getChild(int i) const +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "NodeBuilder child access is not permitted " + "until a Kind is set"; + Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren()) + << "index out of range for NodeBuilder::getChild()"; + return Node(d_nv->getChild(i)); +} + +Node NodeBuilder::operator[](int i) const { return getChild(i); } + +void NodeBuilder::clear(Kind k) +{ + Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind"; + + if (__builtin_expect((nvIsAllocated()), false)) + { + dealloc(); + } + else if (__builtin_expect((!isUsed()), false)) + { + decrRefCounts(); + } + else + { + setUnused(); + } + + d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); + for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); + i != d_inlineNv.nv_end(); + ++i) + { + (*i)->dec(); + } + d_inlineNv.d_nchildren = 0; + // keep track of whether or not we hvae a kind already + d_inlineNv.d_id = (k == kind::UNDEFINED_KIND) ? 0 : 1; +} + +NodeBuilder& NodeBuilder::operator<<(const Kind& k) +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0) + << "can't redefine the Kind of a NodeBuilder"; + Assert(d_nv->d_id == 0) + << "internal inconsistency with NodeBuilder: d_id != 0"; + AssertArgument( + k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, + k, + "illegal node-building kind"); + // This test means: we didn't have a Kind at the beginning (on + // NodeBuilder construction or at the last clear()), but we do + // now. That means we appended a Kind with operator<<(Kind), + // which now (lazily) we'll collapse. + if (__builtin_expect((d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND), + false)) + { + Node n2 = operator Node(); + clear(); + append(n2); + } + else if (d_nv->d_nchildren == 0) + { + d_nv->d_id = 1; // remember that we had a kind from the start + } + d_nv->d_kind = expr::NodeValue::kindToDKind(k); + return *this; +} + +NodeBuilder& NodeBuilder::operator<<(TNode n) +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + // This test means: we didn't have a Kind at the beginning (on + // NodeBuilder construction or at the last clear()), but we do + // now. That means we appended a Kind with operator<<(Kind), + // which now (lazily) we'll collapse. + if (__builtin_expect((d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND), + false)) + { + Node n2 = operator Node(); + clear(); + append(n2); + } + return append(n); +} + +NodeBuilder& NodeBuilder::operator<<(TypeNode n) +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + // This test means: we didn't have a Kind at the beginning (on + // NodeBuilder construction or at the last clear()), but we do + // now. That means we appended a Kind with operator<<(Kind), + // which now (lazily) we'll collapse. + if (__builtin_expect((d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND), + false)) + { + Node n2 = operator Node(); + clear(); + append(n2); + } + return append(n); +} + +NodeBuilder& NodeBuilder::append(const std::vector<TypeNode>& children) +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + return append(children.begin(), children.end()); +} + +NodeBuilder& NodeBuilder::append(TNode n) +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node"; + if (n.getKind() == kind::BUILTIN) + { + return *this << NodeManager::operatorToKind(n); + } + allocateNvIfNecessaryForAppend(); + expr::NodeValue* nv = n.d_nv; + nv->inc(); + d_nv->d_children[d_nv->d_nchildren++] = nv; + Assert(d_nv->d_nchildren <= d_nvMaxChildren); + return *this; +} + +NodeBuilder& NodeBuilder::append(const TypeNode& typeNode) +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node"; + allocateNvIfNecessaryForAppend(); + expr::NodeValue* nv = typeNode.d_nv; + nv->inc(); + d_nv->d_children[d_nv->d_nchildren++] = nv; + Assert(d_nv->d_nchildren <= d_nvMaxChildren); + return *this; +} + +void NodeBuilder::realloc(size_t toSize) +{ + AlwaysAssert(toSize > d_nvMaxChildren) + << "attempt to realloc() a NodeBuilder to a smaller/equal size!"; + Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN)) + << "attempt to realloc() a NodeBuilder to size " << toSize + << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")"; + + if (__builtin_expect((nvIsAllocated()), false)) + { + // Ensure d_nv is not modified on allocation failure + expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc( + d_nv, sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize)); + if (newBlock == NULL) + { + // In this case, d_nv was NOT freed. If we throw, the + // deallocation should occur on destruction of the NodeBuilder. + throw std::bad_alloc(); + } + d_nvMaxChildren = toSize; + Assert(d_nvMaxChildren == toSize); // overflow check + // Here, the copy (between two heap-allocated buffers) has already + // been done for us by the std::realloc(). + d_nv = newBlock; + } + else + { + // Ensure d_nv is not modified on allocation failure + expr::NodeValue* newBlock = (expr::NodeValue*)std::malloc( + sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * toSize)); + if (newBlock == NULL) + { + throw std::bad_alloc(); + } + d_nvMaxChildren = toSize; + Assert(d_nvMaxChildren == toSize); // overflow check + + d_nv = newBlock; + d_nv->d_id = d_inlineNv.d_id; + d_nv->d_rc = 0; + d_nv->d_kind = d_inlineNv.d_kind; + d_nv->d_nchildren = d_inlineNv.d_nchildren; + + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + d_nv->d_children); + + // ensure "inline" children don't get decremented in dtor + d_inlineNv.d_nchildren = 0; + } +} + +void NodeBuilder::dealloc() +{ + Assert(nvIsAllocated()) + << "Internal error: NodeBuilder: dealloc() called without a " + "private NodeBuilder-allocated buffer"; + + for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); + ++i) + { + (*i)->dec(); + } + + free(d_nv); + d_nv = &d_inlineNv; + d_nvMaxChildren = default_nchild_thresh; +} + +void NodeBuilder::decrRefCounts() +{ + Assert(!nvIsAllocated()) + << "Internal error: NodeBuilder: decrRefCounts() called with a " + "private NodeBuilder-allocated buffer"; + + for (expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); + i != d_inlineNv.nv_end(); + ++i) + { + (*i)->dec(); + } + + d_inlineNv.d_nchildren = 0; +} + +TypeNode NodeBuilder::constructTypeNode() { return TypeNode(constructNV()); } + +Node NodeBuilder::constructNode() +{ + Node n(constructNV()); + maybeCheckType(n); + return n; +} + +Node* NodeBuilder::constructNodePtr() +{ + std::unique_ptr<Node> np(new Node(constructNV())); + maybeCheckType(*np.get()); + return np.release(); +} + +NodeBuilder::operator Node() { return constructNode(); } + +NodeBuilder::operator TypeNode() { return constructTypeNode(); } + +expr::NodeValue* NodeBuilder::constructNV() +{ + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "Can't make an expression of an undefined kind!"; + + // NOTE: The comments in this function refer to the cases in the + // file comments at the top of this file. + + // Case 0: If a VARIABLE + if (getMetaKind() == kind::metakind::VARIABLE + || getMetaKind() == kind::metakind::NULLARY_OPERATOR) + { + /* 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. */ + + Assert(!nvIsAllocated()) + << "internal NodeBuilder error: " + "VARIABLE-kinded NodeBuilder is heap-allocated !?"; + Assert(d_inlineNv.d_nchildren == 0) + << "improperly-formed VARIABLE-kinded NodeBuilder: " + "no children permitted"; + + // we have to copy the inline NodeValue out + expr::NodeValue* nv = + (expr::NodeValue*)std::malloc(sizeof(expr::NodeValue)); + if (nv == NULL) + { + throw std::bad_alloc(); + } + // there are no children, so we don't have to worry about + // reference counts in this case. + nv->d_nchildren = 0; + nv->d_kind = d_nv->d_kind; + nv->d_id = d_nm->next_id++; // FIXME multithreading + nv->d_rc = 0; + setUsed(); + if (Debug.isOn("gc")) + { + Debug("gc") << "creating node value " << nv << " [" << nv->d_id << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } + return nv; + } + + // check that there are the right # of children for this kind + Assert(getMetaKind() != kind::metakind::CONSTANT) + << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"; + Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind())) + << "Nodes with kind " << getKind() << " must have at least " + << kind::metakind::getMinArityForKind(getKind()) + << " children (the one under " + "construction has " + << getNumChildren() << ")"; + Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind())) + << "Nodes with kind " << getKind() << " must have at most " + << kind::metakind::getMaxArityForKind(getKind()) + << " children (the one under " + "construction has " + << getNumChildren() << ")"; + + // Implementation differs depending on whether the NodeValue was + // malloc'ed or not and whether or not it's in the already-been-seen + // NodeManager pool of Nodes. See implementation notes at the top + // of this file. + + if (__builtin_expect((!nvIsAllocated()), true)) + { + /** Case 1. d_nv points to d_inlineNv: it is the backing store + ** allocated "inline" in this NodeBuilder. **/ + + // Lookup the expression value in the pool we already have + expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); + // If something else is there, we reuse it + if (poolNv != NULL) + { + /* Subcase (a): The Node under construction already exists in + * the NodeManager's 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. + */ + decrRefCounts(); + d_inlineNv.d_nchildren = 0; + setUsed(); + return poolNv; + } + else + { + /* Subcase (b): The Node under construction is NOT already in + * the NodeManager's pool. */ + + /* 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. */ + + // create the canonical expression value for this node + expr::NodeValue* nv = (expr::NodeValue*)std::malloc( + sizeof(expr::NodeValue) + + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren)); + if (nv == NULL) + { + throw std::bad_alloc(); + } + nv->d_nchildren = d_inlineNv.d_nchildren; + nv->d_kind = d_inlineNv.d_kind; + nv->d_id = d_nm->next_id++; // FIXME multithreading + nv->d_rc = 0; + + std::copy(d_inlineNv.d_children, + d_inlineNv.d_children + d_inlineNv.d_nchildren, + nv->d_children); + + d_inlineNv.d_nchildren = 0; + setUsed(); + + // poolNv = nv; + d_nm->poolInsert(nv); + if (Debug.isOn("gc")) + { + Debug("gc") << "creating node value " << nv << " [" << nv->d_id + << "]: "; + nv->printAst(Debug("gc")); + Debug("gc") << std::endl; + } + return nv; + } + } + else + { + /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger + ** buffer that was heap-allocated by this NodeBuilder. **/ + + // Lookup the expression value in the pool we already have (with insert) + expr::NodeValue* poolNv = d_nm->poolLookup(d_nv); + // If something else is there, we reuse it + if (poolNv != NULL) + { + /* Subcase (a): The Node under construction already exists in + * the NodeManager's pool. */ + + /* 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. */ + + dealloc(); + setUsed(); + return poolNv; + } + else + { + /* Subcase (b) The Node under construction is NOT already in the + * NodeManager's pool. */ + + /* 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. */ + + crop(); + expr::NodeValue* nv = d_nv; + nv->d_id = d_nm->next_id++; // FIXME multithreading + d_nv = &d_inlineNv; + d_nvMaxChildren = default_nchild_thresh; + setUsed(); + + // poolNv = nv; + d_nm->poolInsert(nv); + Debug("gc") << "creating node value " << nv << " [" << nv->d_id + << "]: " << *nv << "\n"; + return nv; + } + } +} + +void NodeBuilder::internalCopy(const NodeBuilder& nb) +{ + if (nb.isUsed()) + { + setUsed(); + return; + } + + bool realloced CVC4_UNUSED = false; + if (nb.d_nvMaxChildren > d_nvMaxChildren) + { + realloced = true; + realloc(nb.d_nvMaxChildren); + } + + Assert(nb.d_nvMaxChildren <= d_nvMaxChildren); + Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin()); + Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren) + << "realloced:" << (realloced ? "true" : "false") + << ", d_nvMax:" << d_nvMaxChildren + << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin() + << ", nc:" << nb.d_nv->getNumChildren(); + std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin()); + + d_nv->d_nchildren = nb.d_nv->d_nchildren; + + for (expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); + ++i) + { + (*i)->inc(); + } +} + +#ifdef CVC4_DEBUG +inline void NodeBuilder::maybeCheckType(const TNode n) const +{ + /* force an immediate type check, if early type checking is + enabled and the current node isn't a variable or constant */ + kind::MetaKind mk = n.getMetaKind(); + if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR + && mk != kind::metakind::CONSTANT) + { + d_nm->getType(n, true); + } +} +#endif /* CVC4_DEBUG */ + +bool NodeBuilder::isUsed() const +{ + return __builtin_expect((d_nv == NULL), false); +} + +void NodeBuilder::setUsed() +{ + Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!"; + Assert(d_inlineNv.d_nchildren == 0 + && d_nvMaxChildren == default_nchild_thresh) + << "Internal error: bad `inline' state in NodeBuilder!"; + d_nv = NULL; +} + +void NodeBuilder::setUnused() +{ + Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!"; + Assert(d_inlineNv.d_nchildren == 0 + && d_nvMaxChildren == default_nchild_thresh) + << "Internal error: bad `inline' state in NodeBuilder!"; + d_nv = &d_inlineNv; +} + +bool NodeBuilder::nvIsAllocated() const +{ + return __builtin_expect((d_nv != &d_inlineNv), false) + && __builtin_expect((d_nv != NULL), true); +} + +bool NodeBuilder::nvNeedsToBeAllocated() const +{ + return __builtin_expect((d_nv->d_nchildren == d_nvMaxChildren), false); +} + +void NodeBuilder::realloc() +{ + size_t newSize = 2 * size_t(d_nvMaxChildren); + size_t hardLimit = expr::NodeValue::MAX_CHILDREN; + realloc(__builtin_expect((newSize > hardLimit), false) ? hardLimit : newSize); +} + +void NodeBuilder::allocateNvIfNecessaryForAppend() +{ + if (__builtin_expect((nvNeedsToBeAllocated()), false)) + { + realloc(); + } +} + +void NodeBuilder::crop() +{ + if (__builtin_expect((nvIsAllocated()), false) + && __builtin_expect((d_nvMaxChildren > d_nv->d_nchildren), true)) + { + // Ensure d_nv is not modified on allocation failure + expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc( + d_nv, + sizeof(expr::NodeValue) + + (sizeof(expr::NodeValue*) * d_nv->d_nchildren)); + if (newBlock == NULL) + { + // In this case, d_nv was NOT freed. If we throw, the + // deallocation should occur on destruction of the + // NodeBuilder. + throw std::bad_alloc(); + } + d_nv = newBlock; + d_nvMaxChildren = d_nv->d_nchildren; + } +} + +NodeBuilder& NodeBuilder::collapseTo(Kind k) +{ + AssertArgument( + k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, + k, + "illegal collapsing kind"); + + if (getKind() != k) + { + Node n = operator Node(); + clear(); + d_nv->d_kind = expr::NodeValue::kindToDKind(k); + d_nv->d_id = 1; // have a kind already + return append(n); + } + return *this; +} + +std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb) +{ + return out << *nb.d_nv; +} + +} // namespace cvc5 diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index eaf5b040d..218a08766 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -102,7 +102,7 @@ ** 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() + ** 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, @@ -130,413 +130,70 @@ ** 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. - ** - ** Regarding the backing store (typically on the stack): the file - ** below provides the template: - ** - ** template < unsigned nchild_thresh > class NodeBuilder; - ** - ** The default: - ** - ** NodeBuilder<> b; - ** - ** gives you a backing buffer with capacity for 10 children in - ** the same place as the NodeBuilder<> itself is allocated. You - ** can specify another size as a template parameter, but it must - ** be a compile-time constant. **/ #include "cvc4_private.h" /* strong dependency; make sure node is included first */ #include "expr/node.h" -#include "expr/type_node.h" #ifndef CVC4__NODE_BUILDER_H #define CVC4__NODE_BUILDER_H -#include <cstdlib> #include <iostream> -#include <memory> #include <vector> -namespace cvc5 { -static const unsigned default_nchild_thresh = 10; - -template <unsigned nchild_thresh> -class NodeBuilder; - -class NodeManager; -} // namespace cvc5 - #include "base/check.h" -#include "base/output.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" +#include "expr/type_node.h" namespace cvc5 { -// Sometimes it's useful for debugging to output a NodeBuilder that -// isn't yet a Node.. -template <unsigned nchild_thresh> -std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb); +class NodeManager; /** - * The main template NodeBuilder. + * The NodeBuilder. */ -template <unsigned nchild_thresh = default_nchild_thresh> class NodeBuilder { - /** - * An "in-line" stack-allocated buffer for use by the - * NodeBuilder. - */ - expr::NodeValue d_inlineNv; - /** - * Space for the children of the node being constructed. This is - * never accessed directly, but rather through - * d_inlineNv.d_children[i]. - */ - expr::NodeValue* d_inlineNvChildSpace[nchild_thresh]; - - /** - * A pointer to the "current" NodeValue buffer; either &d_inlineNv - * or a heap-allocated one if d_inlineNv wasn't big enough. - */ - expr::NodeValue* d_nv; - - /** The NodeManager at play */ - NodeManager* d_nm; - - /** - * The number of children allocated in d_nv. - */ - uint32_t d_nvMaxChildren; - - template <unsigned N> - void internalCopy(const NodeBuilder<N>& nb); - - /** - * Returns whether or not this NodeBuilder has been "used"---i.e., - * whether a Node has been extracted with operator Node(). - * Internally, this state is represented by d_nv pointing to NULL. - */ - inline bool isUsed() const { - return __builtin_expect( ( d_nv == NULL ), false ); - } - - /** - * Set this NodeBuilder to the `used' state. - */ - inline void setUsed() { - Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!"; - Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh) - << "Internal error: bad `inline' state in NodeBuilder!"; - d_nv = NULL; - } - - /** - * Set this NodeBuilder to the `unused' state. Should only be done - * from clear(). - */ - inline void setUnused() { - Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!"; - Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh) - << "Internal error: bad `inline' state in NodeBuilder!"; - d_nv = &d_inlineNv; - } - - /** - * Returns true if d_nv is *not* the "in-line" one (it was - * heap-allocated by this class). - */ - inline bool nvIsAllocated() const { - return __builtin_expect( ( d_nv != &d_inlineNv ), false ) && __builtin_expect(( d_nv != NULL ), true ); - } - - /** - * Returns true if adding a child requires (re)allocation of d_nv - * first. - */ - inline bool nvNeedsToBeAllocated() const { - return __builtin_expect( ( d_nv->d_nchildren == d_nvMaxChildren ), false ); - } - - /** - * (Re)allocate d_nv using a default grow factor. Ensure that child - * pointers are copied into the new buffer, and if the "inline" - * NodeValue is evacuated, make sure its children won't be - * double-decremented later (on destruction/clear). - */ - inline void realloc() - { - size_t newSize = 2 * size_t(d_nvMaxChildren); - size_t hardLimit = expr::NodeValue::MAX_CHILDREN; - realloc(__builtin_expect((newSize > hardLimit), false) ? hardLimit - : newSize); - } - - /** - * (Re)allocate d_nv to a specific size. Specify "copy" if the - * children should be copied; if they are, and if the "inline" - * NodeValue is evacuated, make sure its children won't be - * double-decremented later (on destruction/clear). - */ - void realloc(size_t toSize); - - /** - * If d_nv needs to be (re)allocated to add an additional child, do - * so using realloc(), which ensures child pointers are copied and - * that the reference counts of the "inline" NodeValue won't be - * double-decremented on destruction/clear. Otherwise, do nothing. - */ - inline void allocateNvIfNecessaryForAppend() { - if(__builtin_expect( ( nvNeedsToBeAllocated() ), false )) { - realloc(); - } - } - - /** - * Deallocate a d_nv that was heap-allocated by this class during - * grow operations. (Marks this NodeValue no longer allocated so - * that double-deallocations don't occur.) - * - * PRECONDITION: only call this when nvIsAllocated() == true. - * POSTCONDITION: !nvIsAllocated() - */ - void dealloc(); - - /** - * "Purge" the "inline" children. Decrement all their reference - * counts and set the number of children to zero. - * - * PRECONDITION: only call this when nvIsAllocated() == false. - * POSTCONDITION: d_inlineNv.d_nchildren == 0. - */ - void decrRefCounts(); - - /** - * Trim d_nv down to the size it needs to be for the number of - * children it has. Used when a Node is extracted from a - * NodeBuilder and we want the returned memory not to suffer from - * internal fragmentation. If d_nv was not heap-allocated by this - * class, or is already the right size, this function does nothing. - * - * @throws bad_alloc if the reallocation fails - */ - void crop() { - if(__builtin_expect( ( nvIsAllocated() ), false ) && - __builtin_expect( ( d_nvMaxChildren > d_nv->d_nchildren ), true )) { - // Ensure d_nv is not modified on allocation failure - expr::NodeValue* newBlock = (expr::NodeValue*) - std::realloc(d_nv, - sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); - if(newBlock == NULL) { - // In this case, d_nv was NOT freed. If we throw, the - // deallocation should occur on destruction of the - // NodeBuilder. - throw std::bad_alloc(); - } - d_nv = newBlock; - d_nvMaxChildren = d_nv->d_nchildren; - } - } - - // used by convenience node builders - NodeBuilder<nchild_thresh>& collapseTo(Kind k) { - AssertArgument(k != kind::UNDEFINED_KIND && - k != kind::NULL_EXPR && - k < kind::LAST_KIND, - k, "illegal collapsing kind"); - - if(getKind() != k) { - Node n = operator Node(); - clear(); - d_nv->d_kind = expr::NodeValue::kindToDKind(k); - d_nv->d_id = 1; // have a kind already - return append(n); - } - return *this; - } - -public: - - inline NodeBuilder() : - d_nv(&d_inlineNv), - d_nm(NodeManager::currentNM()), - d_nvMaxChildren(nchild_thresh) { - - d_inlineNv.d_id = 0; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); - d_inlineNv.d_nchildren = 0; - } - - inline NodeBuilder(Kind k) : - d_nv(&d_inlineNv), - d_nm(NodeManager::currentNM()), - d_nvMaxChildren(nchild_thresh) { - Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND) - << "illegal Node-building kind"; - - d_inlineNv.d_id = 1; // have a kind already - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - d_inlineNv.d_nchildren = 0; - } - - inline NodeBuilder(NodeManager* nm) : - d_nv(&d_inlineNv), - d_nm(nm), - d_nvMaxChildren(nchild_thresh) { + friend std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); - d_inlineNv.d_id = 0; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(kind::UNDEFINED_KIND); - d_inlineNv.d_nchildren = 0; - } - - inline NodeBuilder(NodeManager* nm, Kind k) : - d_nv(&d_inlineNv), - d_nm(nm), - d_nvMaxChildren(nchild_thresh) { - Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND) - << "illegal Node-building kind"; - - d_inlineNv.d_id = 1; // have a kind already - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - d_inlineNv.d_nchildren = 0; - } - - inline ~NodeBuilder() { - if(__builtin_expect( ( nvIsAllocated() ), false )) { - dealloc(); - } else if(__builtin_expect( ( !isUsed() ), false )) { - decrRefCounts(); - } - } + constexpr static size_t default_nchild_thresh = 10; - // These implementations are identical, but we need to have both of - // these because the templatized version isn't recognized as a - // generalization of a copy constructor (and a default copy - // constructor will be generated [?]) - inline NodeBuilder(const NodeBuilder& nb) : - d_nv(&d_inlineNv), - d_nm(nb.d_nm), - d_nvMaxChildren(nchild_thresh) { + public: + NodeBuilder(); + NodeBuilder(Kind k); + NodeBuilder(NodeManager* nm); + NodeBuilder(NodeManager* nm, Kind k); + NodeBuilder(const NodeBuilder& nb); - d_inlineNv.d_id = nb.d_nv->d_id; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = nb.d_nv->d_kind; - d_inlineNv.d_nchildren = 0; - - internalCopy(nb); - } - - // technically this is a conversion, not a copy - template <unsigned N> - inline NodeBuilder(const NodeBuilder<N>& nb) : - d_nv(&d_inlineNv), - d_nm(nb.d_nm), - d_nvMaxChildren(nchild_thresh) { - - d_inlineNv.d_id = nb.d_nv->d_id; - d_inlineNv.d_rc = 0; - d_inlineNv.d_kind = nb.d_nv->d_kind; - d_inlineNv.d_nchildren = 0; - - internalCopy(nb); - } - - typedef expr::NodeValue::iterator< NodeTemplate<true> > iterator; - typedef expr::NodeValue::iterator< NodeTemplate<true> > const_iterator; - - /** Get the begin-const-iterator of this Node-under-construction. */ - inline const_iterator begin() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "Iterators over NodeBuilder<> are undefined " - "until a Kind is set"; - return d_nv->begin< NodeTemplate<true> >(); - } - - /** Get the end-const-iterator of this Node-under-construction. */ - inline const_iterator end() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "Iterators over NodeBuilder<> are undefined " - "until a Kind is set"; - return d_nv->end< NodeTemplate<true> >(); - } + ~NodeBuilder(); /** Get the kind of this Node-under-construction. */ - inline Kind getKind() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - return d_nv->getKind(); - } + Kind getKind() const; /** Get the kind of this Node-under-construction. */ - inline kind::MetaKind getMetaKind() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "The metakind of a NodeBuilder<> is undefined " - "until a Kind is set"; - return d_nv->getMetaKind(); - } + kind::MetaKind getMetaKind() const; /** Get the current number of children of this Node-under-construction. */ - inline unsigned getNumChildren() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "The number of children of a NodeBuilder<> is undefined " - "until a Kind is set"; - return d_nv->getNumChildren(); - } + unsigned getNumChildren() const; /** * Access to the operator of this Node-under-construction. Only * allowed if this NodeBuilder is unused, and has a defined kind * that is of PARAMETERIZED metakind. */ - inline Node getOperator() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "NodeBuilder<> operator access is not permitted " - "until a Kind is set"; - Assert(getMetaKind() == kind::metakind::PARAMETERIZED) - << "NodeBuilder<> operator access is only permitted " - "on parameterized kinds, not `" - << getKind() << "'"; - return Node(d_nv->getOperator()); - } + Node getOperator() const; /** * Access to children of this Node-under-construction. Only allowed * if this NodeBuilder is unused and has a defined kind. */ - inline Node getChild(int i) const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "NodeBuilder<> child access is not permitted " - "until a Kind is set"; - Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren()) - << "index out of range for NodeBuilder::getChild()"; - return Node(d_nv->getChild(i)); - } + Node getChild(int i) const; /** Access to children of this Node-under-construction. */ - inline Node operator[](int i) const { - return getChild(i); - } + Node operator[](int i) const; /** * "Reset" this node builder (optionally setting a new kind for it), @@ -555,82 +212,28 @@ public: // "Stream" expression constructor syntax /** Set the Kind of this Node-under-construction. */ - inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0) - << "can't redefine the Kind of a NodeBuilder"; - Assert(d_nv->d_id == 0) - << "internal inconsistency with NodeBuilder: d_id != 0"; - AssertArgument(k != kind::UNDEFINED_KIND && - k != kind::NULL_EXPR && - k < kind::LAST_KIND, - k, "illegal node-building kind"); - // This test means: we didn't have a Kind at the beginning (on - // NodeBuilder construction or at the last clear()), but we do - // now. That means we appended a Kind with operator<<(Kind), - // which now (lazily) we'll collapse. - if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) { - Node n2 = operator Node(); - clear(); - append(n2); - } else if(d_nv->d_nchildren == 0) { - d_nv->d_id = 1; // remember that we had a kind from the start - } - d_nv->d_kind = expr::NodeValue::kindToDKind(k); - return *this; - } + NodeBuilder& operator<<(const Kind& k); /** * If this Node-under-construction has a Kind set, collapse it and * append the given Node as a child. Otherwise, simply append. */ - NodeBuilder<nchild_thresh>& operator<<(TNode n) { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - // This test means: we didn't have a Kind at the beginning (on - // NodeBuilder construction or at the last clear()), but we do - // now. That means we appended a Kind with operator<<(Kind), - // which now (lazily) we'll collapse. - if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) { - Node n2 = operator Node(); - clear(); - append(n2); - } - return append(n); - } + NodeBuilder& operator<<(TNode n); /** * If this Node-under-construction has a Kind set, collapse it and * append the given Node as a child. Otherwise, simply append. */ - NodeBuilder<nchild_thresh>& operator<<(TypeNode n) { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - // This test means: we didn't have a Kind at the beginning (on - // NodeBuilder construction or at the last clear()), but we do - // now. That means we appended a Kind with operator<<(Kind), - // which now (lazily) we'll collapse. - if(__builtin_expect( ( d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND ), false )) { - Node n2 = operator Node(); - clear(); - append(n2); - } - return append(n); - } + NodeBuilder& operator<<(TypeNode n); /** Append a sequence of children to this TypeNode-under-construction. */ - inline NodeBuilder<nchild_thresh>& - append(const std::vector<TypeNode>& children) { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - return append(children.begin(), children.end()); - } + NodeBuilder& append(const std::vector<TypeNode>& children); /** Append a sequence of children to this Node-under-construction. */ template <bool ref_count> - inline NodeBuilder<nchild_thresh>& - append(const std::vector<NodeTemplate<ref_count> >& children) { + inline NodeBuilder& append( + const std::vector<NodeTemplate<ref_count> >& children) + { Assert(!isUsed()) << "NodeBuilder is one-shot only; " "attempt to access it after conversion"; return append(children.begin(), children.end()); @@ -638,7 +241,8 @@ public: /** Append a sequence of children to this Node-under-construction. */ template <class Iterator> - NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) { + NodeBuilder& append(const Iterator& begin, const Iterator& end) + { Assert(!isUsed()) << "NodeBuilder is one-shot only; " "attempt to access it after conversion"; for(Iterator i = begin; i != end; ++i) { @@ -648,681 +252,158 @@ public: } /** Append a child to this Node-under-construction. */ - NodeBuilder<nchild_thresh>& append(TNode n) { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node"; - if(n.getKind() == kind::BUILTIN) { - return *this << NodeManager::operatorToKind(n); - } - allocateNvIfNecessaryForAppend(); - expr::NodeValue* nv = n.d_nv; - nv->inc(); - d_nv->d_children[d_nv->d_nchildren++] = nv; - Assert(d_nv->d_nchildren <= d_nvMaxChildren); - return *this; - } + NodeBuilder& append(TNode n); /** Append a child to this Node-under-construction. */ - NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node"; - allocateNvIfNecessaryForAppend(); - expr::NodeValue* nv = typeNode.d_nv; - nv->inc(); - d_nv->d_children[d_nv->d_nchildren++] = nv; - Assert(d_nv->d_nchildren <= d_nvMaxChildren); - return *this; - } - -private: - - /** Construct the node value out of the node builder */ - expr::NodeValue* constructNV(); - expr::NodeValue* constructNV() const; - -#ifdef CVC4_DEBUG - // Throws a TypeCheckingExceptionPrivate on a failure. - void maybeCheckType(const TNode n) const; -#else /* CVC4_DEBUG */ - // Do nothing if not in debug mode. - inline void maybeCheckType(const TNode n) const {} -#endif /* CVC4_DEBUG */ - -public: + NodeBuilder& append(const TypeNode& typeNode); /** Construct the Node out of the node builder */ Node constructNode(); - Node constructNode() const; /** Construct a Node on the heap out of the node builder */ Node* constructNodePtr(); - Node* constructNodePtr() const; /** Construction of the TypeNode out of the node builder */ TypeNode constructTypeNode(); - TypeNode constructTypeNode() const; // two versions, so we can support extraction from (const) // NodeBuilders which are temporaries appearing as rvalues operator Node(); - operator Node() const; // similarly for TypeNode operator TypeNode(); - operator TypeNode() const; - - NodeBuilder<nchild_thresh>& operator&=(TNode); - NodeBuilder<nchild_thresh>& operator|=(TNode); - NodeBuilder<nchild_thresh>& operator+=(TNode); - NodeBuilder<nchild_thresh>& operator-=(TNode); - NodeBuilder<nchild_thresh>& operator*=(TNode); - - // This is needed for copy constructors of different sizes to access - // private fields - template <unsigned N> - friend class NodeBuilder; - - template <unsigned N> - friend std::ostream& operator<<(std::ostream& out, const NodeBuilder<N>& nb); - -};/* class NodeBuilder<> */ - -} // namespace cvc5 - -// TODO: add templatized NodeTemplate<ref_count> to all above and -// below inlines for 'const [T]Node&' arguments? Technically a lot of -// time is spent in the TNode conversion and copy constructor, but -// this should be optimized into a simple pointer copy (?) -// TODO: double-check this. - -#include "expr/node.h" -#include "expr/node_manager.h" -#include "options/expr_options.h" - -namespace cvc5 { - -template <unsigned nchild_thresh> -void NodeBuilder<nchild_thresh>::clear(Kind k) { - Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind"; - - if(__builtin_expect( ( nvIsAllocated() ), false )) { - dealloc(); - } else if(__builtin_expect( ( !isUsed() ), false )) { - decrRefCounts(); - } else { - setUnused(); - } - - d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k); - for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); - i != d_inlineNv.nv_end(); - ++i) { - (*i)->dec(); - } - d_inlineNv.d_nchildren = 0; - // keep track of whether or not we hvae a kind already - d_inlineNv.d_id = (k == kind::UNDEFINED_KIND) ? 0 : 1; -} - -template <unsigned nchild_thresh> -void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { - AlwaysAssert(toSize > d_nvMaxChildren) - << "attempt to realloc() a NodeBuilder to a smaller/equal size!"; - Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN)) - << "attempt to realloc() a NodeBuilder to size " << toSize - << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")"; - - if(__builtin_expect( ( nvIsAllocated() ), false )) { - // Ensure d_nv is not modified on allocation failure - expr::NodeValue* newBlock = (expr::NodeValue*) - std::realloc(d_nv, sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * toSize )); - if(newBlock == NULL) { - // In this case, d_nv was NOT freed. If we throw, the - // deallocation should occur on destruction of the NodeBuilder. - throw std::bad_alloc(); - } - d_nvMaxChildren = toSize; - Assert(d_nvMaxChildren == toSize); // overflow check - // Here, the copy (between two heap-allocated buffers) has already - // been done for us by the std::realloc(). - d_nv = newBlock; - } else { - // Ensure d_nv is not modified on allocation failure - expr::NodeValue* newBlock = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * toSize )); - if(newBlock == NULL) { - throw std::bad_alloc(); - } - d_nvMaxChildren = toSize; - Assert(d_nvMaxChildren == toSize); // overflow check - - d_nv = newBlock; - d_nv->d_id = d_inlineNv.d_id; - d_nv->d_rc = 0; - d_nv->d_kind = d_inlineNv.d_kind; - d_nv->d_nchildren = d_inlineNv.d_nchildren; - - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + d_inlineNv.d_nchildren, - d_nv->d_children); - - // ensure "inline" children don't get decremented in dtor - d_inlineNv.d_nchildren = 0; - } -} - -template <unsigned nchild_thresh> -void NodeBuilder<nchild_thresh>::dealloc() { - Assert(nvIsAllocated()) - << "Internal error: NodeBuilder: dealloc() called without a " - "private NodeBuilder-allocated buffer"; - - for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); - i != d_nv->nv_end(); - ++i) { - (*i)->dec(); - } - - free(d_nv); - d_nv = &d_inlineNv; - d_nvMaxChildren = nchild_thresh; -} - -template <unsigned nchild_thresh> -void NodeBuilder<nchild_thresh>::decrRefCounts() { - Assert(!nvIsAllocated()) - << "Internal error: NodeBuilder: decrRefCounts() called with a " - "private NodeBuilder-allocated buffer"; - - for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); - i != d_inlineNv.nv_end(); - ++i) { - (*i)->dec(); - } - - d_inlineNv.d_nchildren = 0; -} - - -template <unsigned nchild_thresh> -TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() { - return TypeNode(constructNV()); -} - -template <unsigned nchild_thresh> -TypeNode NodeBuilder<nchild_thresh>::constructTypeNode() const { - return TypeNode(constructNV()); -} - -template <unsigned nchild_thresh> -Node NodeBuilder<nchild_thresh>::constructNode() { - Node n = Node(constructNV()); - maybeCheckType(n); - return n; -} - -template <unsigned nchild_thresh> -Node NodeBuilder<nchild_thresh>::constructNode() const { - Node n = Node(constructNV()); - maybeCheckType(n); - return n; -} - -template <unsigned nchild_thresh> -Node* NodeBuilder<nchild_thresh>::constructNodePtr() { - // maybeCheckType() can throw an exception. Make sure to call the destructor - // on the exception branch. - std::unique_ptr<Node> np(new Node(constructNV())); - maybeCheckType(*np.get()); - return np.release(); -} -template <unsigned nchild_thresh> -Node* NodeBuilder<nchild_thresh>::constructNodePtr() const { - std::unique_ptr<Node> np(new Node(constructNV())); - maybeCheckType(*np.get()); - return np.release(); -} + private: + void internalCopy(const NodeBuilder& nb); -template <unsigned nchild_thresh> -NodeBuilder<nchild_thresh>::operator Node() { - return constructNode(); -} - -template <unsigned nchild_thresh> -NodeBuilder<nchild_thresh>::operator Node() const { - return constructNode(); -} - -template <unsigned nchild_thresh> -NodeBuilder<nchild_thresh>::operator TypeNode() { - return constructTypeNode(); -} - -template <unsigned nchild_thresh> -NodeBuilder<nchild_thresh>::operator TypeNode() const { - return constructTypeNode(); -} - -template <unsigned nchild_thresh> -expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "Can't make an expression of an undefined kind!"; - - // NOTE: The comments in this function refer to the cases in the - // file comments at the top of this file. - - // Case 0: If a VARIABLE - if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) { - /* 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. */ - - Assert(!nvIsAllocated()) - << "internal NodeBuilder error: " - "VARIABLE-kinded NodeBuilder is heap-allocated !?"; - Assert(d_inlineNv.d_nchildren == 0) - << "improperly-formed VARIABLE-kinded NodeBuilder: " - "no children permitted"; - - // we have to copy the inline NodeValue out - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue)); - if(nv == NULL) { - throw std::bad_alloc(); - } - // there are no children, so we don't have to worry about - // reference counts in this case. - nv->d_nchildren = 0; - nv->d_kind = d_nv->d_kind; - nv->d_id = d_nm->next_id++;// FIXME multithreading - nv->d_rc = 0; - setUsed(); - if(Debug.isOn("gc")) { - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: "; - nv->printAst(Debug("gc")); - Debug("gc") << std::endl; - } - return nv; - } - - // check that there are the right # of children for this kind - Assert(getMetaKind() != kind::metakind::CONSTANT) - << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"; - Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind())) - << "Nodes with kind " << getKind() << " must have at least " - << kind::metakind::getMinArityForKind(getKind()) - << " children (the one under " - "construction has " - << getNumChildren() << ")"; - Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind())) - << "Nodes with kind " << getKind() << " must have at most " - << kind::metakind::getMaxArityForKind(getKind()) - << " children (the one under " - "construction has " - << getNumChildren() << ")"; - - // Implementation differs depending on whether the NodeValue was - // malloc'ed or not and whether or not it's in the already-been-seen - // NodeManager pool of Nodes. See implementation notes at the top - // of this file. - - if(__builtin_expect( ( ! nvIsAllocated() ), true )) { - /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** allocated "inline" in this NodeBuilder. **/ - - // Lookup the expression value in the pool we already have - expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv); - // If something else is there, we reuse it - if(poolNv != NULL) { - /* Subcase (a): The Node under construction already exists in - * the NodeManager's 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. - */ - decrRefCounts(); - d_inlineNv.d_nchildren = 0; - setUsed(); - return poolNv; - } else { - /* Subcase (b): The Node under construction is NOT already in - * the NodeManager's pool. */ - - /* 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. */ - - // create the canonical expression value for this node - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); - if(nv == NULL) { - throw std::bad_alloc(); - } - nv->d_nchildren = d_inlineNv.d_nchildren; - nv->d_kind = d_inlineNv.d_kind; - nv->d_id = d_nm->next_id++;// FIXME multithreading - nv->d_rc = 0; - - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + d_inlineNv.d_nchildren, - nv->d_children); - - d_inlineNv.d_nchildren = 0; - setUsed(); - - //poolNv = nv; - d_nm->poolInsert(nv); - if(Debug.isOn("gc")) { - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: "; - nv->printAst(Debug("gc")); - Debug("gc") << std::endl; - } - return nv; - } - } else { - /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger - ** buffer that was heap-allocated by this NodeBuilder. **/ - - // Lookup the expression value in the pool we already have (with insert) - expr::NodeValue* poolNv = d_nm->poolLookup(d_nv); - // If something else is there, we reuse it - if(poolNv != NULL) { - /* Subcase (a): The Node under construction already exists in - * the NodeManager's pool. */ - - /* 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. */ - - dealloc(); - setUsed(); - return poolNv; - } else { - /* Subcase (b) The Node under construction is NOT already in the - * NodeManager's pool. */ - - /* 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. */ - - crop(); - expr::NodeValue* nv = d_nv; - nv->d_id = d_nm->next_id++;// FIXME multithreading - d_nv = &d_inlineNv; - d_nvMaxChildren = nchild_thresh; - setUsed(); - - //poolNv = nv; - d_nm->poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return nv; - } - } -} - -// CONST VERSION OF NODE EXTRACTOR -template <unsigned nchild_thresh> -expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { - Assert(!isUsed()) << "NodeBuilder is one-shot only; " - "attempt to access it after conversion"; - Assert(getKind() != kind::UNDEFINED_KIND) - << "Can't make an expression of an undefined kind!"; - - // NOTE: The comments in this function refer to the cases in the - // file comments at the top of this file. - - // Case 0: If a VARIABLE - if(getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR) { - /* 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. */ - - Assert(!nvIsAllocated()) - << "internal NodeBuilder error: " - "VARIABLE-kinded NodeBuilder is heap-allocated !?"; - Assert(d_inlineNv.d_nchildren == 0) - << "improperly-formed VARIABLE-kinded NodeBuilder: " - "no children permitted"; - - // we have to copy the inline NodeValue out - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue)); - if(nv == NULL) { - throw std::bad_alloc(); - } - // there are no children, so we don't have to worry about - // reference counts in this case. - nv->d_nchildren = 0; - nv->d_kind = d_nv->d_kind; - nv->d_id = d_nm->next_id++;// FIXME multithreading - nv->d_rc = 0; - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return nv; - } - - // check that there are the right # of children for this kind - Assert(getMetaKind() != kind::metakind::CONSTANT) - << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"; - Assert(getNumChildren() >= kind::metakind::getMinArityForKind(getKind())) - << "Nodes with kind " << getKind() << " must have at least " - << kind::metakind::getMinArityForKind(getKind()) - << " children (the one under " - "construction has " - << getNumChildren() << ")"; - Assert(getNumChildren() <= kind::metakind::getMaxArityForKind(getKind())) - << "Nodes with kind " << getKind() << " must have at most " - << kind::metakind::getMaxArityForKind(getKind()) - << " children (the one under " - "construction has " - << getNumChildren() << ")"; - -#if 0 - // if the kind is PARAMETERIZED, check that the operator is correctly-kinded - Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED || - NodeManager::operatorToKind(getOperator()) == getKind()) << - "Attempted to construct a parameterized kind `"<< getKind() <<"' with " - "incorrectly-kinded operator `"<< getOperator().getKind() <<"'"; -#endif /* 0 */ - - // Implementation differs depending on whether the NodeValue was - // malloc'ed or not and whether or not it's in the already-been-seen - // NodeManager pool of Nodes. See implementation notes at the top - // of this file. - - if(__builtin_expect( ( ! nvIsAllocated() ), true )) { - /** Case 1. d_nv points to d_inlineNv: it is the backing store - ** allocated "inline" in this NodeBuilder. **/ - - // Lookup the expression value in the pool we already have - expr::NodeValue* poolNv = d_nm->poolLookup(const_cast<expr::NodeValue*>(&d_inlineNv)); - // If something else is there, we reuse it - if(poolNv != NULL) { - /* Subcase (a): The Node under construction already exists in - * the NodeManager's pool. */ - - /* 1(a). The existing NodeManager pool entry is returned; we - * leave child reference counts alone and get them at - * NodeBuilder destruction time. */ - - return poolNv; - } else { - /* Subcase (b): The Node under construction is NOT already in - * the NodeManager's pool. */ - - /* 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 cannot be marked as "used", so we increment all - * child reference counts (which will be decremented to match on - * destruction of the NodeBuilder). We return a Node wrapper - * for this new NodeValue, which increments its reference - * count. */ - - // create the canonical expression value for this node - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); - if(nv == NULL) { - throw std::bad_alloc(); - } - nv->d_nchildren = d_inlineNv.d_nchildren; - nv->d_kind = d_inlineNv.d_kind; - nv->d_id = d_nm->next_id++;// FIXME multithreading - nv->d_rc = 0; + /** + * Returns whether or not this NodeBuilder has been "used"---i.e., + * whether a Node has been extracted with operator Node(). + * Internally, this state is represented by d_nv pointing to NULL. + */ + bool isUsed() const; - std::copy(d_inlineNv.d_children, - d_inlineNv.d_children + d_inlineNv.d_nchildren, - nv->d_children); + /** + * Set this NodeBuilder to the `used' state. + */ + void setUsed(); - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - i != nv->nv_end(); - ++i) { - (*i)->inc(); - } + /** + * Set this NodeBuilder to the `unused' state. Should only be done + * from clear(). + */ + void setUnused(); - //poolNv = nv; - d_nm->poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return nv; - } - } else { - /** Case 2. d_nv does NOT point to d_inlineNv: it is a new, larger - ** buffer that was heap-allocated by this NodeBuilder. **/ + /** + * Returns true if d_nv is *not* the "in-line" one (it was + * heap-allocated by this class). + */ + bool nvIsAllocated() const; - // Lookup the expression value in the pool we already have (with insert) - expr::NodeValue* poolNv = d_nm->poolLookup(d_nv); - // If something else is there, we reuse it - if(poolNv != NULL) { - /* Subcase (a): The Node under construction already exists in - * the NodeManager's pool. */ + /** + * Returns true if adding a child requires (re)allocation of d_nv + * first. + */ + bool nvNeedsToBeAllocated() const; - /* 2(a). The existing NodeManager pool entry is returned; we - * leave child reference counts alone and get them at - * NodeBuilder destruction time. */ + /** + * (Re)allocate d_nv using a default grow factor. Ensure that child + * pointers are copied into the new buffer, and if the "inline" + * NodeValue is evacuated, make sure its children won't be + * double-decremented later (on destruction/clear). + */ + void realloc(); - return poolNv; - } else { - /* Subcase (b) The Node under construction is NOT already in the - * NodeManager's pool. */ + /** + * (Re)allocate d_nv to a specific size. Specify "copy" if the + * children should be copied; if they are, and if the "inline" + * NodeValue is evacuated, make sure its children won't be + * double-decremented later (on destruction/clear). + */ + void realloc(size_t toSize); - /* 2(b). The heap-allocated d_nv cannot be "cropped" to the - * correct size; we create a copy, increment child reference - * counts, place this copy into the NodeManager pool, and return - * a Node wrapper around it. The child reference counts will be - * decremented to match at NodeBuilder destruction time. */ + /** + * If d_nv needs to be (re)allocated to add an additional child, do + * so using realloc(), which ensures child pointers are copied and + * that the reference counts of the "inline" NodeValue won't be + * double-decremented on destruction/clear. Otherwise, do nothing. + */ + void allocateNvIfNecessaryForAppend(); - // create the canonical expression value for this node - expr::NodeValue* nv = (expr::NodeValue*) - std::malloc(sizeof(expr::NodeValue) + - ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); - if(nv == NULL) { - throw std::bad_alloc(); - } - nv->d_nchildren = d_nv->d_nchildren; - nv->d_kind = d_nv->d_kind; - nv->d_id = d_nm->next_id++;// FIXME multithreading - nv->d_rc = 0; + /** + * Deallocate a d_nv that was heap-allocated by this class during + * grow operations. (Marks this NodeValue no longer allocated so + * that double-deallocations don't occur.) + * + * PRECONDITION: only call this when nvIsAllocated() == true. + * POSTCONDITION: !nvIsAllocated() + */ + void dealloc(); - std::copy(d_nv->d_children, - d_nv->d_children + d_nv->d_nchildren, - nv->d_children); + /** + * "Purge" the "inline" children. Decrement all their reference + * counts and set the number of children to zero. + * + * PRECONDITION: only call this when nvIsAllocated() == false. + * POSTCONDITION: d_inlineNv.d_nchildren == 0. + */ + void decrRefCounts(); - for(expr::NodeValue::nv_iterator i = nv->nv_begin(); - i != nv->nv_end(); - ++i) { - (*i)->inc(); - } + /** + * Trim d_nv down to the size it needs to be for the number of + * children it has. Used when a Node is extracted from a + * NodeBuilder and we want the returned memory not to suffer from + * internal fragmentation. If d_nv was not heap-allocated by this + * class, or is already the right size, this function does nothing. + * + * @throws bad_alloc if the reallocation fails + */ + void crop(); - //poolNv = nv; - d_nm->poolInsert(nv); - Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << *nv << "\n"; - return nv; - } - } -} + /** Construct the node value out of the node builder */ + expr::NodeValue* constructNV(); -template <unsigned nchild_thresh> -template <unsigned N> -void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { - if(nb.isUsed()) { - setUsed(); - return; - } +#ifdef CVC4_DEBUG + // Throws a TypeCheckingExceptionPrivate on a failure. + void maybeCheckType(const TNode n) const; +#else /* CVC4_DEBUG */ + // Do nothing if not in debug mode. + inline void maybeCheckType(const TNode n) const {} +#endif /* CVC4_DEBUG */ - bool realloced CVC4_UNUSED = false; - if(nb.d_nvMaxChildren > d_nvMaxChildren) { - realloced = true; - realloc(nb.d_nvMaxChildren); - } + // used by convenience node builders + NodeBuilder& collapseTo(Kind k); - Assert(nb.d_nvMaxChildren <= d_nvMaxChildren); - Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin()); - Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren) - << "realloced:" << (realloced ? "true" : "false") - << ", d_nvMax:" << d_nvMaxChildren - << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin() - << ", nc:" << nb.d_nv->getNumChildren(); - std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin()); + /** + * An "in-line" stack-allocated buffer for use by the + * NodeBuilder. + */ + expr::NodeValue d_inlineNv; + /** + * Space for the children of the node being constructed. This is + * never accessed directly, but rather through + * d_inlineNv.d_children[i]. + */ + expr::NodeValue* d_inlineNvChildSpace[default_nchild_thresh]; - d_nv->d_nchildren = nb.d_nv->d_nchildren; + /** + * A pointer to the "current" NodeValue buffer; either &d_inlineNv + * or a heap-allocated one if d_inlineNv wasn't big enough. + */ + expr::NodeValue* d_nv; - for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); - i != d_nv->nv_end(); - ++i) { - (*i)->inc(); - } -} + /** The NodeManager at play */ + NodeManager* d_nm; -#ifdef CVC4_DEBUG -template <unsigned nchild_thresh> -inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const -{ - /* force an immediate type check, if early type checking is - enabled and the current node isn't a variable or constant */ - kind::MetaKind mk = n.getMetaKind(); - if (mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR - && mk != kind::metakind::CONSTANT) - { - d_nm->getType(n, true); - } -} -#endif /* CVC4_DEBUG */ + /** + * The number of children allocated in d_nv. + */ + uint32_t d_nvMaxChildren; +}; /* class NodeBuilder */ -template <unsigned nchild_thresh> -std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb) { - return out << *nb.d_nv; -} +// Sometimes it's useful for debugging to output a NodeBuilder that +// isn't yet a Node.. +std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb); } // namespace cvc5 diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6d2d150f5..4b95e08df 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -504,7 +504,7 @@ TypeNode NodeManager::getType(TNode n, bool check) } Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) { - Node n = NodeBuilder<0>(this, kind::SKOLEM); + Node n = NodeBuilder(this, kind::SKOLEM); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); if((flags & SKOLEM_EXACT_NAME) == 0) { @@ -834,8 +834,8 @@ size_t NodeManager::poolSize() const{ } TypeNode NodeManager::mkSort(uint32_t flags) { - NodeBuilder<1> nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder(this, kind::SORT_TAG); nb << sortTag; TypeNode tn = nb.constructTypeNode(); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { @@ -845,8 +845,8 @@ TypeNode NodeManager::mkSort(uint32_t flags) { } TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { - NodeBuilder<1> nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder(this, kind::SORT_TAG); nb << sortTag; TypeNode tn = nb.constructTypeNode(); setAttribute(tn, expr::VarNameAttr(), name); @@ -870,7 +870,7 @@ TypeNode NodeManager::mkSort(TypeNode constructor, Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size()) << "arity mismatch in application of sort constructor"; - NodeBuilder<> nb(this, kind::SORT_TYPE); + NodeBuilder nb(this, kind::SORT_TYPE); Node sortTag = Node(constructor.d_nv->d_children[0]); nb << sortTag; nb.append(children); @@ -887,8 +887,8 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, uint32_t flags) { Assert(arity > 0); - NodeBuilder<> nb(this, kind::SORT_TYPE); - Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); + NodeBuilder nb(this, kind::SORT_TYPE); + Node sortTag = NodeBuilder(this, kind::SORT_TAG); nb << sortTag; TypeNode type = nb.constructTypeNode(); setAttribute(type, expr::VarNameAttr(), name); @@ -901,7 +901,7 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::VARIABLE); + Node n = NodeBuilder(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); @@ -913,7 +913,7 @@ Node NodeManager::mkVar(const std::string& name, const TypeNode& type) Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); + Node* n = NodeBuilder(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); setAttribute(*n, expr::VarNameAttr(), name); @@ -1044,7 +1044,7 @@ Node NodeManager::mkChain(Kind kind, const std::vector<Node>& children) Node NodeManager::mkVar(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::VARIABLE); + Node n = NodeBuilder(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { @@ -1055,7 +1055,7 @@ Node NodeManager::mkVar(const TypeNode& type) Node* NodeManager::mkVarPtr(const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); + Node* n = NodeBuilder(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { @@ -1065,28 +1065,28 @@ Node* NodeManager::mkVarPtr(const TypeNode& type) } Node NodeManager::mkBoundVar(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE); + Node n = NodeBuilder(this, kind::BOUND_VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); return n; } Node* NodeManager::mkBoundVarPtr(const TypeNode& type) { - Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr(); + Node* n = NodeBuilder(this, kind::BOUND_VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); return n; } Node NodeManager::mkInstConstant(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::INST_CONSTANT); + Node n = NodeBuilder(this, kind::INST_CONSTANT); n.setAttribute(TypeAttr(), type); n.setAttribute(TypeCheckedAttr(), true); return n; } Node NodeManager::mkBooleanTermVariable() { - Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE); + Node n = NodeBuilder(this, kind::BOOLEAN_TERM_VARIABLE); n.setAttribute(TypeAttr(), booleanType()); n.setAttribute(TypeCheckedAttr(), true); return n; @@ -1095,7 +1095,7 @@ Node NodeManager::mkBooleanTermVariable() { Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ - Node n = NodeBuilder<0>(this, k).constructNode(); + Node n = NodeBuilder(this, k).constructNode(); setAttribute(n, TypeAttr(), type); //setAttribute(n, TypeCheckedAttr(), true); d_unique_vars[k][type] = n; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 857bcc25f..a72eada23 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -88,7 +88,6 @@ class NodeManager friend class expr::NodeValue; friend class expr::TypeChecker; - template <unsigned nchild_thresh> friend class NodeBuilder; friend class NodeManagerScope; @@ -1239,67 +1238,67 @@ inline Kind NodeManager::operatorToKind(TNode n) { } inline Node NodeManager::mkNode(Kind kind, TNode child1) { - NodeBuilder<1> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) { - NodeBuilder<1> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1; return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) { - NodeBuilder<2> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) { - NodeBuilder<2> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2; return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { - NodeBuilder<3> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3) { - NodeBuilder<3> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3; return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<4> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<4> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4; return nb.constructNodePtr(); } inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<5> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; return nb.constructNode(); } inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<5> nb(this, kind); + NodeBuilder nb(this, kind); nb << child1 << child2 << child3 << child4 << child5; return nb.constructNodePtr(); } @@ -1309,7 +1308,7 @@ template <bool ref_count> inline Node NodeManager::mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, kind); + NodeBuilder nb(this, kind); nb.append(children); return nb.constructNode(); } @@ -1346,14 +1345,14 @@ template <bool ref_count> inline Node* NodeManager::mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, kind); + NodeBuilder nb(this, kind); nb.append(children); return nb.constructNodePtr(); } // for operators inline Node NodeManager::mkNode(TNode opNode) { - NodeBuilder<1> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1361,7 +1360,7 @@ inline Node NodeManager::mkNode(TNode opNode) { } inline Node* NodeManager::mkNodePtr(TNode opNode) { - NodeBuilder<1> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1369,7 +1368,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode) { } inline Node NodeManager::mkNode(TNode opNode, TNode child1) { - NodeBuilder<2> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1378,7 +1377,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1) { } inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) { - NodeBuilder<2> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1387,7 +1386,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) { } inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { - NodeBuilder<3> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1396,7 +1395,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { } inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) { - NodeBuilder<3> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1406,7 +1405,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) { inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, TNode child3) { - NodeBuilder<4> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1416,7 +1415,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3) { - NodeBuilder<4> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1426,7 +1425,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<5> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1436,7 +1435,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4) { - NodeBuilder<5> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1446,7 +1445,7 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<6> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1456,7 +1455,7 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, TNode child4, TNode child5) { - NodeBuilder<6> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1469,7 +1468,7 @@ template <bool ref_count> inline Node NodeManager::mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1481,7 +1480,7 @@ template <bool ref_count> inline Node* NodeManager::mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children) { - NodeBuilder<> nb(this, operatorToKind(opNode)); + NodeBuilder nb(this, operatorToKind(opNode)); if(opNode.getKind() != kind::BUILTIN) { nb << opNode; } @@ -1491,23 +1490,24 @@ inline Node* NodeManager::mkNodePtr(TNode opNode, inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) { - return (NodeBuilder<1>(this, kind) << child1).constructTypeNode(); + return (NodeBuilder(this, kind) << child1).constructTypeNode(); } inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, TypeNode child2) { - return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode(); + return (NodeBuilder(this, kind) << child1 << child2).constructTypeNode(); } inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1, TypeNode child2, TypeNode child3) { - return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode(); + return (NodeBuilder(this, kind) << child1 << child2 << child3) + .constructTypeNode(); } // N-ary version for types inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) { - return NodeBuilder<>(this, kind).append(children).constructTypeNode(); + return NodeBuilder(this, kind).append(children).constructTypeNode(); } template <class T> diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 3815ea5be..3f4b7602e 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -36,7 +36,7 @@ namespace cvc5 { template <bool ref_count> class NodeTemplate; class TypeNode; -template <unsigned N> class NodeBuilder; +class NodeBuilder; class NodeManager; namespace expr { @@ -65,7 +65,6 @@ class NodeValue template <bool> friend class ::cvc5::NodeTemplate; friend class ::cvc5::TypeNode; - template <unsigned nchild_thresh> friend class ::cvc5::NodeBuilder; friend class ::cvc5::NodeManager; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index cbade1220..2dafe40da 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -39,7 +39,7 @@ TypeNode TypeNode::substitute(const TypeNode& type, } // otherwise compute - NodeBuilder<> nb(getKind()); + NodeBuilder nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator nb << TypeNode(d_nv->d_children[0]); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 98515be2a..f8cc5a44b 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -77,7 +77,6 @@ private: friend class NodeManager; - template <unsigned nchild_thresh> friend class NodeBuilder; /** @@ -797,7 +796,7 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, cache[*this] = *this; return *this; } else { - NodeBuilder<> nb(getKind()); + NodeBuilder nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator nb << TypeNode(d_nv->d_children[0]); diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index df8e93bc7..ac7707d16 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -356,7 +356,7 @@ void BoolToBV::rebuildNode(const TNode& n, Kind new_kind) { Kind k = n.getKind(); NodeManager* nm = NodeManager::currentNM(); - NodeBuilder<> builder(new_kind); + NodeBuilder builder(new_kind); Debug("bool-to-bv") << "BoolToBV::rebuildNode with " << n << " and new_kind = " << kindToString(new_kind) diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 7bd0e7715..6b8b7af2f 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -500,8 +500,8 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem( /* Flatten mult expression. */ n = RewriteRule<FlattenAssocCommut>::run<true>(n); /* Split operands into consts and non-consts */ - NodeBuilder<> nb_consts(NodeManager::currentNM(), k); - NodeBuilder<> nb_nonconsts(NodeManager::currentNM(), k); + NodeBuilder nb_consts(NodeManager::currentNM(), k); + NodeBuilder nb_nonconsts(NodeManager::currentNM(), k); for (const Node& nn : n) { Node nnrw = Rewriter::rewrite(nn); diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index 9f219e7a4..a8382974c 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -220,7 +220,7 @@ Node BVToBool::convertBvTerm(TNode node) default: Unhandled(); } - NodeBuilder<> builder(new_kind); + NodeBuilder builder(new_kind); for (unsigned i = 0; i < node.getNumChildren(); ++i) { builder << convertBvTerm(node[i]); @@ -254,7 +254,7 @@ Node BVToBool::liftNode(TNode current) } else { - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 510d35419..c5f24c15c 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -116,7 +116,7 @@ Node BVToInt::makeBinary(Node n) else if (numChildren > 0) { // current has children, but we do not binarize it - NodeBuilder<> builder(k); + NodeBuilder builder(k); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -220,7 +220,7 @@ Node BVToInt::eliminationPass(Node n) { // The main operator is replaced, and the children // are replaced with their eliminated counterparts. - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -886,7 +886,7 @@ Node BVToInt::reconstructNode(Node originalNode, // first, we adjust the children of the node as needed. // re-construct the term with the adjusted children. kind::Kind_t oldKind = originalNode.getKind(); - NodeBuilder<> builder(oldKind); + NodeBuilder builder(oldKind); if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << originalNode.getOperator(); diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index 307be46bf..60345992f 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -121,7 +121,7 @@ Node ForeignTheoryRewrite::reconstructNode(Node originalNode, } // re-build the node with the same kind and new children kind::Kind_t k = originalNode.getKind(); - NodeBuilder<> builder(k); + NodeBuilder builder(k); // special case for parameterized nodes if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index b1f8ad771..ef9b261b0 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -79,7 +79,7 @@ Node intToBVMakeBinary(TNode n, NodeMap& cache) } else { - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } @@ -186,7 +186,7 @@ Node intToBV(TNode n, NodeMap& cache) } } } - NodeBuilder<> builder(newKind); + NodeBuilder builder(newKind); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 7c246c3e1..f3c4d2e12 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -57,7 +57,7 @@ size_t removeFromConjunction(Node& n, || (sub.getKind() == kind::AND && (subremovals = removeFromConjunction(sub, toRemove)) > 0)) { - NodeBuilder<> b(kind::AND); + NodeBuilder b(kind::AND); b.append(n.begin(), j); if (subremovals > 0) { @@ -559,7 +559,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node sum; if (pos.getKind() == kind::AND) { - NodeBuilder<> sumb(kind::PLUS); + NodeBuilder sumb(kind::PLUS); for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { sumb << nm->mkNode( diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 028322c1e..5e572d1d8 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -37,7 +37,7 @@ PreprocessingPassResult StaticLearning::applyInternal( for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { - NodeBuilder<> learned(kind::AND); + NodeBuilder learned(kind::AND); learned << (*assertionsToPreprocess)[i]; d_preprocContext->getTheoryEngine()->ppStaticLearn( (*assertionsToPreprocess)[i], learned); diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index a3ad701a8..7826c207b 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -401,7 +401,7 @@ Node ITECompressor::compressBooleanITEs(Node toCompress) } } - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Node curr = toCompress; while (curr.getKind() == kind::ITE && (curr[1] == d_false || curr[2] == d_false) @@ -465,7 +465,7 @@ Node ITECompressor::compressTerm(Node toCompress) } } - NodeBuilder<> nb(toCompress.getKind()); + NodeBuilder nb(toCompress.getKind()); if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -504,7 +504,7 @@ Node ITECompressor::compressBoolean(Node toCompress) else { bool ta = ite::isTheoryAtom(toCompress); - NodeBuilder<> nb(toCompress.getKind()); + NodeBuilder nb(toCompress.getKind()); if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (toCompress.getOperator()); @@ -906,7 +906,7 @@ Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar) return d_replaceOverCache[p]; } - NodeBuilder<> builder(n.getKind()); + NodeBuilder builder(n.getKind()); if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << n.getOperator(); @@ -1207,7 +1207,7 @@ Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite) } else { - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); NodeVec::const_iterator it = intersection.begin(), end = intersection.end(); for (; it != end; ++it) { @@ -1332,7 +1332,7 @@ Node ITESimplifier::simpConstants(TNode simpContext, if (iteNode.getKind() == kind::ITE) { - NodeBuilder<> builder(kind::ITE); + NodeBuilder builder(kind::ITE); builder << iteNode[0]; unsigned i = 1; for (; i < iteNode.getNumChildren(); ++i) @@ -1428,7 +1428,7 @@ Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar) return simpVar; } - NodeBuilder<> builder(c.getKind()); + NodeBuilder builder(c.getKind()); if (c.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << c.getOperator(); @@ -1584,7 +1584,7 @@ Node ITESimplifier::simpITE(TNode assertion) if (stackHead.d_children_added) { // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -1731,7 +1731,7 @@ Node ITECareSimplifier::substitute(TNode e, return e; } - NodeBuilder<> builder(e.getKind()); + NodeBuilder builder(e.getKind()); if (e.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << e.getOperator(); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 1caea7bb7..10c84f582 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -76,7 +76,7 @@ bool CnfStream::assertClause(TNode node, SatClause& c) else { Assert(c.size() > 1); - NodeBuilder<> b(kind::OR); + NodeBuilder b(kind::OR); for (unsigned i = 0; i < c.size(); ++i) { b << getNode(c[i]); diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 07d072751..bfb14e2c4 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -18,6 +18,7 @@ #include "expr/node_algorithm.h" #include "options/base_options.h" +#include "options/expr_options.h" #include "options/language.h" #include "options/smt_options.h" #include "proof/proof_manager.h" diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index e00ed907f..c1daf9879 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -19,6 +19,7 @@ #include "base/configuration.h" #include "base/output.h" #include "lib/strtok_r.h" +#include "options/option_exception.h" #include "preprocessing/preprocessing_pass_registry.h" #include "smt/command.h" #include "smt/node_command.h" diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index 85a2732c9..59597b97f 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -294,7 +294,7 @@ TrustNode ExpandDefs::expandDefinitions( if (node.getNumChildren() > 0) { // cout << "cons : " << node << std::endl; - NodeBuilder<> nb(node.getKind()); + NodeBuilder nb(node.getKind()); if (node.getMetaKind() == metakind::PARAMETERIZED) { Debug("expand") << "op : " << node.getOperator() << std::endl; diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 9f1f71bd7..28f393704 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -14,6 +14,7 @@ #include "smt/preprocessor.h" +#include "options/expr_options.h" #include "options/smt_options.h" #include "preprocessing/preprocessing_pass_context.h" #include "printer/printer.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d7c44fef3..a925c04ab 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -24,6 +24,7 @@ #include "expr/bound_var_manager.h" #include "expr/node.h" #include "options/base_options.h" +#include "options/expr_options.h" #include "options/language.h" #include "options/main_options.h" #include "options/printer_options.h" diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h index de53e539c..495c2c16d 100644 --- a/src/smt_util/boolean_simplification.h +++ b/src/smt_util/boolean_simplification.h @@ -82,7 +82,7 @@ class BooleanSimplification { return buffer[0]; } - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); nb.append(buffer); return nb; } @@ -108,7 +108,7 @@ class BooleanSimplification { return buffer[0]; } - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); nb.append(buffer); return nb; } @@ -128,7 +128,7 @@ class BooleanSimplification { TNode right = implication[1]; Node notLeft = negate(left); - Node clause = NodeBuilder<2>(kind::OR) << notLeft << right; + Node clause = NodeBuilder(kind::OR) << notLeft << right; return simplifyClause(clause); } diff --git a/src/smt_util/nary_builder.cpp b/src/smt_util/nary_builder.cpp index efff058c5..ef988318f 100644 --- a/src/smt_util/nary_builder.cpp +++ b/src/smt_util/nary_builder.cpp @@ -185,7 +185,7 @@ Node RePairAssocCommutativeOperators::case_other(TNode n){ return n; } - NodeBuilder<> nb(n.getKind()); + NodeBuilder nb(n.getKind()); if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << n.getOperator(); diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 8e75f6850..caa052065 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -1785,7 +1785,7 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){ // Node explainSet(const set<ConstraintP>& inp){ // Assert(!inp.empty()); -// NodeBuilder<> nb(kind::AND); +// NodeBuilder nb(kind::AND); // set<ConstraintP>::const_iterator iter, end; // for(iter = inp.begin(), end = inp.end(); iter != end; ++iter){ // const ConstraintP c = *iter; diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 4c991dba3..218fdf179 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -35,7 +35,7 @@ namespace theory { namespace arith { Node ArithIteUtils::applyReduceVariablesInItes(Node n){ - NodeBuilder<> nb(n.getKind()); + NodeBuilder nb(n.getKind()); if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (n.getOperator()); } @@ -239,7 +239,7 @@ Node ArithIteUtils::reduceConstantIteByGCD(Node n){ } if(n.getNumChildren() > 0){ - NodeBuilder<> nb(n.getKind()); + NodeBuilder nb(n.getKind()); if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << (n.getOperator()); } diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 87aba7b45..452200796 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -235,7 +235,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if( num==1 ){ return RewriteResponse(REWRITE_AGAIN, base); }else{ - NodeBuilder<> nb(kind::MULT); + NodeBuilder nb(kind::MULT); for(unsigned i=0; i < num; ++i){ nb << base; } diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 9c764ac7a..ce54133c5 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -57,8 +57,8 @@ ArithStaticLearner::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications); } -void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ - +void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned) +{ vector<TNode> workList; workList.push_back(n); TNodeSet processed; @@ -101,8 +101,10 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ } } - -void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){ +void ArithStaticLearner::process(TNode n, + NodeBuilder& learned, + const TNodeSet& defTrue) +{ Debug("arith::static") << "===================== looking at " << n << endl; switch(n.getKind()){ @@ -136,7 +138,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet } } -void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ +void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned) +{ Assert(n.getKind() == kind::ITE); Assert(n[0].getKind() != EQUAL); Assert(isRelationOperator(n[0].getKind())); @@ -167,8 +170,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ switch(k){ case LT: // (ite (< x y) x y) case LEQ: { // (ite (<= x y) x y) - Node nLeqX = NodeBuilder<2>(LEQ) << n << t; - Node nLeqY = NodeBuilder<2>(LEQ) << n << e; + Node nLeqX = NodeBuilder(LEQ) << n << t; + Node nLeqY = NodeBuilder(LEQ) << n << e; Debug("arith::static") << n << "is a min =>" << nLeqX << nLeqY << endl; learned << nLeqX << nLeqY; ++(d_statistics.d_iteMinMaxApplications); @@ -176,8 +179,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ } case GT: // (ite (> x y) x y) case GEQ: { // (ite (>= x y) x y) - Node nGeqX = NodeBuilder<2>(GEQ) << n << t; - Node nGeqY = NodeBuilder<2>(GEQ) << n << e; + Node nGeqX = NodeBuilder(GEQ) << n << t; + Node nGeqY = NodeBuilder(GEQ) << n << e; Debug("arith::static") << n << "is a max =>" << nGeqX << nGeqY << endl; learned << nGeqX << nGeqY; ++(d_statistics.d_iteMinMaxApplications); @@ -188,7 +191,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ } } -void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ +void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned) +{ Assert(n.getKind() == ITE); Debug("arith::static") << "iteConstant(" << n << ")" << endl; @@ -202,9 +206,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ d_minMap.insert(n, min); Node nGeqMin; if (min.getInfinitesimalPart() == 0) { - nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart()); + nGeqMin = NodeBuilder(kind::GEQ) + << n << mkRationalNode(min.getNoninfinitesimalPart()); } else { - nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart()); + nGeqMin = NodeBuilder(kind::GT) + << n << mkRationalNode(min.getNoninfinitesimalPart()); } learned << nGeqMin; Debug("arith::static") << n << " iteConstant" << nGeqMin << endl; @@ -221,9 +227,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ d_maxMap.insert(n, max); Node nLeqMax; if (max.getInfinitesimalPart() == 0) { - nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart()); + nLeqMax = NodeBuilder(kind::LEQ) + << n << mkRationalNode(max.getNoninfinitesimalPart()); } else { - nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart()); + nLeqMax = NodeBuilder(kind::LT) + << n << mkRationalNode(max.getNoninfinitesimalPart()); } learned << nLeqMax; Debug("arith::static") << n << " iteConstant" << nLeqMax << endl; diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 73810dedd..b96d7a86a 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -45,19 +45,22 @@ private: public: ArithStaticLearner(context::Context* userContext); ~ArithStaticLearner(); - void staticLearning(TNode n, NodeBuilder<>& learned); + void staticLearning(TNode n, NodeBuilder& learned); void addBound(TNode n); -private: - void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue); + private: + void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue); - void iteMinMax(TNode n, NodeBuilder<>& learned); - void iteConstant(TNode n, NodeBuilder<>& learned); + void iteMinMax(TNode n, NodeBuilder& learned); + void iteConstant(TNode n, NodeBuilder& learned); - /** These fields are designed to be accessible to ArithStaticLearner methods. */ - class Statistics { - public: + /** + * These fields are designed to be accessible to ArithStaticLearner methods. + */ + class Statistics + { + public: IntStat d_iteMinMaxApplications; IntStat d_iteConstantApplications; diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 852550917..bc35c6941 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -194,17 +194,18 @@ inline Kind negateKind(Kind k){ inline Node negateConjunctionAsClause(TNode conjunction){ Assert(conjunction.getKind() == kind::AND); - NodeBuilder<> orBuilder(kind::OR); + NodeBuilder orBuilder(kind::OR); for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){ TNode child = *i; - Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child); + Node negatedChild = NodeBuilder(kind::NOT) << (child); orBuilder << negatedChild; } return orBuilder; } -inline Node maybeUnaryConvert(NodeBuilder<>& builder){ +inline Node maybeUnaryConvert(NodeBuilder& builder) +{ Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT); Assert(builder.getNumChildren() >= 1); @@ -247,7 +248,8 @@ inline Node getIdentity(Kind k){ } } -inline Node safeConstructNary(NodeBuilder<>& nb) { +inline Node safeConstructNary(NodeBuilder& nb) +{ switch (nb.getNumChildren()) { case 0: return getIdentity(nb.getKind()); diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index ea597468d..43589fdce 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -223,7 +223,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP TNode eq = d_watchedEqualities[s]; ConstraintCP eqC = d_constraintDatabase.getConstraint( s, ConstraintType::Equality, lb->getValue()); - NodeBuilder<> reasonBuilder(Kind::AND); + NodeBuilder reasonBuilder(Kind::AND); auto pfLb = lb->externalExplainByAssertions(reasonBuilder); auto pfUb = ub->externalExplainByAssertions(reasonBuilder); Node reason = safeConstructNary(reasonBuilder); @@ -256,7 +256,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){ //Explain for conflict is correct as these proofs are generated //and stored eagerly //These will be safe for propagation later as well - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); // An open proof of eq from literals now in reason. if (Debug.isOn("arith::cong")) { @@ -284,7 +284,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){ //Explain for conflict is correct as these proofs are generated and stored eagerly //These will be safe for propagation later as well - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); // An open proof of eq from literals now in reason. auto pf = c->externalExplainByAssertions(nb); if (Debug.isOn("arith::cong::notzero")) @@ -456,7 +456,9 @@ void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumpti } } -void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){ +void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, + NodeBuilder& nb) +{ std::set<TNode>::const_iterator it = s.begin(); std::set<TNode>::const_iterator it_end = s.end(); for(; it != it_end; ++it) { @@ -504,7 +506,8 @@ TrustNode ArithCongruenceManager::explain(TNode external) return trn; } -void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){ +void ArithCongruenceManager::explain(TNode external, NodeBuilder& out) +{ Node internal = externalToInternal(external); std::vector<TNode> assumptions; @@ -627,7 +630,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){ Node eq = xAsNode.eqNode(asRational); d_keepAlive.push_back(eq); - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); auto pf = c->externalExplainByAssertions(nb); Node reason = safeConstructNary(nb); d_keepAlive.push_back(reason); @@ -646,7 +649,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ << ub << std::endl; ArithVar x = lb->getVariable(); - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); auto pfLb = lb->externalExplainByAssertions(nb); auto pfUb = ub->externalExplainByAssertions(nb); Node reason = safeConstructNary(nb); diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 055d5ddbb..325f7002b 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -212,7 +212,7 @@ private: void enableSharedTerms(); void dequeueLiterals(); - void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb); + void enqueueIntoNB(const std::set<TNode> all, NodeBuilder& nb); /** * Determine an explaination for `internal`. That is a conjunction of theory @@ -251,7 +251,7 @@ private: */ TrustNode explain(TNode literal); - void explain(TNode lit, NodeBuilder<>& out); + void explain(TNode lit, NodeBuilder& out); void addWatchedPair(ArithVar s, TNode x, TNode y); diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index baa9b1ebb..14daca11b 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -481,7 +481,7 @@ bool Constraint::isInternalAssumption() const { TrustNode Constraint::externalExplainByAssertions() const { - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel); Node exp = safeConstructNary(nb); if (d_database->isProofEnabled()) @@ -1078,12 +1078,12 @@ TrustNode Constraint::split() TNode lhs = eqNode[0]; TNode rhs = eqNode[1]; - Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs; - Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs; - Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs; - Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs; + Node leqNode = NodeBuilder(kind::LEQ) << lhs << rhs; + Node ltNode = NodeBuilder(kind::LT) << lhs << rhs; + Node gtNode = NodeBuilder(kind::GT) << lhs << rhs; + Node geqNode = NodeBuilder(kind::GEQ) << lhs << rhs; - Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode; + Node lemma = NodeBuilder(OR) << leqNode << geqNode; TrustNode trustedLemma; if (d_database->isProofEnabled()) @@ -1517,7 +1517,7 @@ TrustNode Constraint::externalExplainForPropagation(TNode lit) const Assert(hasProof()); Assert(!isAssumption()); Assert(!isInternalAssumption()); - NodeBuilder<> nb(Kind::AND); + NodeBuilder nb(Kind::AND); auto pfFromAssumptions = externalExplain(nb, d_assertionOrder); Node n = safeConstructNary(nb); if (d_database->isProofEnabled()) @@ -1553,7 +1553,7 @@ TrustNode Constraint::externalExplainConflict() const { Debug("pf::arith::explain") << this << std::endl; Assert(inConflict()); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); auto pf1 = externalExplainByAssertions(nb); auto not2 = getNegation()->getProofLiteral().negate(); auto pf2 = getNegation()->externalExplainByAssertions(nb); @@ -1650,7 +1650,7 @@ void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){ } Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){ - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); ConstraintCPVec::const_iterator i, end; for(i = v.begin(), end = v.end(); i != end; ++i){ ConstraintCP v_i = *i; @@ -1660,7 +1660,7 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order) } std::shared_ptr<ProofNode> Constraint::externalExplain( - NodeBuilder<>& nb, AssertionOrder order) const + NodeBuilder& nb, AssertionOrder order) const { if (Debug.isOn("pf::arith::explain")) { @@ -1857,14 +1857,14 @@ std::shared_ptr<ProofNode> Constraint::externalExplain( } Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){ - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); a->externalExplainByAssertions(nb); b->externalExplainByAssertions(nb); return nb; } Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){ - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); a->externalExplainByAssertions(nb); b->externalExplainByAssertions(nb); c->externalExplainByAssertions(nb); @@ -1982,7 +1982,7 @@ TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const return d_congruenceManager.explain(c->getLiteral()); } -void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const +void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder& nb) const { Assert(c->hasLiteral()); // NOTE: this is not a recommended method since it ignores proofs diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index d00f16c90..33e39a5f0 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -571,8 +571,7 @@ class Constraint { * This is not appropriate for propagation! * Use explainForPropagation() instead. */ - std::shared_ptr<ProofNode> externalExplainByAssertions( - NodeBuilder<>& nb) const + std::shared_ptr<ProofNode> externalExplainByAssertions(NodeBuilder& nb) const { return externalExplain(nb, AssertionOrderSentinel); } @@ -876,7 +875,7 @@ class Constraint { * This is the minimum fringe of the implication tree * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). */ - std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb, + std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb, AssertionOrder order) const; static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); @@ -1168,7 +1167,7 @@ private: */ TrustNode eeExplain(ConstraintCP c) const; /** Get an explanation for this constraint from the equality engine */ - void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; + void eeExplain(ConstraintCP c, NodeBuilder& nb) const; /** * Returns a constraint with the variable v, the constraint type t, and a value diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 6e069cdf6..3825a3a42 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -198,7 +198,7 @@ Node DioSolver::proveIndex(TrailIndex i){ const Polynomial& proof = d_trail[i].d_proof; Assert(!proof.isConstant()); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); for(Polynomial::iterator iter = proof.begin(), end = proof.end(); iter!= end; ++iter){ Monomial m = (*iter); Assert(!m.isConstant()); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 7b9002d82..940812604 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -420,7 +420,7 @@ public: template <class GetNodeIterator> inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) { - NodeBuilder<> nb(k); + NodeBuilder nb(k); while(start != end) { nb << (*start).getNode(); diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 23f141535..248897ced 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -108,8 +108,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, // Whether a strict inequality is in the sum. bool strict = false; - NodeBuilder<> leftSum(Kind::PLUS); - NodeBuilder<> rightSum(Kind::PLUS); + NodeBuilder leftSum(Kind::PLUS); + NodeBuilder rightSum(Kind::PLUS); for (size_t i = 0; i < children.size(); ++i) { // Adjust strictness @@ -163,8 +163,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, // Whether a strict inequality is in the sum. bool strict = false; - NodeBuilder<> leftSum(Kind::PLUS); - NodeBuilder<> rightSum(Kind::PLUS); + NodeBuilder leftSum(Kind::PLUS); + NodeBuilder rightSum(Kind::PLUS); for (size_t i = 0; i < children.size(); ++i) { Rational scalar = args[i].getConst<Rational>(); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 577aa0e6c..2e2a99174 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -139,8 +139,8 @@ TrustNode TheoryArith::ppRewriteEq(TNode atom) return TrustNode::null(); } Assert(atom[0].getType().isReal()); - Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; + Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1]; + Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1]; Node rewritten = Rewriter::rewrite(leq.andNode(geq)); Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; @@ -161,7 +161,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert( return d_internal->ppAssert(tin, outSubstitutions); } -void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned) +{ d_internal->ppStaticLearn(n, learned); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 40abe21e0..94d8a11dd 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -120,7 +120,7 @@ class TheoryArith : public Theory { * symbols. */ TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void ppStaticLearn(TNode in, NodeBuilder& learned) override; std::string identify() const override { return std::string("TheoryArith"); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index b11bff768..349630c02 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -244,7 +244,7 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& // Assert(uppos < upconf.getNumChildren()); // Assert(equalUpToNegation(dnconf[dnpos], upconf[uppos])); - // NodeBuilder<> nb(kind::AND); + // NodeBuilder nb(kind::AND); // dropPosition(nb, dnconf, dnpos); // dropPosition(nb, upconf, uppos); // return safeConstructNary(nb); @@ -1201,14 +1201,13 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert( return Theory::PP_ASSERT_STATUS_UNSOLVED; } -void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder& learned) +{ TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer); d_learner.staticLearning(n, learned); } - - ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){ ArithVar bestBasic = ARITHVAR_SENTINEL; uint64_t bestRowLength = std::numeric_limits<uint64_t>::max(); @@ -2211,7 +2210,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const C Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){ Debug("arith::toSumNode") << "toSumNode() begin" << endl; - NodeBuilder<> nb(kind::PLUS); + NodeBuilder nb(kind::PLUS); NodeManager* nm = NodeManager::currentNM(); DenseMap<Rational>::const_iterator iter, end; iter = sum.begin(), end = sum.end(); @@ -4682,7 +4681,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b } Node flattenImplication(Node imp){ - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); std::unordered_set<Node, NodeHashFunction> included; Node left = imp[0]; Node right = imp[1]; @@ -4770,7 +4769,7 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C // Add the explaination proofs. for (const auto constraint : explain) { - NodeBuilder<> nb; + NodeBuilder nb; conflictPfs.push_back(constraint->externalExplainByAssertions(nb)); } // Collect the farkas coefficients, as nodes. @@ -5275,7 +5274,7 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t Assert(Polynomial::isMember(tp)); tmp.second = DeltaRational(0); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Polynomial p = Polynomial::parsePolynomial(tp); for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) { @@ -5460,7 +5459,7 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg switch(finalState){ case Inferred: { - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ const Tableau::Entry& e =*ri; ArithVar colVar = e.getColVar(); @@ -5668,7 +5667,7 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg // switch(finalState){ // case Inferred: // { -// NodeBuilder<> nb(kind::AND); +// NodeBuilder nb(kind::AND); // for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); // !ri.atEnd(); ++ri){ // const Tableau::Entry& e =*ri; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 929f40b56..1a40af4a0 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -474,7 +474,7 @@ private: void notifyRestart(); Theory::PPAssertStatus ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions); - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder& learned); std::string identify() const { return std::string("TheoryArith"); } @@ -678,8 +678,7 @@ private: bool isImpliedUpperBound(ArithVar var, Node exp); bool isImpliedLowerBound(ArithVar var, Node exp); - void internalExplain(TNode n, NodeBuilder<>& explainBuilder); - + void internalExplain(TNode n, NodeBuilder& explainBuilder); void asVectors(const Polynomial& p, std::vector<Rational>& coeffs, diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 543d9833c..3403eaee7 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -250,7 +250,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck // (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0 TNode write_i, write_j, index_i, index_j; Node conc; - NodeBuilder<> result(kind::AND); + NodeBuilder result(kind::AND); int i, j; write_i = left; for (i = leftWrites-1; i >= 0; --i) { @@ -260,7 +260,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck // ... && index_i /= index_(i+1)] -> read(store, index_i) = v_i write_j = left; { - NodeBuilder<> hyp(kind::AND); + NodeBuilder hyp(kind::AND); for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; if (!ppCheck || !ppDisequal(index_i, index_j)) { @@ -303,7 +303,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck // store(store(...),i,select(a,i)) = a && select(store(...),i)=v Node l = left; Node tmp; - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); while (right.getKind() == kind::STORE) { tmp = nm->mkNode(kind::SELECT, l, right[1]); nb << tmp.eqNode(right[2]); @@ -337,7 +337,7 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems) // select(store(a,i,v),j) = select(a,j) // IF i != j if (term[0].getKind() == kind::STORE && ppDisequal(term[0][1], term[1])) { - ret = NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1]; + ret = NodeBuilder(kind::SELECT) << term[0][0] << term[1]; } break; } @@ -345,8 +345,10 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems) // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) // IF i != j and j comes before i in the ordering if (term[0].getKind() == kind::STORE && (term[1] < term[0][1]) && ppDisequal(term[1],term[0][1])) { - Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2]; - Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2]; + Node inner = NodeBuilder(kind::STORE) + << term[0][0] << term[1] << term[2]; + Node outer = NodeBuilder(kind::STORE) + << inner << term[0][1] << term[0][2]; ret = outer; } break; @@ -1443,7 +1445,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned } } - NodeBuilder<> conjunction(invert ? kind::OR : kind::AND); + NodeBuilder conjunction(invert ? kind::OR : kind::AND); std::set<TNode>::const_iterator it = all.begin(); std::set<TNode>::const_iterator it_end = all.end(); while (it != it_end) { diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index f1e002735..70a5674b8 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -88,7 +88,7 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) Assert(childList.size() < static_cast<size_t>(expr::NodeValue::MAX_CHILDREN) * static_cast<size_t>(expr::NodeValue::MAX_CHILDREN)); - NodeBuilder<> nb(k); + NodeBuilder nb(k); ChildList::iterator cur = childList.begin(), next, en = childList.end(); while (cur != en) { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 62c458723..acb67a373 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -151,7 +151,7 @@ Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) { return assertion; } - NodeBuilder<> result(assertion.getKind()); + NodeBuilder result(assertion.getKind()); if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) { result << assertion.getOperator(); } @@ -204,7 +204,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) assertion_table.addEntry(func.getOperator(), args); } - NodeBuilder<> assertion_builder(kind::OR); + NodeBuilder assertion_builder(kind::OR); // construct skolemized assertion for (ArgsTable::iterator it = assertion_table.begin(); it != assertion_table.end(); @@ -214,7 +214,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) ++(d_statistics.d_numArgsSkolemized); TNode func = it->first; ArgsTableEntry& args = it->second; - NodeBuilder<> skolem_func(kind::APPLY_UF); + NodeBuilder skolem_func(kind::APPLY_UF); skolem_func << func; std::vector<Node> skolem_args; @@ -241,7 +241,7 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) // for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); // ++it) { - NodeBuilder<> arg_assignment(kind::AND); + NodeBuilder arg_assignment(kind::AND); // ArgsVec& args = *it; for (unsigned k = 0; k < av.size(); ++k) { @@ -342,7 +342,7 @@ Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) { return sig; } - NodeBuilder<> builder(node.getKind()); + NodeBuilder builder(node.getKind()); if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << node.getOperator(); } @@ -676,7 +676,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign return signature; } - NodeBuilder<> builder(signature.getKind()); + NodeBuilder builder(signature.getKind()); if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << signature.getOperator(); } diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 311d44c94..dd0be5cc0 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -247,7 +247,7 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) } Assert(node.getType().isBitVector()); - NodeBuilder<> nb(node.getKind()); + NodeBuilder nb(node.getKind()); if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << node.getOperator(); diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index a5d3e9bb6..568ef2ebf 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -411,7 +411,7 @@ bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) { if (clause.size() > 1) { - NodeBuilder<> lemmab(kind::OR); + NodeBuilder lemmab(kind::OR); for (unsigned i = 0; i < clause.size(); ++ i) { lemmab << d_cnf->getNode(clause[i]); } diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index faa285b97..8fa8fd850 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -90,7 +90,7 @@ class BVSolver virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }; - virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned){}; + virtual void ppStaticLearn(TNode in, NodeBuilder& learned){}; virtual void presolve(){}; diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp index 125cb243f..0aa99a889 100644 --- a/src/theory/bv/bv_solver_bitblast.cpp +++ b/src/theory/bv/bv_solver_bitblast.cpp @@ -256,7 +256,7 @@ Node BVSolverBitblast::getValue(TNode node) } else if (it->second.isNull()) { - NodeBuilder<> nb(cur.getKind()); + NodeBuilder nb(cur.getKind()); if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { nb << cur.getOperator(); diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index 00190233c..c12121bf8 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -741,7 +741,7 @@ EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) ; } -void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned) +void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned) { if (d_staticLearnCache.find(in) != d_staticLearnCache.end()) { diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index ea647346e..35b9964e0 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -97,7 +97,7 @@ class BVSolverLazy : public BVSolver TrustNode ppRewrite(TNode t) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void ppStaticLearn(TNode in, NodeBuilder& learned) override; void presolve() override; diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index c025dab5d..221ad3cbd 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -160,7 +160,7 @@ Node SubstitutionEx::internalApply(TNode node) { // children already processed if (head.childrenAdded) { - NodeBuilder<> nb(current.getKind()); + NodeBuilder nb(current.getKind()); std::vector<Node> reasons; if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -512,7 +512,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { return changed; } - NodeBuilder<> nb(kind::BITVECTOR_XOR); + NodeBuilder nb(kind::BITVECTOR_XOR); for (unsigned i = 1; i < left.getNumChildren(); ++i) { nb << left[i]; } @@ -848,7 +848,7 @@ void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) { Node sk = utils::mkVar(size); skolems.push_back(sk); } - NodeBuilder<> skolem_nb(kind::BITVECTOR_CONCAT); + NodeBuilder skolem_nb(kind::BITVECTOR_CONCAT); for (int i = skolems.size() - 1; i >= 0; --i) { skolem_nb << skolems[i]; @@ -975,7 +975,7 @@ Node mergeExplanations(const std::vector<Node>& expls) { return *literals.begin(); } - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) { nb << *it; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 8f9f88ea2..2c6d52b15 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -223,7 +223,7 @@ void TheoryBV::notifySharedTerm(TNode t) d_internal->notifySharedTerm(t); } -void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) +void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned) { d_internal->ppStaticLearn(in, learned); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c9ddaad11..c22f5c95a 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -92,7 +92,7 @@ class TheoryBV : public Theory TrustNode ppRewrite(TNode t, std::vector<SkolemLemma>& lems) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void ppStaticLearn(TNode in, NodeBuilder& learned) override; void presolve() override; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index e92ed5543..6435e0e3c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -642,7 +642,7 @@ struct ApplyRuleToChildren { if (node.getKind() != kind) { return RewriteRule<rule>::template run<true>(node); } - NodeBuilder<> result(kind); + NodeBuilder result(kind); for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) { result << RewriteRule<rule>::template run<true>(node[i]); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 7060b68a9..c463f0faf 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -36,7 +36,7 @@ bool RewriteRule<ConcatFlatten>::applies(TNode node) { template<> inline Node RewriteRule<ConcatFlatten>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<ConcatFlatten>(" << node << ")" << std::endl; - NodeBuilder<> result(kind::BITVECTOR_CONCAT); + NodeBuilder result(kind::BITVECTOR_CONCAT); std::vector<Node> processing_stack; processing_stack.push_back(node); while (!processing_stack.empty()) { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 4872f8070..39425b41e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -284,7 +284,7 @@ static inline void updateCoefMap(TNode current, unsigned size, } } else if (current[current.getNumChildren()-1].isConst()) { - NodeBuilder<> nb(kind::BITVECTOR_MULT); + NodeBuilder nb(kind::BITVECTOR_MULT); TNode::iterator child_it = current.begin(); for(; (child_it+1) != current.end(); ++child_it) { Assert(!(*child_it).isConst()); @@ -353,7 +353,7 @@ static inline void addToChildren(TNode term, } else if (term.getKind() == kind::BITVECTOR_MULT) { - NodeBuilder<> nb(kind::BITVECTOR_MULT); + NodeBuilder nb(kind::BITVECTOR_MULT); TNode::iterator child_it = term.begin(); for (; child_it != term.end(); ++child_it) { @@ -896,7 +896,7 @@ bool RewriteRule<BitwiseEq>::applies(TNode node) { static inline Node mkNodeKind(Kind k, TNode node, TNode c) { unsigned i = 0; unsigned nc = node.getNumChildren(); - NodeBuilder<> nb(k); + NodeBuilder nb(k); for(; i < nc; ++i) { nb << node[i].eqNode(c); } @@ -991,7 +991,7 @@ template<> inline Node RewriteRule<NegMult>::apply(TNode node) { Debug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl; TNode mult = node[0]; - NodeBuilder<> nb(kind::BITVECTOR_MULT); + NodeBuilder nb(kind::BITVECTOR_MULT); BitVector bv(utils::getSize(node), (unsigned)1); TNode::iterator child_it = mult.begin(); for(; (child_it+1) != mult.end(); ++child_it) { @@ -1492,8 +1492,8 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node) Debug("bv-rewrite") << "RewriteRule<NormalizeEqPlusNeg>(" << node << ")" << std::endl; - NodeBuilder<> nb_lhs(kind::BITVECTOR_PLUS); - NodeBuilder<> nb_rhs(kind::BITVECTOR_PLUS); + NodeBuilder nb_lhs(kind::BITVECTOR_PLUS); + NodeBuilder nb_rhs(kind::BITVECTOR_PLUS); NodeManager *nm = NodeManager::currentNM(); if (node[0].getKind() == kind::BITVECTOR_PLUS) diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 3244ebb6e..3dd0da3bd 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -286,7 +286,7 @@ inline Node RewriteRule<RepeatEliminate>::apply(TNode node) if(amount == 1) { return a; } - NodeBuilder<> result(kind::BITVECTOR_CONCAT); + NodeBuilder result(kind::BITVECTOR_CONCAT); for(unsigned i = 0; i < amount; ++i) { result << node[0]; } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 2e99cc467..c0bce9097 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -558,10 +558,10 @@ inline Node RewriteRule<AndOrXorConcatPullUp>::apply(TNode node) Kind kind = node.getKind(); TNode concat; Node x, y, z, c; - NodeBuilder<> xb(kind); - NodeBuilder<> yb(kind::BITVECTOR_CONCAT); - NodeBuilder<> zb(kind::BITVECTOR_CONCAT); - NodeBuilder<> res(kind::BITVECTOR_CONCAT); + NodeBuilder xb(kind); + NodeBuilder yb(kind::BITVECTOR_CONCAT); + NodeBuilder zb(kind::BITVECTOR_CONCAT); + NodeBuilder res(kind::BITVECTOR_CONCAT); NodeManager* nm = NodeManager::currentNM(); for (const TNode& child : node) @@ -1680,13 +1680,13 @@ Node RewriteRule<MergeSignExtend>::apply(TNode node) { .d_zeroExtendAmount; if (amount2 == 0) { - NodeBuilder<> nb(kind::BITVECTOR_SIGN_EXTEND); + NodeBuilder nb(kind::BITVECTOR_SIGN_EXTEND); Node op = nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount1)); nb << op << node[0][0]; Node res = nb; return res; } - NodeBuilder<> nb(kind::BITVECTOR_ZERO_EXTEND); + NodeBuilder nb(kind::BITVECTOR_ZERO_EXTEND); Node op = nm->mkConst<BitVectorZeroExtend>( BitVectorZeroExtend(amount1 + amount2)); nb << op << node[0][0]; @@ -2246,7 +2246,7 @@ Node RewriteRule<MultSltMult>::apply(TNode node) Node zero_t = utils::mkZero(utils::getSize(t)); Node zero_a = utils::mkZero(utils::getSize(a)); - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Kind k = is_sext ? kind::BITVECTOR_SLT : kind::BITVECTOR_ULT; nb << t.eqNode(zero_t).notNode(); nb << a.eqNode(zero_a).notNode(); diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index c2a7f05b6..96f91ea9f 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -384,7 +384,7 @@ Node mkConcat(TNode node, unsigned repeat) { return node; } - NodeBuilder<> result(kind::BITVECTOR_CONCAT); + NodeBuilder result(kind::BITVECTOR_CONCAT); for (unsigned i = 0; i < repeat; ++i) { result << node; @@ -503,7 +503,7 @@ Node eliminateInt2Bv(TNode node) { return v[0]; } - NodeBuilder<> result(kind::BITVECTOR_CONCAT); + NodeBuilder result(kind::BITVECTOR_CONCAT); result.append(v.rbegin(), v.rend()); return Node(result); } diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 04258d441..38b6caf94 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -140,7 +140,7 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) /* All the same, or just one */ if (all.size() == 1) { return conjunctions[0]; } - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); for (TNode n : all) { conjunction << n; } return conjunction; } @@ -159,7 +159,7 @@ Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes) /* All the same, or just one */ if (all.size() == 1) { return nodes[0]; } - NodeBuilder<> disjunction(kind::OR); + NodeBuilder disjunction(kind::OR); for (TNode n : all) { disjunction << n; } return disjunction; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9d231f07d..6b455e38c 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -322,7 +322,7 @@ void TheoryDatatypes::postCheck(Effort level) Node test = utils::mkTester(n, consIndex, dt); Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; test = Rewriter::rewrite( test ); - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); nb << test << test.notNode(); Node lemma = nb; d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); @@ -543,7 +543,7 @@ TrustNode TheoryDatatypes::expandDefinition(Node n) { Assert(tn.isDatatype()); const DType& dt = tn.getDType(); - NodeBuilder<> b(APPLY_CONSTRUCTOR); + NodeBuilder b(APPLY_CONSTRUCTOR); b << dt[0].getConstructor(); size_t size, updateIndex; if (n.getKind() == TUPLE_UPDATE) @@ -957,7 +957,7 @@ void TheoryDatatypes::addTester( Assert(testerIndex != -1); //we must explain why each term in the set of testers for this equivalence class is equal std::vector< Node > eq_terms; - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); for (unsigned i = 0; i < n_lbl; i++) { Node ti = d_labels_data[n][i]; diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 769446fd2..ca147b88e 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -138,7 +138,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ } } Debug("dt-enum-debug") << "Get constructor..." << std::endl; - NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); + NodeBuilder b(kind::APPLY_CONSTRUCTOR); if (d_datatype.isParametric()) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index 3b5a115c8..1d124045b 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -648,7 +648,7 @@ symbolicBitVector<false> symbolicBitVector<isSigned>::toUnsigned(void) const template <> symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const { - NodeBuilder<> construct(kind::BITVECTOR_SIGN_EXTEND); + NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND); construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>( BitVectorSignExtend(extension)) << *this; @@ -659,7 +659,7 @@ symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const template <> symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const { - NodeBuilder<> construct(kind::BITVECTOR_ZERO_EXTEND); + NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND); construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>( BitVectorZeroExtend(extension)) << *this; @@ -673,7 +673,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract( { Assert(this->getWidth() > reduction); - NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + NodeBuilder construct(kind::BITVECTOR_EXTRACT); construct << NodeManager::currentNM()->mkConst<BitVectorExtract>( BitVectorExtract((this->getWidth() - 1) - reduction, 0)) << *this; @@ -724,7 +724,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract( { Assert(upper >= lower); - NodeBuilder<> construct(kind::BITVECTOR_EXTRACT); + NodeBuilder construct(kind::BITVECTOR_EXTRACT); construct << NodeManager::currentNM()->mkConst<BitVectorExtract>( BitVectorExtract(upper, lower)) << *this; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 38444c7af..f2df859f0 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -91,7 +91,7 @@ Node buildConjunct(const std::vector<TNode> &assumptions) { } else { // \todo see bv::utils::flattenAnd - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); for (std::vector<TNode>::const_iterator it = assumptions.begin(); it != assumptions.end(); ++it) { conjunction << *it; diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index d84c553de..ba94dca13 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -110,8 +110,7 @@ namespace rewrite { size_t children = node.getNumChildren(); if (children > 2) { - - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); for (size_t i = 0; i < children - 1; ++i) { for (size_t j = i + 1; j < children; ++j) { diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 014e46925..292ec2ec6 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -202,7 +202,7 @@ static Node dropChild(Node n, unsigned index) if (nchildren < 2) return Node::null(); Kind k = n.getKind(); - NodeBuilder<> nb(k); + NodeBuilder nb(k); for (unsigned i = 0; i < nchildren; ++i) { if (i == index) continue; @@ -350,7 +350,7 @@ Node BvInverter::solveBvLit(Node sv, unsigned upper, lower; upper = bv::utils::getSize(t) - 1; lower = 0; - NodeBuilder<> nb(BITVECTOR_CONCAT); + NodeBuilder nb(BITVECTOR_CONCAT); for (unsigned i = 0; i < nchildren; i++) { if (i < index) diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp index e53e64a94..53e672346 100644 --- a/src/theory/quantifiers/bv_inverter_utils.cpp +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -1180,7 +1180,7 @@ namespace { Node defaultShiftIC(Kind litk, Kind shk, Node s, Node t) { unsigned w; - NodeBuilder<> nb(OR); + NodeBuilder nb(OR); NodeManager* nm; nm = NodeManager::currentNM(); @@ -2000,7 +2000,7 @@ Node getICBvConcat(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t) unsigned nchildren = sv_t.getNumChildren(); unsigned w1 = 0, w2 = 0; unsigned w = bv::utils::getSize(t), wx = bv::utils::getSize(x); - NodeBuilder<> nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT); + NodeBuilder nbs1(BITVECTOR_CONCAT), nbs2(BITVECTOR_CONCAT); Node s1, s2; Node t1, t2, tx; Node scl, scr; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index 030258113..0a544f785 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -66,7 +66,7 @@ Node normalizePvMult( bool neg, neg_coeff = false; bool found_pv = false; NodeManager* nm; - NodeBuilder<> nb(BITVECTOR_MULT); + NodeBuilder nb(BITVECTOR_MULT); BvLinearAttribute is_linear; nm = NodeManager::currentNM(); @@ -168,8 +168,8 @@ Node normalizePvPlus( std::unordered_map<Node, bool, NodeHashFunction>& contains_pv) { NodeManager* nm; - NodeBuilder<> nb_c(BITVECTOR_PLUS); - NodeBuilder<> nb_l(BITVECTOR_PLUS); + NodeBuilder nb_c(BITVECTOR_PLUS); + NodeBuilder nb_l(BITVECTOR_PLUS); BvLinearAttribute is_linear; bool neg; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 2c91df7a7..89358c511 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -104,7 +104,8 @@ bool QuantifiersRewriter::isLiteral( Node n ){ return true; } -void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ +void QuantifiersRewriter::addNodeToOrBuilder(Node n, NodeBuilder& t) +{ if( n.getKind()==OR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ t << n[i]; @@ -1596,7 +1597,7 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) BoundVarManager* bvm = nm->getBoundVarManager(); // Break apart the quantifed formula // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn - NodeBuilder<> t(kind::AND); + NodeBuilder t(kind::AND); std::vector<Node> argsc; for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++) { @@ -1645,8 +1646,8 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa) // aggressive miniscoping implies that free variable miniscoping should // be applied first Node newBody = body; - NodeBuilder<> body_split(kind::OR); - NodeBuilder<> tb(kind::OR); + NodeBuilder body_split(kind::OR); + NodeBuilder tb(kind::OR); for (const Node& trm : body) { if (expr::hasSubterm(trm, args)) diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 5ea8352d0..c45bc9e88 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -140,7 +140,7 @@ class QuantifiersRewriter : public TheoryRewriter Kind k, std::map<Node, bool>& lit_pol, bool& childrenChanged); - static void addNodeToOrBuilder(Node n, NodeBuilder<>& t); + static void addNodeToOrBuilder(Node n, NodeBuilder& t); static void computeArgs(const std::vector<Node>& args, std::map<Node, bool>& activeMap, Node n, diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 2a19824ac..51b400dbe 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -85,7 +85,7 @@ TrustNode Skolemize::process(Node q) // otherwise, we use the more general skolemization with inductive // strengthening, which does not support proofs Node body = getSkolemizedBody(q); - NodeBuilder<> nb(kind::OR); + NodeBuilder nb(kind::OR); nb << q << body.notNode(); lem = nb; } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 1d9620dab..c247d8f08 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -89,7 +89,7 @@ struct RewriteStackElement { /** Index of the child this node is done rewriting */ unsigned d_nextChild : 32; /** Builder for this node */ - NodeBuilder<> d_builder; + NodeBuilder d_builder; }; RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 8d005c6fe..87a3ae9af 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1210,7 +1210,7 @@ Node mkAnd(const std::vector<TNode>& conjunctions) return conjunctions[0]; } - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); std::set<TNode>::const_iterator it = all.begin(); std::set<TNode>::const_iterator it_end = all.end(); while (it != it_end) diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index cc4027aad..04e0fe2e5 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -639,7 +639,7 @@ Node RegExpEntail::getFixedLengthForRegexp(Node n) } else if (n.getKind() == REGEXP_CONCAT) { - NodeBuilder<> nb(PLUS); + NodeBuilder nb(PLUS); for (const Node& nc : n) { Node flc = getFixedLengthForRegexp(nc); diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 302f7dc0b..a7bbb68e3 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -1184,7 +1184,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node one = nm->mkConst(Rational(1)); if (flr == one) { - NodeBuilder<> nb(AND); + NodeBuilder nb(AND); for (const Node& xc : x) { nb << nm->mkNode(STRING_IN_REGEXP, xc, r); @@ -1926,7 +1926,7 @@ Node SequencesRewriter::rewriteContains(Node node) { std::vector<Node> vec = Word::getChars(node[0]); Node emp = Word::mkEmptyWord(t.getType()); - NodeBuilder<> nb(OR); + NodeBuilder nb(OR); nb << emp.eqNode(t); for (const Node& c : vec) { @@ -1970,7 +1970,7 @@ Node SequencesRewriter::rewriteContains(Node node) { std::vector<Node> nc1; utils::getConcat(node[0], nc1); - NodeBuilder<> nb(OR); + NodeBuilder nb(OR); for (const Node& ncc : nc1) { nb << nm->mkNode(STRING_STRCTN, ncc, node[1]); @@ -2057,7 +2057,7 @@ Node SequencesRewriter::rewriteContains(Node node) if (nc2.size() > 1) { Node emp = Word::mkEmptyWord(stype); - NodeBuilder<> nb2(kind::AND); + NodeBuilder nb2(kind::AND); for (const Node& n2 : nc2) { if (n2 == n) @@ -3283,7 +3283,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) else if (len.getKind() == PLUS) { // x + y -> norm(x) + norm(y) - NodeBuilder<> concatBuilder(STRING_CONCAT); + NodeBuilder concatBuilder(STRING_CONCAT); for (const auto& n : len) { Node sn = canonicalStrForSymbolicLength(n, stype); @@ -3312,7 +3312,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) } std::vector<Node> nRepChildren; utils::getConcat(nRep, nRepChildren); - NodeBuilder<> concatBuilder(STRING_CONCAT); + NodeBuilder concatBuilder(STRING_CONCAT); for (size_t i = 0, reps = intReps.getUnsignedInt(); i < reps; i++) { concatBuilder.append(nRepChildren); diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 62ba41743..fc5a0a52c 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -842,7 +842,7 @@ Node StringsEntail::getMultisetApproximation(Node a) } else if (a.getKind() == STRING_CONCAT) { - NodeBuilder<> nb(STRING_CONCAT); + NodeBuilder nb(STRING_CONCAT); for (const Node& ac : a) { nb << getMultisetApproximation(ac); @@ -974,7 +974,7 @@ Node StringsEntail::inferEqsFromContains(Node x, Node y) cs.push_back(yiLen[0]); } - NodeBuilder<> nb(AND); + NodeBuilder nb(AND); // (= x (str.++ y1' ... ym')) if (!cs.empty()) { diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 1a7ca7f6a..2a3da149c 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -179,7 +179,7 @@ Node StringsRewriter::rewriteStrConvert(Node node) } else if (node[0].getKind() == STRING_CONCAT) { - NodeBuilder<> concatBuilder(STRING_CONCAT); + NodeBuilder concatBuilder(STRING_CONCAT); for (const Node& nc : node[0]) { concatBuilder << nm->mkNode(nk, nc); diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index a61f2d49c..9102b6188 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -224,7 +224,7 @@ bool SubstitutionMinimize::findInternal(Node n, if (cur.getNumChildren() > 0) { std::vector<Node> children; - NodeBuilder<> nb(cur.getKind()); + NodeBuilder nb(cur.getKind()); if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { if (cur.getKind() == APPLY_UF) diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 7a4516996..1a45f467c 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -81,7 +81,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { if (stackHead.d_children_added) { // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << Node(cache[current.getOperator()]); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 4b06a5fa8..4c0d14346 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -686,7 +686,7 @@ class Theory { * *never* clear it. It is a conjunction to add to the formula at * the top-level and may contain other theories' contributions. */ - virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { } + virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {} enum PPAssertStatus { /** Atom has been solved */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6271f0afb..e4b05a3c2 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -727,7 +727,8 @@ void TheoryEngine::notifyRestart() { CVC4_FOR_EACH_THEORY; } -void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) { +void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder& learned) +{ // Reset the interrupt flag d_interrupted = false; @@ -1638,7 +1639,7 @@ theory::TrustNode TheoryEngine::getExplanation( } else { - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); std::set<TNode>::const_iterator it = exp.begin(); std::set<TNode>::const_iterator it_end = exp.end(); while (it != it_end) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7b91191f9..731e362ef 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -498,7 +498,7 @@ class TheoryEngine { * Calls ppStaticLearn() on all theories, accumulating their * combined contributions in the "learned" builder. */ - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder& learned); /** * Calls presolve() on all theories and returns true diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 78a4e6526..a28cb19f7 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -320,7 +320,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess( if (stackHead.children_added) { // Children have been processed, so substitute - NodeBuilder<> builder(current.getKind()); + NodeBuilder builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << current.getOperator(); @@ -396,7 +396,7 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term, Node newTerm = term; if (!term.isClosure()) { - NodeBuilder<> newNode(term.getKind()); + NodeBuilder newNode(term.getKind()); if (term.getMetaKind() == kind::metakind::PARAMETERIZED) { newNode << term.getOperator(); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 8f006d8ff..5fbbd3700 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1841,7 +1841,7 @@ void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigge Node EqualityEngine::evaluateTerm(TNode node) { Debug("equality::evaluation") << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl; - NodeBuilder<> builder; + NodeBuilder builder; builder << node.getKind(); if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { builder << node.getOperator(); diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 558838bd8..0586da6a0 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -525,7 +525,7 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { Debug("ufsymm") << "UFSYMM p == " << p << endl; if(i != p.end() || p.size() != cts.size()) { Debug("ufsymm") << "UFSYMM cts != p" << endl; - NodeBuilder<> disj(kind::OR); + NodeBuilder disj(kind::OR); NodeManager* nm = NodeManager::currentNM(); for (const Node& nn : cts) { diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index b4ea3640d..e38a1f67b 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -65,7 +65,7 @@ class SymmetryBreaker : public context::ContextNotifyObj { class Template { Node d_template; - NodeBuilder<> d_assertions; + NodeBuilder d_assertions; std::unordered_map<TNode, std::set<TNode>, TNodeHashFunction> d_sets; std::unordered_map<TNode, TNode, TNodeHashFunction> d_reps; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index f3c0a0ba0..6969da194 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -112,7 +112,7 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { return conjunctions[0]; } - NodeBuilder<> conjunction(kind::AND); + NodeBuilder conjunction(kind::AND); std::set<TNode>::const_iterator it = all.begin(); std::set<TNode>::const_iterator it_end = all.end(); while (it != it_end) { @@ -347,7 +347,8 @@ void TheoryUF::presolve() { Debug("uf") << "uf: end presolve()" << endl; } -void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { +void TheoryUF::ppStaticLearn(TNode n, NodeBuilder& learned) +{ //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); vector<TNode> workList; @@ -466,7 +467,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { if(options::ufSymmetryBreaker()) { d_symb.assertFormula(n); } -}/* TheoryUF::ppStaticLearn() */ +} /* TheoryUF::ppStaticLearn() */ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index f6f4b3ee9..66cf36ead 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -144,8 +144,7 @@ private: void preRegisterTerm(TNode term) override; TrustNode explain(TNode n) override; - - void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; + void ppStaticLearn(TNode in, NodeBuilder& learned) override; void presolve() override; void computeCareGraph() override; diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 5177ff453..02bd50b75 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -76,7 +76,7 @@ class TestNodeBlackNode : public TestNode void testNaryExpForSize(Kind k, uint32_t n) { - NodeBuilder<> nbz(k); + NodeBuilder nbz(k); Node trueNode = d_nodeManager->mkConst(true); for (uint32_t i = 0; i < n; ++i) { @@ -459,7 +459,7 @@ TEST_F(TestNodeBlackNode, getNumChildren) TEST_F(TestNodeBlackNode, iterator) { - NodeBuilder<> b; + NodeBuilder b; Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); @@ -518,8 +518,8 @@ TEST_F(TestNodeBlackNode, toString) "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node z = d_nodeManager->mkSkolem( "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node m = NodeBuilder<>() << w << x << kind::OR; - Node n = NodeBuilder<>() << m << y << z << kind::AND; + Node m = NodeBuilder() << w << x << kind::OR; + Node n = NodeBuilder() << m << y << z << kind::AND; ASSERT_EQ(n.toString(), "(AND (OR w x) y z)"); } @@ -536,9 +536,9 @@ TEST_F(TestNodeBlackNode, toStream) "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); Node z = d_nodeManager->mkSkolem( "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME); - Node m = NodeBuilder<>() << x << y << kind::OR; - Node n = NodeBuilder<>() << w << m << z << kind::AND; - Node o = NodeBuilder<>() << n << n << kind::XOR; + Node m = NodeBuilder() << x << y << kind::OR; + Node n = NodeBuilder() << w << m << z << kind::AND; + Node o = NodeBuilder() << n << n << kind::XOR; std::stringstream sstr; sstr << Node::dag(false); @@ -764,7 +764,7 @@ TEST_F(TestNodeBlackNode, isConst) namespace { Node level0(NodeManager* nm) { - NodeBuilder<> nb(kind::AND); + NodeBuilder nb(kind::AND); Node x = nm->mkSkolem("x", nm->booleanType()); nb << x; nb << x; diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 39c5552df..8c6145940 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -39,8 +39,7 @@ namespace test { class TestNodeBlackNodeBuilder : public TestNode { protected: - template <unsigned N> - void push_back(NodeBuilder<N>& nb, uint32_t n) + void push_back(NodeBuilder& nb, uint32_t n) { for (uint32_t i = 0; i < n; ++i) { @@ -54,189 +53,43 @@ class TestNodeBlackNodeBuilder : public TestNode TEST_F(TestNodeBlackNodeBuilder, ctors) { /* Default size tests. */ - NodeBuilder<> def; + NodeBuilder def; ASSERT_EQ(def.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(def.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(def.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif - NodeBuilder<> spec(d_specKind); + NodeBuilder spec(d_specKind); ASSERT_EQ(spec.getKind(), d_specKind); ASSERT_EQ(spec.getNumChildren(), 0u); - ASSERT_EQ(spec.begin(), spec.end()); - NodeBuilder<> from_nm(d_nodeManager.get()); + NodeBuilder from_nm(d_nodeManager.get()); ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS ASSERT_DEATH(from_nm.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif - NodeBuilder<> from_nm_kind(d_nodeManager.get(), d_specKind); + NodeBuilder from_nm_kind(d_nodeManager.get(), d_specKind); ASSERT_EQ(from_nm_kind.getKind(), d_specKind); ASSERT_EQ(from_nm_kind.getNumChildren(), 0u); - ASSERT_EQ(from_nm_kind.begin(), from_nm_kind.end()); - - /* Non-default size tests */ - NodeBuilder<K> ws; - ASSERT_EQ(ws.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - ASSERT_DEATH(ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); -#endif - - NodeBuilder<K> ws_kind(d_specKind); - ASSERT_EQ(ws_kind.getKind(), d_specKind); - ASSERT_EQ(ws_kind.getNumChildren(), 0u); - ASSERT_EQ(ws_kind.begin(), ws_kind.end()); - - NodeBuilder<K> ws_from_nm(d_nodeManager.get()); - ASSERT_EQ(ws_from_nm.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - ASSERT_DEATH(ws_from_nm.getNumChildren(), - "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(ws_from_nm.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(ws_from_nm.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); -#endif - - NodeBuilder<K> ws_from_nm_kind(d_nodeManager.get(), d_specKind); - ASSERT_EQ(ws_from_nm_kind.getKind(), d_specKind); - ASSERT_EQ(ws_from_nm_kind.getNumChildren(), 0u); - ASSERT_EQ(ws_from_nm_kind.begin(), ws_from_nm_kind.end()); - - /* Extreme size tests */ - NodeBuilder<0> ws_size_0; - - /* Allocating on the heap instead of the stack. */ - NodeBuilder<LARGE_K>* ws_size_large = new NodeBuilder<LARGE_K>; - delete ws_size_large; /* Copy constructors */ - NodeBuilder<> copy(def); + NodeBuilder copy(def); ASSERT_EQ(copy.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(copy.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(copy.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); -#endif - - NodeBuilder<K> cp_ws(ws); - ASSERT_EQ(cp_ws.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - ASSERT_DEATH(cp_ws.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(cp_ws.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(cp_ws.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); -#endif - - NodeBuilder<K - 10> cp_from_larger(ws); - ASSERT_EQ(cp_from_larger.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - ASSERT_DEATH(cp_from_larger.getNumChildren(), - "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(cp_from_larger.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(cp_from_larger.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); -#endif - - NodeBuilder<K + 10> cp_from_smaller(ws); - ASSERT_EQ(cp_from_smaller.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS - ASSERT_DEATH(cp_from_smaller.getNumChildren(), - "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(cp_from_smaller.begin(), - "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(cp_from_smaller.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif } TEST_F(TestNodeBlackNodeBuilder, dtor) { - NodeBuilder<K>* nb = new NodeBuilder<K>(); - delete nb; -} - -TEST_F(TestNodeBlackNodeBuilder, begin_end) -{ - /* Test begin() and end() without resizing. */ - NodeBuilder<K> ws(d_specKind); - ASSERT_EQ(ws.begin(), ws.end()); - - push_back(ws, K); - ASSERT_NE(ws.begin(), ws.end()); - - NodeBuilder<K>::iterator iter = ws.begin(); - for (uint32_t i = 0; i < K; ++i) - { - ASSERT_NE(iter, ws.end()); - ++iter; - } - ASSERT_EQ(iter, ws.end()); - - NodeBuilder<K>::const_iterator citer = ws.begin(); - for (uint32_t i = 0; i < K; ++i) - { - ASSERT_NE(citer, ws.end()); - ++citer; - } - ASSERT_EQ(citer, ws.end()); - - /* Repeat same tests and make sure that resizing occurs. */ - NodeBuilder<> smaller(d_specKind); - ASSERT_EQ(smaller.begin(), smaller.end()); - - push_back(smaller, K); - ASSERT_NE(smaller.begin(), smaller.end()); - - NodeBuilder<>::iterator smaller_iter = smaller.begin(); - for (uint32_t i = 0; i < K; ++i) - { - ASSERT_NE(smaller_iter, smaller.end()); - ++smaller_iter; - } - ASSERT_EQ(iter, ws.end()); - - NodeBuilder<>::const_iterator smaller_citer = smaller.begin(); - for (uint32_t i = 0; i < K; ++i) - { - ASSERT_NE(smaller_citer, smaller.end()); - ++smaller_citer; - } - ASSERT_EQ(smaller_citer, smaller.end()); -} - -TEST_F(TestNodeBlackNodeBuilder, iterator) -{ - NodeBuilder<> b; - Node x = d_nodeManager->mkSkolem("x", *d_boolTypeNode); - Node y = d_nodeManager->mkSkolem("z", *d_boolTypeNode); - Node z = d_nodeManager->mkSkolem("y", *d_boolTypeNode); - b << x << y << z << AND; - - { - NodeBuilder<>::iterator i = b.begin(); - ASSERT_EQ(*i++, x); - ASSERT_EQ(*i++, y); - ASSERT_EQ(*i++, z); - ASSERT_EQ(i, b.end()); - } - - { - const NodeBuilder<>& c = b; - NodeBuilder<>::const_iterator i = c.begin(); - ASSERT_EQ(*i++, x); - ASSERT_EQ(*i++, y); - ASSERT_EQ(*i++, z); - ASSERT_EQ(i, b.end()); - } + std::unique_ptr<NodeBuilder> nb(new NodeBuilder()); } TEST_F(TestNodeBlackNodeBuilder, getKind) { - NodeBuilder<> noKind; + NodeBuilder noKind; ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); @@ -244,16 +97,14 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) ASSERT_EQ(noKind.getKind(), UNDEFINED_KIND); noKind << PLUS; - ASSERT_EQ(noKind.getKind(), PLUS); Node n = noKind; - #ifdef CVC4_ASSERTIONS ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)"); #endif - NodeBuilder<> spec(PLUS); + NodeBuilder spec(PLUS); ASSERT_EQ(spec.getKind(), PLUS); spec << x << x; ASSERT_EQ(spec.getKind(), PLUS); @@ -263,12 +114,12 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) { Node x(d_nodeManager->mkSkolem("x", *d_intTypeNode)); - NodeBuilder<> nb; + NodeBuilder nb; #ifdef CVC4_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif - nb << PLUS << x << x; + nb << PLUS << x << x; ASSERT_EQ(nb.getNumChildren(), 2u); nb << x << x; @@ -278,10 +129,11 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) #ifdef CVC4_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif + nb.clear(PLUS); ASSERT_EQ(nb.getNumChildren(), 0u); - nb << x << x << x; + nb << x << x << x; ASSERT_EQ(nb.getNumChildren(), 3u); nb << x << x << x; @@ -296,7 +148,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) TEST_F(TestNodeBlackNodeBuilder, operator_square) { - NodeBuilder<> arr(d_specKind); + NodeBuilder arr(d_specKind); Node i_0 = d_nodeManager->mkConst(false); Node i_2 = d_nodeManager->mkConst(true); @@ -308,18 +160,14 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square) #endif arr << i_0; - ASSERT_EQ(arr[0], i_0); push_back(arr, 1); - arr << i_2; - ASSERT_EQ(arr[0], i_0); ASSERT_EQ(arr[2], i_2); push_back(arr, K - 3); - ASSERT_EQ(arr[0], i_0); ASSERT_EQ(arr[2], i_2); for (unsigned i = 3; i < K; ++i) @@ -328,7 +176,6 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square) } arr << i_K; - ASSERT_EQ(arr[0], i_0); ASSERT_EQ(arr[2], i_2); for (unsigned i = 3; i < K; ++i) @@ -345,72 +192,57 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square) TEST_F(TestNodeBlackNodeBuilder, clear) { - NodeBuilder<> nb; - + NodeBuilder nb; ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif nb << d_specKind; push_back(nb, K); - ASSERT_EQ(nb.getKind(), d_specKind); ASSERT_EQ(nb.getNumChildren(), K); - ASSERT_NE(nb.begin(), nb.end()); nb.clear(); - ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif nb << d_specKind; push_back(nb, K); - ASSERT_EQ(nb.getKind(), d_specKind); ASSERT_EQ(nb.getNumChildren(), K); - ASSERT_NE(nb.begin(), nb.end()); nb.clear(d_specKind); - ASSERT_EQ(nb.getKind(), d_specKind); ASSERT_EQ(nb.getNumChildren(), 0u); - ASSERT_EQ(nb.begin(), nb.end()); push_back(nb, K); nb.clear(); - ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); #ifdef CVC4_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(nb.begin(), "getKind\\(\\) != kind::UNDEFINED_KIND"); - ASSERT_DEATH(nb.end(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif } TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) { #ifdef CVC4_ASSERTIONS - NodeBuilder<> spec(d_specKind); + NodeBuilder spec(d_specKind); ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder"); #endif - NodeBuilder<> noSpec; + NodeBuilder noSpec; noSpec << d_specKind; ASSERT_EQ(noSpec.getKind(), d_specKind); - NodeBuilder<> modified; + NodeBuilder modified; push_back(modified, K); modified << d_specKind; ASSERT_EQ(modified.getKind(), d_specKind); - NodeBuilder<> nb(d_specKind); + NodeBuilder nb(d_specKind); nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false); nb.clear(PLUS); @@ -424,20 +256,20 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder"); #endif - NodeBuilder<> testRef; + NodeBuilder testRef; ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind); #ifdef CVC4_ASSERTIONS - NodeBuilder<> testTwo; + NodeBuilder testTwo; ASSERT_DEATH(testTwo << d_specKind << PLUS, "can't redefine the Kind of a NodeBuilder"); #endif - NodeBuilder<> testMixOrder1; + NodeBuilder testMixOrder1; ASSERT_EQ( (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(), d_specKind); - NodeBuilder<> testMixOrder2; + NodeBuilder testMixOrder2; ASSERT_EQ( (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(), d_specKind); @@ -445,30 +277,25 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node) { - NodeBuilder<K> nb(d_specKind); + NodeBuilder nb(d_specKind); ASSERT_EQ(nb.getKind(), d_specKind); ASSERT_EQ(nb.getNumChildren(), 0u); - ASSERT_EQ(nb.begin(), nb.end()); push_back(nb, K); ASSERT_EQ(nb.getKind(), d_specKind); ASSERT_EQ(nb.getNumChildren(), K); - ASSERT_NE(nb.begin(), nb.end()); #ifdef CVC4_ASSERTIONS Node n = nb; ASSERT_DEATH(nb << n, "!isUsed\\(\\)"); #endif - NodeBuilder<> overflow(d_specKind); + NodeBuilder overflow(d_specKind); ASSERT_EQ(overflow.getKind(), d_specKind); ASSERT_EQ(overflow.getNumChildren(), 0u); - ASSERT_EQ(overflow.begin(), overflow.end()); push_back(overflow, 5 * K + 1); - ASSERT_EQ(overflow.getKind(), d_specKind); ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1); - ASSERT_NE(overflow.begin(), overflow.end()); } TEST_F(TestNodeBlackNodeBuilder, append) @@ -495,7 +322,7 @@ TEST_F(TestNodeBlackNodeBuilder, append) "Nodes with kind XOR must have at most 2 children"); #endif - NodeBuilder<> b(d_specKind); + NodeBuilder b(d_specKind); /* test append(TNode) */ b.append(n).append(o).append(q); @@ -538,8 +365,8 @@ TEST_F(TestNodeBlackNodeBuilder, append) TEST_F(TestNodeBlackNodeBuilder, operator_node_cast) { - NodeBuilder<K> implicit(d_specKind); - NodeBuilder<K> explic(d_specKind); + NodeBuilder implicit(d_specKind); + NodeBuilder explic(d_specKind); push_back(implicit, K); push_back(explic, K); @@ -560,7 +387,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_node_cast) TEST_F(TestNodeBlackNodeBuilder, leftist_building) { - NodeBuilder<> nb; + NodeBuilder nb; Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode); diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index dcdbc074f..66ac65cb5 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -41,7 +41,7 @@ TEST_F(TestNodeWhiteNodeManager, mkConst_rational) TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) { - NodeBuilder<> nb; + NodeBuilder nb; ASSERT_NO_THROW(nb.realloc(15)); ASSERT_NO_THROW(nb.realloc(25)); diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index 20de9d3e4..9e3c4bb7d 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -17,6 +17,7 @@ #include <string> #include "base/check.h" +#include "expr/node_builder.h" #include "test_node.h" namespace cvc5 { @@ -36,7 +37,7 @@ TEST_F(TestNodeWhiteNode, copy_ctor) { Node e(Node::s_null); } TEST_F(TestNodeWhiteNode, builder) { - NodeBuilder<> b; + NodeBuilder b; ASSERT_TRUE(b.d_nv->getId() == 0); ASSERT_TRUE(b.d_nv->getKind() == UNDEFINED_KIND); ASSERT_EQ(b.d_nv->d_nchildren, 0u); diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index d313e01c7..6f0398439 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -2046,16 +2046,16 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial) bv::utils::mkExtract( d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0))); - NodeBuilder<> nbx(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nbx(d_nodeManager.get(), kind::BITVECTOR_MULT); nbx << d_x << d_one << x; Node x_mul_one_mul_xx = nbx.constructNode(); - NodeBuilder<> nby(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nby(d_nodeManager.get(), kind::BITVECTOR_MULT); nby << d_y << y << d_one; Node y_mul_yy_mul_one = nby.constructNode(); - NodeBuilder<> nbz(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nbz(d_nodeManager.get(), kind::BITVECTOR_MULT); nbz << d_three << d_z << z; Node three_mul_z_mul_zz = nbz.constructNode(); - NodeBuilder<> nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT); + NodeBuilder nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT); nbz2 << d_z << d_nine << z; Node z_mul_nine_mul_zz = nbz2.constructNode(); @@ -2671,20 +2671,20 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1) Node mult2x = d_nodeManager->mkNode(kind::BITVECTOR_MULT, zext40x, zext40x); ASSERT_EQ(BVGauss::getMinBwExpr(mult2x), 32); - NodeBuilder<> nbmult3p(kind::BITVECTOR_MULT); + NodeBuilder nbmult3p(kind::BITVECTOR_MULT); nbmult3p << zext48p << zext48p << zext48p; Node mult3p = nbmult3p; ASSERT_EQ(BVGauss::getMinBwExpr(mult3p), 11); - NodeBuilder<> nbmult3x(kind::BITVECTOR_MULT); + NodeBuilder nbmult3x(kind::BITVECTOR_MULT); nbmult3x << zext48x << zext48x << zext48x; Node mult3x = nbmult3x; ASSERT_EQ(BVGauss::getMinBwExpr(mult3x), 48); - NodeBuilder<> nbmult4p(kind::BITVECTOR_MULT); + NodeBuilder nbmult4p(kind::BITVECTOR_MULT); nbmult4p << zext48p << zext48p8 << zext48p; Node mult4p = nbmult4p; ASSERT_EQ(BVGauss::getMinBwExpr(mult4p), 11); - NodeBuilder<> nbmult4x(kind::BITVECTOR_MULT); + NodeBuilder nbmult4x(kind::BITVECTOR_MULT); nbmult4x << zext48x << zext48x8 << zext48x; Node mult4x = nbmult4x; ASSERT_EQ(BVGauss::getMinBwExpr(mult4x), 40); @@ -2739,29 +2739,29 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1) Node add3x = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext48x8, zext48x); ASSERT_EQ(BVGauss::getMinBwExpr(add3x), 17); - NodeBuilder<> nbadd4p(kind::BITVECTOR_PLUS); + NodeBuilder nbadd4p(kind::BITVECTOR_PLUS); nbadd4p << zext48p << zext48p << zext48p; Node add4p = nbadd4p; ASSERT_EQ(BVGauss::getMinBwExpr(add4p), 6); - NodeBuilder<> nbadd4x(kind::BITVECTOR_PLUS); + NodeBuilder nbadd4x(kind::BITVECTOR_PLUS); nbadd4x << zext48x << zext48x << zext48x; Node add4x = nbadd4x; ASSERT_EQ(BVGauss::getMinBwExpr(add4x), 18); - NodeBuilder<> nbadd5p(kind::BITVECTOR_PLUS); + NodeBuilder nbadd5p(kind::BITVECTOR_PLUS); nbadd5p << zext48p << zext48p8 << zext48p; Node add5p = nbadd5p; ASSERT_EQ(BVGauss::getMinBwExpr(add5p), 6); - NodeBuilder<> nbadd5x(kind::BITVECTOR_PLUS); + NodeBuilder nbadd5x(kind::BITVECTOR_PLUS); nbadd5x << zext48x << zext48x8 << zext48x; Node add5x = nbadd5x; ASSERT_EQ(BVGauss::getMinBwExpr(add5x), 18); - NodeBuilder<> nbadd6p(kind::BITVECTOR_PLUS); + NodeBuilder nbadd6p(kind::BITVECTOR_PLUS); nbadd6p << zext48p << zext48p << zext48p << zext48p; Node add6p = nbadd6p; ASSERT_EQ(BVGauss::getMinBwExpr(add6p), 6); - NodeBuilder<> nbadd6x(kind::BITVECTOR_PLUS); + NodeBuilder nbadd6x(kind::BITVECTOR_PLUS); nbadd6x << zext48x << zext48x << zext48x << zext48x; Node add6x = nbadd6x; ASSERT_EQ(BVGauss::getMinBwExpr(add6x), 18); diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index baacbce5a..97bbb1bcf 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -152,8 +152,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause) d_hfc, d_ac, d_d.andNode(d_b)); - out = NodeBuilder<>(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc - << d_ac << d_d.andNode(d_b); + out = NodeBuilder(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc + << d_ac << d_d.andNode(d_b); test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); in = d_nodeManager->mkNode(kind::OR, @@ -162,8 +162,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause) d_hfc, d_ac, d_d.andNode(d_b)); - out = NodeBuilder<>(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode() - << d_hfc << d_ac << d_d.andNode(d_b); + out = NodeBuilder(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode() + << d_hfc << d_ac << d_d.andNode(d_b); test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); #ifdef CVC4_ASSERTIONS @@ -207,7 +207,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause) d_ga.orNode(d_c).notNode(), d_hfc.orNode(d_ac), d_d.andNode(d_b).notNode())); - out = NodeBuilder<>(kind::OR) + out = NodeBuilder(kind::OR) << d_a.notNode() << d_b.notNode() << d_fa << d_ga.orNode(d_c).notNode() << d_hfc << d_ac << d_d.notNode(); test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in)); @@ -237,8 +237,8 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict) d_fa, d_hfc.orNode(d_ac), d_d.andNode(d_b)); - out = NodeBuilder<>(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode() - << d_hfc.orNode(d_ac) << d_d << d_b; + out = NodeBuilder(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode() + << d_hfc.orNode(d_ac) << d_d << d_b; test_nodes_equal(out, BooleanSimplification::simplifyConflict(in)); #ifdef CVC4_ASSERTIONS |