unit test fixes for new NodeManager constructor (related to previous two trunk commits)

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index 06c8decfc32d28173df78e0752e5227e4bcb4f2c..a324bbbf1fe376ea9b75bd1ffeec9bc716ad19bd 100644 (file)
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -45,7 +45,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt);
+    d_nodeManager = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 448933622f94a6cec15cf44631a923af62a4c5aa..571be2789db6d852beb13952c0527452afb9f869 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -70,7 +70,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     d_booleanType = new TypeNode(d_nm->booleanType());

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 5389e1308f776620b4555c59f131773ae91476c7..6bd5aa1fd47ffb1104881331dc7b86bf817c0316 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -46,7 +46,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt);
+    d_nodeManager = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());

diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 49c9b7952ab84d9a2107bcaead814cef73052e2d..320d4ddbef6e0d0619ee31c9f35a13037af98f82 100644 (file)
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -50,7 +50,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     specKind = AND;

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index af79f5ff25613cdf2358f8aedfb5e5b7fa681783..e6ebc6724facdfc873e0dcb542ea151acc4d6613 100644 (file)
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -42,7 +42,7 @@ public:
 
   void setUp() {
     d_context = new Context;
-    d_nodeManager = new NodeManager(d_context);
+    d_nodeManager = new NodeManager(d_context, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 

diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 62fdeb45be6c92a796eff5fb6fff015b13a54db5..95d3271f2ed8818a167e4be6539cf01472dc2fa1 100644 (file)
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -40,7 +40,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context();
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 

diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index 4e7c198eeb037c152ab188fe6c8c53614282069b..e97407dfcb52d3bbe0bf0dae0d4a803ee936cd7e 100644 (file)
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nodeManager = new NodeManager(d_ctxt);
+    d_nodeManager = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 74413796a6a7d9edc1345ffa508a92f43ef7e781..9d6311acb982fe8b39dc8a4f1395e3b640251111 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context();
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 2e1a6d3f4a39da99e34e1aeca24534844cdaf35b..af9b7bd0f32a0ab005eee98f41e489623fc57d77 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -67,7 +67,7 @@ protected:
 //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
 //        istringstream stream(goodInputs[i]);
         Parser *parser =
-          ParserBuilder(*d_exprManager,"test")
+          ParserBuilder(d_exprManager,"test")
             .withStringInput(goodInput)
             .withInputLanguage(d_lang)
             .build();
@@ -94,7 +94,7 @@ protected:
 //      Debug.on("parser");
 
     Parser *parser =
-      ParserBuilder(*d_exprManager,"test")
+      ParserBuilder(d_exprManager,"test")
         .withStringInput(badInput)
         .withInputLanguage(d_lang)
         .withStrictMode(strictMode)
@@ -116,7 +116,7 @@ protected:
 //        istringstream stream(context + goodBooleanExprs[i]);
 
         Parser *parser =
-          ParserBuilder(*d_exprManager,"test")
+          ParserBuilder(d_exprManager,"test")
             .withStringInput(goodExpr)
             .withInputLanguage(d_lang)
             .build();
@@ -153,7 +153,7 @@ protected:
 //      cout << "Testing bad expr: '" << badExpr << "'\n";
 
       Parser *parser =
-        ParserBuilder(*d_exprManager,"test")
+        ParserBuilder(d_exprManager,"test")
           .withStringInput(badExpr)
           .withInputLanguage(d_lang)
           .withStrictMode(strictMode)

diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 06259ddb0893ecb5f311fa47d8094f8e37c78933..06b09f2ce79e20b4067503885c17c1328882419d 100644 (file)
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -92,7 +92,7 @@ public:
     /* fs.close(); */
 
     checkEmptyInput(
-      ParserBuilder(*d_exprManager,filename)
+      ParserBuilder(d_exprManager,filename)
         .withInputLanguage(LANG_CVC4)
                     );
 
@@ -108,7 +108,7 @@ public:
     fs.close();
 
     checkTrueInput(
-      ParserBuilder(*d_exprManager,filename)
+      ParserBuilder(d_exprManager,filename)
         .withInputLanguage(LANG_CVC4)
                    );
 
@@ -117,7 +117,7 @@ public:
 
   void testEmptyStringInput() {
     checkEmptyInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStringInput("")
                     );
@@ -125,7 +125,7 @@ public:
 
   void testTrueStringInput() {
     checkTrueInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStringInput("TRUE")
                    );
@@ -134,7 +134,7 @@ public:
   void testEmptyStreamInput() {
     stringstream ss( "", ios_base::in );
     checkEmptyInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStreamInput(ss)
                     );
@@ -143,7 +143,7 @@ public:
   void testTrueStreamInput() {
     stringstream ss( "TRUE", ios_base::in );
     checkTrueInput(
-      ParserBuilder(*d_exprManager,"foo")
+      ParserBuilder(d_exprManager,"foo")
         .withInputLanguage(LANG_CVC4)
         .withStreamInput(ss)
                    );

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index fffa36105b40785516fbe0736005dc5e0d926829..f6118d85c95bf103e96587a5a09bb8573f131d50 100644 (file)
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -104,7 +104,7 @@ class CnfStreamBlack : public CxxTest::TestSuite {
 
 void setUp() {
   d_context = new Context;
-  d_nodeManager = new NodeManager(d_context);
+  d_nodeManager = new NodeManager(d_context, NULL);
   NodeManagerScope nms(d_nodeManager);
   d_satSolver = new FakeSatSolver;
   d_theoryEngine = new TheoryEngine(d_context);

diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h
index e88f11673aff4d03db8caeb33a1f84fed0b768ca..0e8f5addb6a4fc799e8d4de5e909c83908cad57f 100644 (file)
--- a/test/unit/theory/shared_term_manager_black.h
+++ b/test/unit/theory/shared_term_manager_black.h
@@ -56,7 +56,7 @@ public:
   void setUp() {
     d_ctxt = new Context;
 
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     d_theoryEngine = new TheoryEngine(d_ctxt);

diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
index 39dad4732c8bd2b8f2f6966309b365abc02fd7ca..c60da29220d2256978546aff8957cb66e25d828b 100644 (file)
--- a/test/unit/theory/stacking_map_black.h
+++ b/test/unit/theory/stacking_map_black.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_map = new StackingMap<TNode, TNodeHashFunction>(d_ctxt);
 

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 9de8f94b40265183d151089eaf0701fb41a977b7..060c3036df619b56719921b3442af92d8c25d784 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -93,7 +93,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
     d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL));

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 1897bbd1c402085ea1b0b5bd543ed5a5e5bdcc60..2d39af95646b475f991b4a10563ed9b7529339ec 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -163,7 +163,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL));
     d_outputChannel.clear();

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 26908ec6e5e18b5305e1a4fb5f2cf0fafb1c7a59..f1a83cd496321b8f19c32dc54be8f61bed76015a 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -236,7 +236,7 @@ public:
   void setUp() {
     d_ctxt = new Context;
 
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
 
     d_nullChannel = new FakeOutputChannel;

diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h
index 1940bc199ca0230334018777b4021df4c391452c..ae3eee369d2e555edf321874e3fea36012c3e20d 100644 (file)
--- a/test/unit/theory/theory_uf_tim_white.h
+++ b/test/unit/theory/theory_uf_tim_white.h
@@ -58,7 +58,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
     d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL));

diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h
index b9b4e58cece0cf519fc2dc049aef81067f76ae6d..6ba6539468f99c9648dcde69215e2da404ead936 100644 (file)
--- a/test/unit/theory/union_find_black.h
+++ b/test/unit/theory/union_find_black.h
@@ -43,7 +43,7 @@ public:
 
   void setUp() {
     d_ctxt = new Context;
-    d_nm = new NodeManager(d_ctxt);
+    d_nm = new NodeManager(d_ctxt, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_uf = new UnionFind<TNode, TNodeHashFunction>(d_ctxt);
 

diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h
index a12cb79ead4c1b342d7d73c6d92ea9e0513cbdff..f5e299377570f256f374c047468fab5c5542038e 100644 (file)
--- a/test/unit/util/congruence_closure_white.h
+++ b/test/unit/util/congruence_closure_white.h
@@ -108,7 +108,7 @@ public:
 
   void setUp() {
     d_context = new Context;
-    d_nm = new NodeManager(d_context);
+    d_nm = new NodeManager(d_context, NULL);
     d_scope = new NodeManagerScope(d_nm);
     d_out = new MyOutputChannel(d_context, d_nm);
     d_cc = new CongruenceClosure<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >(d_context, d_out);