From: Tim King Date: Sun, 23 Jul 2017 03:02:44 +0000 (-0700) Subject: Deprecating the unused convenience_node_builders.h (#203) X-Git-Tag: cvc5-1.0.0~5708 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7785045ede376f7ee5a540ded9afdd7d3f57c47d;p=cvc5.git Deprecating the unused convenience_node_builders.h (#203) --- diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 859d5a312..2400468a2 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -26,7 +26,6 @@ libexpr_la_SOURCES = \ attribute.cpp \ attribute_internals.h \ attribute_unique_id.h \ - convenience_node_builders.h \ chain.h \ emptyset.cpp \ emptyset.h \ diff --git a/src/expr/convenience_node_builders.h b/src/expr/convenience_node_builders.h deleted file mode 100644 index 48f45e696..000000000 --- a/src/expr/convenience_node_builders.h +++ /dev/null @@ -1,399 +0,0 @@ -/********************* */ -/*! \file convenience_node_builders.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Paul Meng - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 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 Convenience node builders. - ** - ** These are convenience node builders for building AND, OR, PLUS, - ** and MULT expressions. - ** - ** \todo These should be moved into theory code (say, - ** src/theory/booleans/node_builders.h and - ** src/theory/arith/node_builders.h), but for now they're here - ** because their design requires CVC4::NodeBuilder to friend them. - **/ - -// TODO: add templatized NodeTemplate to all these 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 "cvc4_private.h" - -#ifndef __CVC4__CONVENIENCE_NODE_BUILDERS_H -#define __CVC4__CONVENIENCE_NODE_BUILDERS_H - -#include "expr/node_builder.h" - -namespace CVC4 { - -class AndNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline AndNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::AND); - } - - inline AndNodeBuilder(TNode a, TNode b) : d_eb(kind::AND) { - d_eb << a << b; - } - - template - inline AndNodeBuilder& operator&&(const NodeTemplate&); - - template - inline OrNodeBuilder operator||(const NodeTemplate&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class AndNodeBuilder */ - -class OrNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline OrNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::OR); - } - - inline OrNodeBuilder(TNode a, TNode b) : d_eb(kind::OR) { - d_eb << a << b; - } - - template - inline AndNodeBuilder operator&&(const NodeTemplate&); - - template - inline OrNodeBuilder& operator||(const NodeTemplate&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class OrNodeBuilder */ - -class PlusNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline PlusNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::PLUS); - } - - inline PlusNodeBuilder(TNode a, TNode b) : d_eb(kind::PLUS) { - d_eb << a << b; - } - - template - inline PlusNodeBuilder& operator+(const NodeTemplate&); - - template - inline PlusNodeBuilder& operator-(const NodeTemplate&); - - template - inline MultNodeBuilder operator*(const NodeTemplate&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class PlusNodeBuilder */ - -class MultNodeBuilder { -public: - NodeBuilder<> d_eb; - - inline MultNodeBuilder(const NodeBuilder<>& eb) : d_eb(eb) { - d_eb.collapseTo(kind::MULT); - } - - inline MultNodeBuilder(TNode a, TNode b) : d_eb(kind::MULT) { - d_eb << a << b; - } - - template - inline PlusNodeBuilder operator+(const NodeTemplate&); - - template - inline PlusNodeBuilder operator-(const NodeTemplate&); - - template - inline MultNodeBuilder& operator*(const NodeTemplate&); - - inline operator NodeBuilder<>() { return d_eb; } - inline operator Node() { return d_eb; } - -};/* class MultNodeBuilder */ - -template -inline NodeBuilder& NodeBuilder::operator&=(TNode e) { - return collapseTo(kind::AND).append(e); -} - -template -inline NodeBuilder& NodeBuilder::operator|=(TNode e) { - return collapseTo(kind::OR).append(e); -} - -template -inline NodeBuilder& NodeBuilder::operator+=(TNode e) { - return collapseTo(kind::PLUS).append(e); -} - -template -inline NodeBuilder& NodeBuilder::operator-=(TNode e) { - return collapseTo(kind::PLUS). - append(NodeManager::currentNM()->mkNode(kind::UMINUS, e)); -} - -template -inline NodeBuilder& NodeBuilder::operator*=(TNode e) { - return collapseTo(kind::MULT).append(e); -} - -template -inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate& n) { - d_eb.append(n); - return *this; -} - -template -inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate& n) { - return OrNodeBuilder(Node(d_eb), n); -} - -inline AndNodeBuilder& operator&&(AndNodeBuilder& a, - const AndNodeBuilder& b) { - return a && Node(const_cast&>(b.d_eb)); -} -inline AndNodeBuilder& operator&&(AndNodeBuilder& a, - const OrNodeBuilder& b) { - return a && Node(const_cast&>(b.d_eb)); -} -inline OrNodeBuilder operator||(AndNodeBuilder& a, - const AndNodeBuilder& b) { - return a || Node(const_cast&>(b.d_eb)); -} -inline OrNodeBuilder operator||(AndNodeBuilder& a, - const OrNodeBuilder& b) { - return a || Node(const_cast&>(b.d_eb)); -} - -template -inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate& n) { - return AndNodeBuilder(Node(d_eb), n); -} - -template -inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate& n) { - d_eb.append(n); - return *this; -} - -inline AndNodeBuilder operator&&(OrNodeBuilder& a, - const AndNodeBuilder& b) { - return a && Node(const_cast&>(b.d_eb)); -} -inline AndNodeBuilder operator&&(OrNodeBuilder& a, - const OrNodeBuilder& b) { - return a && Node(const_cast&>(b.d_eb)); -} -inline OrNodeBuilder& operator||(OrNodeBuilder& a, - const AndNodeBuilder& b) { - return a || Node(const_cast&>(b.d_eb)); -} -inline OrNodeBuilder& operator||(OrNodeBuilder& a, - const OrNodeBuilder& b) { - return a || Node(const_cast&>(b.d_eb)); -} - -template -inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate& n) { - d_eb.append(n); - return *this; -} - -template -inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate& n) { - d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n)); - return *this; -} - -template -inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate& n) { - return MultNodeBuilder(Node(d_eb), n); -} - -inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast&>(b.d_eb)); -} -inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a + Node(const_cast&>(b.d_eb)); -} -inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, - const PlusNodeBuilder& b) { - return a - Node(const_cast&>(b.d_eb)); -} -inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a - Node(const_cast&>(b.d_eb)); -} -inline MultNodeBuilder operator*(PlusNodeBuilder& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast&>(b.d_eb)); -} -inline MultNodeBuilder operator*(PlusNodeBuilder& a, - const MultNodeBuilder& b) { - return a * Node(const_cast&>(b.d_eb)); -} - -template -inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate& n) { - return PlusNodeBuilder(Node(d_eb), n); -} - -template -inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate& n) { - return PlusNodeBuilder(Node(d_eb), - NodeManager::currentNM()->mkNode(kind::UMINUS, n)); -} - -template -inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate& n) { - d_eb.append(n); - return *this; -} - -inline PlusNodeBuilder operator+(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast&>(b.d_eb)); -} -inline PlusNodeBuilder operator+(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a + Node(const_cast&>(b.d_eb)); -} -inline PlusNodeBuilder operator-(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a - Node(const_cast&>(b.d_eb)); -} -inline PlusNodeBuilder operator-(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a - Node(const_cast&>(b.d_eb)); -} -inline MultNodeBuilder& operator*(MultNodeBuilder& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast&>(b.d_eb)); -} -inline MultNodeBuilder& operator*(MultNodeBuilder& a, - const MultNodeBuilder& b) { - return a * Node(const_cast&>(b.d_eb)); -} - -template -inline AndNodeBuilder operator&&(const NodeTemplate& a, - const NodeTemplate& b) { - return AndNodeBuilder(a, b); -} - -template -inline OrNodeBuilder operator||(const NodeTemplate& a, - const NodeTemplate& b) { - return OrNodeBuilder(a, b); -} - -template -inline PlusNodeBuilder operator+(const NodeTemplate& a, - const NodeTemplate& b) { - return PlusNodeBuilder(a, b); -} - -template -inline PlusNodeBuilder operator-(const NodeTemplate& a, - const NodeTemplate& b) { - return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b)); -} - -template -inline MultNodeBuilder operator*(const NodeTemplate& a, - const NodeTemplate& b) { - return MultNodeBuilder(a, b); -} - -template -inline AndNodeBuilder operator&&(const NodeTemplate& a, - const AndNodeBuilder& b) { - return a && Node(const_cast&>(b.d_eb)); -} - -template -inline AndNodeBuilder operator&&(const NodeTemplate& a, - const OrNodeBuilder& b) { - return a && Node(const_cast&>(b.d_eb)); -} - -template -inline OrNodeBuilder operator||(const NodeTemplate& a, - const AndNodeBuilder& b) { - return a || Node(const_cast&>(b.d_eb)); -} - -template -inline OrNodeBuilder operator||(const NodeTemplate& a, - const OrNodeBuilder& b) { - return a || Node(const_cast&>(b.d_eb)); -} - -template -inline PlusNodeBuilder operator+(const NodeTemplate& a, - const PlusNodeBuilder& b) { - return a + Node(const_cast&>(b.d_eb)); -} - -template -inline PlusNodeBuilder operator+(const NodeTemplate& a, - const MultNodeBuilder& b) { - return a + Node(const_cast&>(b.d_eb)); -} - -template -inline PlusNodeBuilder operator-(const NodeTemplate& a, - const PlusNodeBuilder& b) { - return a - Node(const_cast&>(b.d_eb)); -} - -template -inline PlusNodeBuilder operator-(const NodeTemplate& a, - const MultNodeBuilder& b) { - return a - Node(const_cast&>(b.d_eb)); -} - -template -inline MultNodeBuilder operator*(const NodeTemplate& a, - const PlusNodeBuilder& b) { - return a * Node(const_cast&>(b.d_eb)); -} - -template -inline MultNodeBuilder operator*(const NodeTemplate& a, - const MultNodeBuilder& b) { - return a * Node(const_cast&>(b.d_eb)); -} - -template -inline NodeTemplate operator-(const NodeTemplate& a) { - return NodeManager::currentNM()->mkNode(kind::UMINUS, a); -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__CONVENIENCE_NODE_BUILDERS_H */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 57cfa0221..2d45d0367 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -179,12 +179,6 @@ namespace CVC4 { namespace CVC4 { -/* see expr/convenience_node_builders.h */ -class AndNodeBuilder; -class OrNodeBuilder; -class PlusNodeBuilder; -class MultNodeBuilder; - // Sometimes it's useful for debugging to output a NodeBuilder that // isn't yet a Node.. template @@ -728,11 +722,6 @@ public: NodeBuilder& operator-=(TNode); NodeBuilder& operator*=(TNode); - friend class AndNodeBuilder; - friend class OrNodeBuilder; - friend class PlusNodeBuilder; - friend class MultNodeBuilder; - // This is needed for copy constructors of different sizes to access // private fields template diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 5debfa8b9..84fd5cb2d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -39,10 +39,6 @@ namespace CVC4 { template class NodeTemplate; class TypeNode; template class NodeBuilder; -class AndNodeBuilder; -class OrNodeBuilder; -class PlusNodeBuilder; -class MultNodeBuilder; class NodeManager; namespace expr { diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index bd13bd874..478f0f94c 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -18,7 +18,6 @@ #include #include "base/output.h" -#include "expr/convenience_node_builders.h" #include "expr/expr.h" #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 88b229ab6..2aa6f402d 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -21,7 +21,6 @@ #include #include "base/cvc4_assert.h" -#include "expr/convenience_node_builders.h" #include "expr/kind.h" #include "expr/node.h" #include "expr/node_builder.h" @@ -622,80 +621,4 @@ public: TS_ASSERT_EQUALS(nexpected, n); } - - void testConvenienceBuilders() { - Node a = d_nm->mkSkolem("a", *d_booleanType); - - Node b = d_nm->mkSkolem("b", *d_booleanType); - Node c = d_nm->mkSkolem("c", *d_booleanType); - - Node d = d_nm->mkSkolem("d", *d_realType); - Node e = d_nm->mkSkolem("e", *d_realType); - Node f = d_nm->mkSkolem("f", *d_realType); - - Node m = a && b; - TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); - - Node n = (a && b) || c; - TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c)); - - Node p = (a && m) || n; - TS_ASSERT_EQUALS(p, d_nm->mkNode(OR, d_nm->mkNode(AND, a, m), n)); - - Node w = d + e - f; - TS_ASSERT_EQUALS(w, d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f))); - - Node x = d + e + w - f; - TS_ASSERT_EQUALS(x, d_nm->mkNode(PLUS, d, e, w, d_nm->mkNode(UMINUS, f))); - - Node y = f - x - e + w; - TS_ASSERT_EQUALS(y, d_nm->mkNode(PLUS, - f, - d_nm->mkNode(UMINUS, x), - d_nm->mkNode(UMINUS, e), - w)); - - Node q = a && b && c; - TS_ASSERT_EQUALS(q, d_nm->mkNode(AND, a, b, c)); - - Node r = (c && b && a) || (m && n) || p || (a && p); - TS_ASSERT_EQUALS(r, d_nm->mkNode(OR, - d_nm->mkNode(AND, c, b, a), - d_nm->mkNode(AND, m, n), - p, - d_nm->mkNode(AND, a, p))); - - TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c)); - TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); - TS_ASSERT_EQUALS(Node((a || b) || c), d_nm->mkNode(OR, a, b, c)); - TS_ASSERT_EQUALS(Node(a || (b || c)), d_nm->mkNode(OR, a, d_nm->mkNode(OR, b, c))); - TS_ASSERT_EQUALS(Node((a && b) || c), d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); - TS_ASSERT_EQUALS(Node(a && (b || c)), d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); - TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); - TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); - - TS_ASSERT_EQUALS(Node((d + e) + f), d_nm->mkNode(PLUS, d, e, f)); - TS_ASSERT_EQUALS(Node(d + (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, f))); - TS_ASSERT_EQUALS(Node((d - e) - f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), d_nm->mkNode(UMINUS, f))); - TS_ASSERT_EQUALS(Node(d - (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f))))); - TS_ASSERT_EQUALS(Node((d * e) * f), d_nm->mkNode(MULT, d, e, f)); - TS_ASSERT_EQUALS(Node(d * (e * f)), d_nm->mkNode(MULT, d, d_nm->mkNode(MULT, e, f))); - TS_ASSERT_EQUALS(Node((d + e) - f), d_nm->mkNode(PLUS, d, e, d_nm->mkNode(UMINUS, f))); - TS_ASSERT_EQUALS(Node(d + (e - f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f)))); - TS_ASSERT_EQUALS(Node((d - e) + f), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e), f)); - TS_ASSERT_EQUALS(Node(d - (e + f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, e, f)))); - TS_ASSERT_EQUALS(Node((d + e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, e), f)); - TS_ASSERT_EQUALS(Node(d + (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(MULT, e, f))); - TS_ASSERT_EQUALS(Node((d - e) * f), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, e)), f)); - TS_ASSERT_EQUALS(Node(d - (e * f)), d_nm->mkNode(PLUS, d, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, e, f)))); - TS_ASSERT_EQUALS(Node((d * e) + f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), f)); - TS_ASSERT_EQUALS(Node(d * (e + f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, f))); - TS_ASSERT_EQUALS(Node((d * e) - f), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, d, e), d_nm->mkNode(UMINUS, f))); - TS_ASSERT_EQUALS(Node(d * (e - f)), d_nm->mkNode(MULT, d, d_nm->mkNode(PLUS, e, d_nm->mkNode(UMINUS, f)))); - - TS_ASSERT_EQUALS(Node(-d), d_nm->mkNode(UMINUS, d)); - TS_ASSERT_EQUALS(Node(- d - e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), d_nm->mkNode(UMINUS, e))); - TS_ASSERT_EQUALS(Node(- d + e), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, d), e)); - TS_ASSERT_EQUALS(Node(- d * e), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, d), e)); - } }; diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 271c4eadc..a1dc7aacf 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -19,7 +19,6 @@ #include "expr/node.h" #include "expr/node_self_iterator.h" #include "expr/node_builder.h" -#include "expr/convenience_node_builders.h" using namespace CVC4; using namespace CVC4::kind; @@ -52,7 +51,7 @@ public: void testSelfIteration() { Node x = d_nodeManager->mkSkolem("x", *d_booleanType); Node y = d_nodeManager->mkSkolem("y", *d_booleanType); - Node x_and_y = x && y; + Node x_and_y = x.andNode(y); NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y); TS_ASSERT(i != x_and_y.end()); TS_ASSERT(j != x_and_y.end());