Adding Node::getOperator()

Removing references to ExprManager from Type, moving Type creation into NodeManager

1 files changed, 59 insertions, 39 deletions

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 4731810ea..90358a622 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -18,6 +18,7 @@
 //Used in some of the tests
 #include <vector>
 
+#include "expr/expr_manager.h"
 #include "expr/node_value.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
@@ -30,19 +31,19 @@ using namespace std;
 class NodeBlack : public CxxTest::TestSuite {
 private:
 
+  NodeManager *d_nodeManager;
   NodeManagerScope *d_scope;
-  NodeManager *d_nm;
 
 public:
 
   void setUp() {
-    d_nm = new NodeManager();
-    d_scope = new NodeManagerScope(d_nm);
+    d_nodeManager = new NodeManager();
+    d_scope = new NodeManagerScope(d_nodeManager);
   }
 
   void tearDown() {
     delete d_scope;
-    delete d_nm;
+    delete d_nodeManager;
   }
 
   bool imp(bool a, bool b) const {
@@ -88,12 +89,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
     
-    b = d_nm->mkVar();
+    b = d_nodeManager->mkVar();
 
     a = b;
     c = a;
 
-    Node d = d_nm->mkVar();
+    Node d = d_nodeManager->mkVar();
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -128,12 +129,12 @@ public:
 
     Node a, b, c;
     
-    b = d_nm->mkVar();
+    b = d_nodeManager->mkVar();
 
     a = b;
     c = a;
 
-    Node d = d_nm->mkVar();
+    Node d = d_nodeManager->mkVar();
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a,!(a==a)));
@@ -168,9 +169,9 @@ public:
 #endif /* CVC4_ASSERTIONS */
 
     //Basic access check
-    Node tb = d_nm->mkNode(TRUE);
-    Node eb = d_nm->mkNode(FALSE);
-    Node cnd = d_nm->mkNode(XOR, tb, eb);
+    Node tb = d_nodeManager->mkNode(TRUE);
+    Node eb = d_nodeManager->mkNode(FALSE);
+    Node cnd = d_nodeManager->mkNode(XOR, tb, eb);
     Node ite = cnd.iteNode(tb,eb);
 
     TS_ASSERT(tb == cnd[0]);
@@ -190,7 +191,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nm->mkNode(NOT);
+    Node c = d_nodeManager->mkNode(NOT);
     
     b = c;
     TS_ASSERT(b==c);
@@ -208,14 +209,14 @@ public:
      */
 
     
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
+    Node a = d_nodeManager->mkVar();
+    Node b = d_nodeManager->mkVar();
 
     TS_ASSERT(a<b || b<a);
     TS_ASSERT(!(a<b && b<a));
 
-    Node c = d_nm->mkNode(NULL_EXPR);
-    Node d = d_nm->mkNode(NULL_EXPR);
+    Node c = d_nodeManager->mkNode(NULL_EXPR);
+    Node d = d_nodeManager->mkNode(NULL_EXPR);
 
     TS_ASSERT(!(c<d));
     TS_ASSERT(!(d<c));
@@ -228,18 +229,18 @@ public:
      */
     
     //Simple test of descending descendant property
-    Node child = d_nm->mkNode(TRUE);
-    Node parent = d_nm->mkNode(NOT, child);
+    Node child = d_nodeManager->mkNode(TRUE);
+    Node parent = d_nodeManager->mkNode(NOT, child);
 
     TS_ASSERT(child < parent);
 
     //Slightly less simple test of DD property.
     std::vector<Node> chain;
     int N = 500;
-    Node curr = d_nm->mkNode(NULL_EXPR);
+    Node curr = d_nodeManager->mkNode(NULL_EXPR);
     for(int i=0;i<N;i++) {
       chain.push_back(curr);
-      curr = d_nm->mkNode(AND,curr);
+      curr = d_nodeManager->mkNode(AND,curr);
     }
     
     for(int i=0;i<N;i++) {
@@ -254,8 +255,8 @@ public:
 
   void testHash() {
     /* Not sure how to test this except survial... */
-    Node a = d_nm->mkNode(ITE);
-    Node b = d_nm->mkNode(ITE);
+    Node a = d_nodeManager->mkNode(ITE);
+    Node b = d_nodeManager->mkNode(ITE);
     
     TS_ASSERT(b.hash() == a.hash());
   }
@@ -265,8 +266,8 @@ public:
   void testEqNode() {
     /*Node eqNode(const Node& right) const;*/
 
-    Node left = d_nm->mkNode(TRUE);
-    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node left = d_nodeManager->mkNode(TRUE);
+    Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node eq = left.eqNode(right);
     
 
@@ -280,7 +281,7 @@ public:
   void testNotNode() {
     /*  Node notNode() const;*/
 
-    Node child = d_nm->mkNode(TRUE);
+    Node child = d_nodeManager->mkNode(TRUE);
     Node parent = child.notNode();
 
     TS_ASSERT(NOT == parent.getKind());
@@ -292,8 +293,8 @@ public:
   void testAndNode() {
     /*Node andNode(const Node& right) const;*/
     
-    Node left = d_nm->mkNode(TRUE);
-    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node left = d_nodeManager->mkNode(TRUE);
+    Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node eq = left.andNode(right);
     
 
@@ -308,8 +309,8 @@ public:
   void testOrNode() {
     /*Node orNode(const Node& right) const;*/
      
-    Node left = d_nm->mkNode(TRUE);
-    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node left = d_nodeManager->mkNode(TRUE);
+    Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node eq = left.orNode(right);
     
 
@@ -324,9 +325,9 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node cnd = d_nm->mkNode(PLUS);
-    Node thenBranch = d_nm->mkNode(TRUE);
-    Node elseBranch = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node cnd = d_nodeManager->mkNode(PLUS);
+    Node thenBranch = d_nodeManager->mkNode(TRUE);
+    Node elseBranch = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node ite = cnd.iteNode(thenBranch,elseBranch);
     
 
@@ -341,8 +342,8 @@ public:
   void testIffNode() {
     /*  Node iffNode(const Node& right) const; */
      
-    Node left = d_nm->mkNode(TRUE);
-    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node left = d_nodeManager->mkNode(TRUE);
+    Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node eq = left.iffNode(right);
     
 
@@ -356,8 +357,8 @@ public:
   
   void testImpNode() {
     /* Node impNode(const Node& right) const; */
-    Node left = d_nm->mkNode(TRUE);
-    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node left = d_nodeManager->mkNode(TRUE);
+    Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node eq = left.impNode(right);
     
 
@@ -370,8 +371,8 @@ public:
 
   void testXorNode() {
     /*Node xorNode(const Node& right) const;*/
-    Node left = d_nm->mkNode(TRUE);
-    Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
+    Node left = d_nodeManager->mkNode(TRUE);
+    Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE)));
     Node eq = left.xorNode(right);
     
 
@@ -383,7 +384,7 @@ public:
   }
 
   void testKindSingleton(Kind k) {
-    Node n = d_nm->mkNode(k);
+    Node n = d_nodeManager->mkNode(k);
     TS_ASSERT(k == n.getKind());
   }
 
@@ -395,6 +396,25 @@ public:
     testKindSingleton(ITE);
     testKindSingleton(SKOLEM);
   }
+
+
+  void testGetOperator() {
+    const Type* sort = d_nodeManager->mkSort("T");
+    const Type* booleanType = d_nodeManager->booleanType();
+    const Type* predType = d_nodeManager->mkFunctionType(sort,booleanType);
+
+    Node f = d_nodeManager->mkVar(predType);
+    Node a = d_nodeManager->mkVar(booleanType);
+    Node fa = d_nodeManager->mkNode(kind::APPLY,f,a);
+
+    TS_ASSERT( fa.hasOperator() );
+    TS_ASSERT( !f.hasOperator() );
+    TS_ASSERT( !a.hasOperator() );
+
+    TS_ASSERT( f == fa.getOperator() );
+    TS_ASSERT_THROWS( f.getOperator(), AssertionException );
+    TS_ASSERT_THROWS( a.getOperator(), AssertionException );
+  }
   
   void testNaryExpForSize(Kind k, int N){
     NodeBuilder<> nbz(k);