From: Morgan Deters Date: Sat, 16 Apr 2011 00:10:57 +0000 (+0000) Subject: unit test fixes for new NodeManager constructor (related to previous two trunk commits) X-Git-Tag: cvc5-1.0.0~8594 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=718ea1851ab2b79816ed6c858e7f543556402084;p=cvc5.git 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 06c8decfc..a324bbbf1 100644 --- 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 448933622..571be2789 100644 --- 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 5389e1308..6bd5aa1fd 100644 --- 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 49c9b7952..320d4ddbe 100644 --- 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 af79f5ff2..e6ebc6724 100644 --- 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 62fdeb45b..95d3271f2 100644 --- 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 4e7c198ee..e97407dfc 100644 --- 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 74413796a..9d6311acb 100644 --- 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 2e1a6d3f4..af9b7bd0f 100644 --- 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 06259ddb0..06b09f2ce 100644 --- 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 fffa36105..f6118d85c 100644 --- 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 e88f11673..0e8f5addb 100644 --- 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 39dad4732..c60da2922 100644 --- 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(d_ctxt); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 9de8f94b4..060c3036d 100644 --- 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 1897bbd1c..2d39af956 100644 --- 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 26908ec6e..f1a83cd49 100644 --- 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 1940bc199..ae3eee369 100644 --- 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 b9b4e58ce..6ba653946 100644 --- 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(d_ctxt); diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index a12cb79ea..f5e299377 100644 --- 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 >(d_context, d_out);