From 7785045ede376f7ee5a540ded9afdd7d3f57c47d Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 22 Jul 2017 20:02:44 -0700 Subject: Deprecating the unused convenience_node_builders.h (#203) --- src/expr/Makefile.am | 1 - src/expr/convenience_node_builders.h | 399 ----------------------------------- src/expr/node_builder.h | 11 - src/expr/node_value.h | 4 - 4 files changed, 415 deletions(-) delete mode 100644 src/expr/convenience_node_builders.h (limited to 'src/expr') 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 { -- cgit v1.2.3