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