#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"
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();
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();
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();
node.h
node_algorithm.cpp
node_algorithm.h
+ node_builder.cpp
node_builder.h
node_manager.cpp
node_manager.h
}
}
}
- NodeBuilder<> nb(range.getKind());
+ NodeBuilder nb(range.getKind());
for (size_t i = 0, csize = children.size(); i < csize; ++i)
{
nb << children[i];
friend class TypeNode;
friend class NodeManager;
- template <unsigned nchild_thresh>
friend class NodeBuilder;
friend class ::cvc5::expr::attr::AttributeManager;
}
// otherwise compute
- NodeBuilder<> nb(getKind());
+ NodeBuilder nb(getKind());
if(getMetaKind() == kind::metakind::PARAMETERIZED) {
// push the operator
if(getOperator() == node) {
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,
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);
else if (it->second.isNull())
{
// build node
- NodeBuilder<> nb(curr.getKind());
+ NodeBuilder nb(curr.getKind());
if (curr.getMetaKind() == kind::metakind::PARAMETERIZED)
{
// push the operator
--- /dev/null
+/********************* */
+/*! \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 (CVC4_PREDICT_FALSE(nvIsAllocated()))
+ {
+ dealloc();
+ }
+ else if (CVC4_PREDICT_FALSE(!isUsed()))
+ {
+ 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 (CVC4_PREDICT_FALSE(nvIsAllocated()))
+ {
+ dealloc();
+ }
+ else if (CVC4_PREDICT_FALSE(!isUsed()))
+ {
+ 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 (CVC4_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
+ {
+ 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 (CVC4_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
+ {
+ 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 (CVC4_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
+ {
+ 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 (CVC4_PREDICT_FALSE(nvIsAllocated()))
+ {
+ // 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 == nullptr)
+ {
+ // 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 == nullptr)
+ {
+ 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 == nullptr)
+ {
+ 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 (CVC4_PREDICT_TRUE(!nvIsAllocated()))
+ {
+ /** 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 != nullptr)
+ {
+ /* 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 == nullptr)
+ {
+ 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 != nullptr)
+ {
+ /* 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 CVC4_PREDICT_FALSE(d_nv == nullptr); }
+
+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 = nullptr;
+}
+
+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 CVC4_PREDICT_FALSE(d_nv != &d_inlineNv)
+ && CVC4_PREDICT_TRUE(d_nv != nullptr);
+}
+
+bool NodeBuilder::nvNeedsToBeAllocated() const
+{
+ return CVC4_PREDICT_FALSE(d_nv->d_nchildren == d_nvMaxChildren);
+}
+
+void NodeBuilder::realloc()
+{
+ size_t newSize = 2 * size_t(d_nvMaxChildren);
+ size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
+ realloc(CVC4_PREDICT_FALSE(newSize > hardLimit) ? hardLimit : newSize);
+}
+
+void NodeBuilder::allocateNvIfNecessaryForAppend()
+{
+ if (CVC4_PREDICT_FALSE(nvNeedsToBeAllocated()))
+ {
+ realloc();
+ }
+}
+
+void NodeBuilder::crop()
+{
+ if (CVC4_PREDICT_FALSE(nvIsAllocated())
+ && CVC4_PREDICT_TRUE(d_nvMaxChildren > d_nv->d_nchildren))
+ {
+ // 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 == nullptr)
+ {
+ // 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
** 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,
** 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),
// "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());
/** 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) {
}
/** 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
}
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) {
}
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) {
}
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);
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);
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);
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);
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);
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) {
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) {
}
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;
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;
friend class expr::NodeValue;
friend class expr::TypeChecker;
- template <unsigned nchild_thresh>
friend class NodeBuilder;
friend class NodeManagerScope;
}
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();
}
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();
}
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;
}
}
inline Node* NodeManager::mkNodePtr(TNode opNode) {
- NodeBuilder<1> nb(this, operatorToKind(opNode));
+ NodeBuilder nb(this, operatorToKind(opNode));
if(opNode.getKind() != kind::BUILTIN) {
nb << 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;
}
}
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;
}
}
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;
}
}
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;
}
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;
}
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;
}
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;
}
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;
}
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;
}
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;
}
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;
}
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;
}
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>
template <bool ref_count> class NodeTemplate;
class TypeNode;
-template <unsigned N> class NodeBuilder;
+class NodeBuilder;
class NodeManager;
namespace expr {
template <bool>
friend class ::cvc5::NodeTemplate;
friend class ::cvc5::TypeNode;
- template <unsigned nchild_thresh>
friend class ::cvc5::NodeBuilder;
friend class ::cvc5::NodeManager;
}
// otherwise compute
- NodeBuilder<> nb(getKind());
+ NodeBuilder nb(getKind());
if(getMetaKind() == kind::metakind::PARAMETERIZED) {
// push the operator
nb << TypeNode(d_nv->d_children[0]);
friend class NodeManager;
- template <unsigned nchild_thresh>
friend class NodeBuilder;
/**
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]);
{
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)
/* 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);
default: Unhandled();
}
- NodeBuilder<> builder(new_kind);
+ NodeBuilder builder(new_kind);
for (unsigned i = 0; i < node.getNumChildren(); ++i)
{
builder << convertBvTerm(node[i]);
}
else
{
- NodeBuilder<> builder(current.getKind());
+ NodeBuilder builder(current.getKind());
if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << current.getOperator();
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();
{
// 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();
// 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();
}
// 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)
{
}
else
{
- NodeBuilder<> builder(current.getKind());
+ NodeBuilder builder(current.getKind());
if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << current.getOperator();
}
}
}
}
- NodeBuilder<> builder(newKind);
+ NodeBuilder builder(newKind);
if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << current.getOperator();
}
|| (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)
{
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(
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);
}
}
- NodeBuilder<> nb(kind::AND);
+ NodeBuilder nb(kind::AND);
Node curr = toCompress;
while (curr.getKind() == kind::ITE
&& (curr[1] == d_false || curr[2] == d_false)
}
}
- NodeBuilder<> nb(toCompress.getKind());
+ NodeBuilder nb(toCompress.getKind());
if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
{
else
{
bool ta = ite::isTheoryAtom(toCompress);
- NodeBuilder<> nb(toCompress.getKind());
+ NodeBuilder nb(toCompress.getKind());
if (toCompress.getMetaKind() == kind::metakind::PARAMETERIZED)
{
nb << (toCompress.getOperator());
return d_replaceOverCache[p];
}
- NodeBuilder<> builder(n.getKind());
+ NodeBuilder builder(n.getKind());
if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << n.getOperator();
}
else
{
- NodeBuilder<> nb(kind::OR);
+ NodeBuilder nb(kind::OR);
NodeVec::const_iterator it = intersection.begin(), end = intersection.end();
for (; it != end; ++it)
{
if (iteNode.getKind() == kind::ITE)
{
- NodeBuilder<> builder(kind::ITE);
+ NodeBuilder builder(kind::ITE);
builder << iteNode[0];
unsigned i = 1;
for (; i < iteNode.getNumChildren(); ++i)
return simpVar;
}
- NodeBuilder<> builder(c.getKind());
+ NodeBuilder builder(c.getKind());
if (c.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << c.getOperator();
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();
return e;
}
- NodeBuilder<> builder(e.getKind());
+ NodeBuilder builder(e.getKind());
if (e.getMetaKind() == kind::metakind::PARAMETERIZED)
{
builder << e.getOperator();
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]);
#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"
#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"
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;
#include "smt/preprocessor.h"
+#include "options/expr_options.h"
#include "options/smt_options.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "printer/printer.h"
#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"
return buffer[0];
}
- NodeBuilder<> nb(kind::AND);
+ NodeBuilder nb(kind::AND);
nb.append(buffer);
return nb;
}
return buffer[0];
}
- NodeBuilder<> nb(kind::OR);
+ NodeBuilder nb(kind::OR);
nb.append(buffer);
return nb;
}
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);
}
return n;
}
- NodeBuilder<> nb(n.getKind());
+ NodeBuilder nb(n.getKind());
if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
nb << n.getOperator();
// 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;
namespace arith {
Node ArithIteUtils::applyReduceVariablesInItes(Node n){
- NodeBuilder<> nb(n.getKind());
+ NodeBuilder nb(n.getKind());
if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
nb << (n.getOperator());
}
}
if(n.getNumChildren() > 0){
- NodeBuilder<> nb(n.getKind());
+ NodeBuilder nb(n.getKind());
if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
nb << (n.getOperator());
}
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;
}
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;
}
}
-
-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()){
}
}
-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()));
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);
}
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);
}
}
-void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
+void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned)
+{
Assert(n.getKind() == ITE);
Debug("arith::static") << "iteConstant(" << n << ")" << endl;
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;
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;
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;
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);
}
}
-inline Node safeConstructNary(NodeBuilder<>& nb) {
+inline Node safeConstructNary(NodeBuilder& nb)
+{
switch (nb.getNumChildren()) {
case 0:
return getIdentity(nb.getKind());
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);
//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"))
{
//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"))
}
}
-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) {
return trn;
}
-void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
+void ArithCongruenceManager::explain(TNode external, NodeBuilder& out)
+{
Node internal = externalToInternal(external);
std::vector<TNode> assumptions;
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);
<< 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);
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
*/
TrustNode explain(TNode literal);
- void explain(TNode lit, NodeBuilder<>& out);
+ void explain(TNode lit, NodeBuilder& out);
void addWatchedPair(ArithVar s, TNode x, TNode y);
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())
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())
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())
{
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);
}
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;
}
std::shared_ptr<ProofNode> Constraint::externalExplain(
- NodeBuilder<>& nb, AssertionOrder order) const
+ NodeBuilder& nb, AssertionOrder order) const
{
if (Debug.isOn("pf::arith::explain"))
{
}
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);
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
* 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);
}
* 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);
*/
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
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());
template <class GetNodeIterator>
inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
- NodeBuilder<> nb(k);
+ NodeBuilder nb(k);
while(start != end) {
nb << (*start).getNode();
// 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
// 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>();
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;
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);
}
* 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"); }
// 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);
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();
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();
}
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];
// 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.
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) {
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();
// 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;
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"); }
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,
// (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) {
// ... && 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)) {
// 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]);
return TrustNode::null();
}
d_ppEqualityEngine.addTerm(term);
+ NodeManager* nm = NodeManager::currentNM();
Node ret;
switch (term.getKind()) {
case kind::SELECT: {
// 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 = nm->mkNode(kind::SELECT, term[0][0], term[1]);
}
break;
}
// 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 = nm->mkNode(kind::STORE, term[0][0], term[1], term[2]);
+ Node outer = nm->mkNode(kind::STORE, inner, term[0][1], term[0][2]);
ret = outer;
}
break;
}
}
- 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) {
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)
{
return assertion;
}
- NodeBuilder<> result(assertion.getKind());
+ NodeBuilder result(assertion.getKind());
if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) {
result << assertion.getOperator();
}
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();
++(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;
// 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)
{
return sig;
}
- NodeBuilder<> builder(node.getKind());
+ NodeBuilder builder(node.getKind());
if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << node.getOperator();
}
return signature;
}
- NodeBuilder<> builder(signature.getKind());
+ NodeBuilder builder(signature.getKind());
if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) {
builder << signature.getOperator();
}
}
Assert(node.getType().isBitVector());
- NodeBuilder<> nb(node.getKind());
+ NodeBuilder nb(node.getKind());
if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
{
nb << node.getOperator();
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]);
}
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(){};
}
else if (it->second.isNull())
{
- NodeBuilder<> nb(cur.getKind());
+ NodeBuilder nb(cur.getKind());
if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
{
nb << cur.getOperator();
;
}
-void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned)
{
if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
{
TrustNode ppRewrite(TNode t) override;
- void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+ void ppStaticLearn(TNode in, NodeBuilder& learned) override;
void presolve() override;
// children already processed
if (head.childrenAdded) {
- NodeBuilder<> nb(current.getKind());
+ NodeBuilder nb(current.getKind());
std::vector<Node> reasons;
if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
return changed;
}
- NodeBuilder<> nb(kind::BITVECTOR_XOR);
+ NodeBuilder nb(kind::BITVECTOR_XOR);
for (unsigned i = 1; i < left.getNumChildren(); ++i) {
nb << left[i];
}
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];
return *literals.begin();
}
- NodeBuilder<> nb(kind::AND);
+ NodeBuilder nb(kind::AND);
for (TNodeSet::const_iterator it = literals.begin(); it!= literals.end(); ++it) {
nb << *it;
d_internal->notifySharedTerm(t);
}
-void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
+void TheoryBV::ppStaticLearn(TNode in, NodeBuilder& learned)
{
d_internal->ppStaticLearn(in, learned);
}
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;
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]);
}
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()) {
}
}
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());
}
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)
{
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);
}
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) {
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)
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];
}
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)
.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];
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();
{
return node;
}
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ NodeBuilder result(kind::BITVECTOR_CONCAT);
for (unsigned i = 0; i < repeat; ++i)
{
result << node;
{
return v[0];
}
- NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+ NodeBuilder result(kind::BITVECTOR_CONCAT);
result.append(v.rbegin(), v.rend());
return Node(result);
}
/* 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;
}
/* 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;
}
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);
{
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)
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];
}
}
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();
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;
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;
{
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;
{
Assert(upper >= lower);
- NodeBuilder<> construct(kind::BITVECTOR_EXTRACT);
+ NodeBuilder construct(kind::BITVECTOR_EXTRACT);
construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
BitVectorExtract(upper, lower))
<< *this;
} 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;
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) {
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;
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)
Node defaultShiftIC(Kind litk, Kind shk, Node s, Node t)
{
unsigned w;
- NodeBuilder<> nb(OR);
+ NodeBuilder nb(OR);
NodeManager* nm;
nm = NodeManager::currentNM();
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;
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();
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;
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];
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++)
{
// 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))
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,
// 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;
}
/** 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)
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)
}
else if (n.getKind() == REGEXP_CONCAT)
{
- NodeBuilder<> nb(PLUS);
+ NodeBuilder nb(PLUS);
for (const Node& nc : n)
{
Node flc = getFixedLengthForRegexp(nc);
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);
{
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)
{
{
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]);
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)
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);
}
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);
}
else if (a.getKind() == STRING_CONCAT)
{
- NodeBuilder<> nb(STRING_CONCAT);
+ NodeBuilder nb(STRING_CONCAT);
for (const Node& ac : a)
{
nb << getMultisetApproximation(ac);
cs.push_back(yiLen[0]);
}
- NodeBuilder<> nb(AND);
+ NodeBuilder nb(AND);
// (= x (str.++ y1' ... ym'))
if (!cs.empty())
{
}
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);
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)
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()]);
}
* *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 */
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;
}
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)
* 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
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();
Node newTerm = term;
if (!term.isClosure())
{
- NodeBuilder<> newNode(term.getKind());
+ NodeBuilder newNode(term.getKind());
if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
{
newNode << term.getOperator();
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();
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)
{
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;
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) {
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;
if(options::ufSymmetryBreaker()) {
d_symb.assertFormula(n);
}
-}/* TheoryUF::ppStaticLearn() */
+} /* TheoryUF::ppStaticLearn() */
EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
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;
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)
{
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());
"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)");
}
"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);
namespace {
Node level0(NodeManager* nm)
{
- NodeBuilder<> nb(kind::AND);
+ NodeBuilder nb(kind::AND);
Node x = nm->mkSkolem("x", nm->booleanType());
nb << x;
nb << x;
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)
{
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));
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);
{
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;
#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;
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);
#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)
}
arr << i_K;
-
ASSERT_EQ(arr[0], i_0);
ASSERT_EQ(arr[2], i_2);
for (unsigned i = 3; i < K; ++i)
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);
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);
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)
"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);
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);
TEST_F(TestNodeBlackNodeBuilder, leftist_building)
{
- NodeBuilder<> nb;
+ NodeBuilder nb;
Node a = d_nodeManager->mkSkolem("a", *d_boolTypeNode);
TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
{
- NodeBuilder<> nb;
+ NodeBuilder nb;
ASSERT_NO_THROW(nb.realloc(15));
ASSERT_NO_THROW(nb.realloc(25));
#include <string>
#include "base/check.h"
+#include "expr/node_builder.h"
#include "test_node.h"
namespace cvc5 {
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);
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();
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);
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);
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,
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
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));
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
projects / cvc5.git / commitdiff