Deprecating the unused convenience_node_builders.h (#203)

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 859d5a312e87c3f169ed73a3523b78e320215cae..2400468a22652b7dd768808ad5b0e62d9e65be09 100644 (file)
--- 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 (file)
index 48f45e6..0000000
--- 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 57cfa022103a832319f3913ddcfb39be27202686..2d45d03675cc79440c8d375b3447d96c301b8b4c 100644 (file)
--- 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 5debfa8b992fd812cc82823ff52cc6d1fba7731c..84fd5cb2de5329a133f25d620fb5a654d1248360 100644 (file)
--- 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 bd13bd87436947da30b587aec0315bbaf253dd19..478f0f94c288e6fc501f1dbefdf410231e72f73c 100644 (file)
--- 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"

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 88b229ab6bc20fa52c22d9cc6fe45860bbed2678..2aa6f402ddc63b8429732ea6bac60315cf522ed1 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -21,7 +21,6 @@
 #include <sstream>
 
 #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 271c4eadc41e8acb467f13b4ddeadc3460d513e6..a1dc7aacf686085825e5be440ec94a8a0150a319 100644 (file)
--- 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());