Deprecating the unused convenience_node_builders.h (#203)

5 files changed, 0 insertions, 416 deletions

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<ref_count> 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 <bool rc>
-  inline AndNodeBuilder& operator&&(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline OrNodeBuilder operator||(const NodeTemplate<rc>&);
-
-  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 <bool rc>
-  inline AndNodeBuilder operator&&(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline OrNodeBuilder& operator||(const NodeTemplate<rc>&);
-
-  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 <bool rc>
-  inline PlusNodeBuilder& operator+(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline PlusNodeBuilder& operator-(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline MultNodeBuilder operator*(const NodeTemplate<rc>&);
-
-  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 <bool rc>
-  inline PlusNodeBuilder operator+(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline PlusNodeBuilder operator-(const NodeTemplate<rc>&);
-
-  template <bool rc>
-  inline MultNodeBuilder& operator*(const NodeTemplate<rc>&);
-
-  inline operator NodeBuilder<>() { return d_eb; }
-  inline operator Node() { return d_eb; }
-
-};/* class MultNodeBuilder */
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator&=(TNode e) {
-  return collapseTo(kind::AND).append(e);
-}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator|=(TNode e) {
-  return collapseTo(kind::OR).append(e);
-}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator+=(TNode e) {
-  return collapseTo(kind::PLUS).append(e);
-}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator-=(TNode e) {
-  return collapseTo(kind::PLUS).
-    append(NodeManager::currentNM()->mkNode(kind::UMINUS, e));
-}
-
-template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>& NodeBuilder<nchild_thresh>::operator*=(TNode e) {
-  return collapseTo(kind::MULT).append(e);
-}
-
-template <bool rc>
-inline AndNodeBuilder& AndNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-template <bool rc>
-inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) {
-  return OrNodeBuilder(Node(d_eb), n);
-}
-
-inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
-                                  const AndNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
-                                  const OrNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder operator||(AndNodeBuilder& a,
-                                const AndNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder operator||(AndNodeBuilder& a,
-                                const OrNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline AndNodeBuilder OrNodeBuilder::operator&&(const NodeTemplate<rc>& n) {
-  return AndNodeBuilder(Node(d_eb), n);
-}
-
-template <bool rc>
-inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-inline AndNodeBuilder operator&&(OrNodeBuilder& a,
-                                 const AndNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline AndNodeBuilder operator&&(OrNodeBuilder& a,
-                                 const OrNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder& operator||(OrNodeBuilder& a,
-                                 const AndNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline OrNodeBuilder& operator||(OrNodeBuilder& a,
-                                 const OrNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder& PlusNodeBuilder::operator+(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-template <bool rc>
-inline PlusNodeBuilder& PlusNodeBuilder::operator-(const NodeTemplate<rc>& n) {
-  d_eb.append(NodeManager::currentNM()->mkNode(kind::UMINUS, n));
-  return *this;
-}
-
-template <bool rc>
-inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) {
-  return MultNodeBuilder(Node(d_eb), n);
-}
-
-inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
-                                  const PlusNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
-                                  const MultNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder& operator-(PlusNodeBuilder&a,
-                                  const PlusNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder& operator-(PlusNodeBuilder& a,
-                                  const MultNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder operator*(PlusNodeBuilder& a,
-                                 const PlusNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder operator*(PlusNodeBuilder& a,
-                                 const MultNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) {
-  return PlusNodeBuilder(Node(d_eb), n);
-}
-
-template <bool rc>
-inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) {
-  return PlusNodeBuilder(Node(d_eb),
-                         NodeManager::currentNM()->mkNode(kind::UMINUS, n));
-}
-
-template <bool rc>
-inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) {
-  d_eb.append(n);
-  return *this;
-}
-
-inline PlusNodeBuilder operator+(MultNodeBuilder& a,
-                                 const PlusNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder operator+(MultNodeBuilder& a,
-                                 const MultNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder operator-(MultNodeBuilder& a,
-                                 const PlusNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline PlusNodeBuilder operator-(MultNodeBuilder& a,
-                                 const MultNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder& operator*(MultNodeBuilder& a,
-                                  const PlusNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-inline MultNodeBuilder& operator*(MultNodeBuilder& a,
-                                  const MultNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc1, bool rc2>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a,
-                                 const NodeTemplate<rc2>& b) {
-  return AndNodeBuilder(a, b);
-}
-
-template <bool rc1, bool rc2>
-inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a,
-                                const NodeTemplate<rc2>& b) {
-  return OrNodeBuilder(a, b);
-}
-
-template <bool rc1, bool rc2>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a,
-                                 const NodeTemplate<rc2>& b) {
-  return PlusNodeBuilder(a, b);
-}
-
-template <bool rc1, bool rc2>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a,
-                                 const NodeTemplate<rc2>& b) {
-  return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b));
-}
-
-template <bool rc1, bool rc2>
-inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a,
-                                 const NodeTemplate<rc2>& b) {
-  return MultNodeBuilder(a, b);
-}
-
-template <bool rc>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
-                                 const AndNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
-                                 const OrNodeBuilder& b) {
-  return a && Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
-                                const AndNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
-                                const OrNodeBuilder& b) {
-  return a || Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
-                                 const PlusNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
-                                 const MultNodeBuilder& b) {
-  return a + Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
-                                 const PlusNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
-                                 const MultNodeBuilder& b) {
-  return a - Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
-                                 const PlusNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
-                                 const MultNodeBuilder& b) {
-  return a * Node(const_cast<NodeBuilder<>&>(b.d_eb));
-}
-
-template <bool rc>
-inline NodeTemplate<true> operator-(const NodeTemplate<rc>& 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 <unsigned nchild_thresh>
@@ -728,11 +722,6 @@ public:
   NodeBuilder<nchild_thresh>& operator-=(TNode);
   NodeBuilder<nchild_thresh>& 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 <unsigned N>
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 <bool ref_count> class NodeTemplate;
 class TypeNode;
 template <unsigned N> 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 <vector>
 
 #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"