diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/grammar_black.h | 2 | ||||
-rw-r--r-- | test/unit/api/result_black.h | 2 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 2 | ||||
-rw-r--r-- | test/unit/expr/node_black.h | 54 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 3 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_white.h | 2 | ||||
-rw-r--r-- | test/unit/theory/evaluator_white.h | 4 | ||||
-rw-r--r-- | test/unit/theory/sequences_rewriter_white.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_bv_rewriter_white.h | 4 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_word_white.h | 4 |
10 files changed, 37 insertions, 44 deletions
diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h index f30f6b0ad..eee067ef2 100644 --- a/test/unit/api/grammar_black.h +++ b/test/unit/api/grammar_black.h @@ -37,7 +37,7 @@ class GrammarBlack : public CxxTest::TestSuite void GrammarBlack::setUp() { d_solver.reset(new Solver()); } -void GrammarBlack::tearDown() {} +void GrammarBlack::tearDown() { d_solver.reset(nullptr); } void GrammarBlack::testAddRule() { diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h index cbfc9cf23..f9f37a019 100644 --- a/test/unit/api/result_black.h +++ b/test/unit/api/result_black.h @@ -22,7 +22,7 @@ class ResultBlack : public CxxTest::TestSuite { public: void setUp() { d_solver.reset(new Solver()); } - void tearDown() override {} + void tearDown() override { d_solver.reset(nullptr); } void testIsNull(); void testEq(); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 4a7b74c8e..d10813f58 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -167,7 +167,7 @@ class SolverBlack : public CxxTest::TestSuite void SolverBlack::setUp() { d_solver.reset(new Solver()); } -void SolverBlack::tearDown() {} +void SolverBlack::tearDown() { d_solver.reset(nullptr); } void SolverBlack::testGetBooleanSort() { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 1b8a7c92f..91242322a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -22,6 +22,8 @@ #include <string> #include <vector> +#include "api/cvc4cpp.h" +#include "smt/smt_engine.h" #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" @@ -50,15 +52,13 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, int N, class NodeBlack : public CxxTest::TestSuite { private: - Options opts; NodeManager* d_nodeManager; - NodeManagerScope* d_scope; - TypeNode* d_booleanType; - TypeNode* d_realType; - + api::Solver* d_slv; public: void setUp() override { + // setup a SMT engine so that options are in scope + Options opts; char* argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-lang=ast"); @@ -66,18 +66,12 @@ class NodeBlack : public CxxTest::TestSuite { free(argv[0]); free(argv[1]); - d_nodeManager = new NodeManager(NULL, opts); - d_scope = new NodeManagerScope(d_nodeManager); - d_booleanType = new TypeNode(d_nodeManager->booleanType()); - d_realType = new TypeNode(d_nodeManager->realType()); + d_slv = new api::Solver(&opts); + d_nodeManager = d_slv->getSmtEngine()->getNodeManager(); } - void tearDown() override - { - delete d_realType; - delete d_booleanType; - delete d_scope; - delete d_nodeManager; + void tearDown() override { + delete d_slv; } bool imp(bool a, bool b) const { return (!a) || (b); } @@ -114,12 +108,12 @@ class NodeBlack : public CxxTest::TestSuite { void testOperatorEquals() { Node a, b, c; - b = d_nodeManager->mkSkolem("b", *d_booleanType); + b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", *d_booleanType); + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); TS_ASSERT(a == a); TS_ASSERT(a == b); @@ -148,12 +142,12 @@ class NodeBlack : public CxxTest::TestSuite { void testOperatorNotEquals() { Node a, b, c; - b = d_nodeManager->mkSkolem("b", *d_booleanType); + b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", *d_booleanType); + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); /*structed assuming operator == works */ TS_ASSERT(iff(a != a, !(a == a))); @@ -208,7 +202,7 @@ class NodeBlack : public CxxTest::TestSuite { void testOperatorAssign() { Node a, b; Node c = d_nodeManager->mkNode( - NOT, d_nodeManager->mkSkolem("c", *d_booleanType)); + NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType())); b = c; TS_ASSERT(b == c); @@ -324,8 +318,8 @@ class NodeBlack : public CxxTest::TestSuite { void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node a = d_nodeManager->mkSkolem("a", *d_booleanType); - Node b = d_nodeManager->mkSkolem("b", *d_booleanType); + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); Node cnd = d_nodeManager->mkNode(OR, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -383,8 +377,8 @@ class NodeBlack : public CxxTest::TestSuite { void testGetKind() { /*inline Kind getKind() const; */ - Node a = d_nodeManager->mkSkolem("a", *d_booleanType); - Node b = d_nodeManager->mkSkolem("b", *d_booleanType); + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, a); TS_ASSERT(NOT == n.getKind()); @@ -392,8 +386,8 @@ class NodeBlack : public CxxTest::TestSuite { n = d_nodeManager->mkNode(EQUAL, a, b); TS_ASSERT(EQUAL == n.getKind()); - Node x = d_nodeManager->mkSkolem("x", *d_realType); - Node y = d_nodeManager->mkSkolem("y", *d_realType); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType()); n = d_nodeManager->mkNode(PLUS, x, y); TS_ASSERT(PLUS == n.getKind()); @@ -470,9 +464,9 @@ class NodeBlack : public CxxTest::TestSuite { // test iterators void testIterator() { NodeBuilder<> b; - Node x = d_nodeManager->mkSkolem("x", *d_booleanType); - Node y = d_nodeManager->mkSkolem("y", *d_booleanType); - Node z = d_nodeManager->mkSkolem("z", *d_booleanType); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); + Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); Node n = b << x << y << z << kind::AND; { // iterator @@ -717,7 +711,7 @@ class NodeBlack : public CxxTest::TestSuite { // This is for demonstrating what a certain type of user error looks like. // Node level0(){ // NodeBuilder<> nb(kind::AND); - // Node x = d_nodeManager->mkSkolem("x", *d_booleanType); + // Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); // nb << x; // nb << x; // return Node(nb.constructNode()); diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 9d5a0fc8d..8668f746b 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -209,8 +209,7 @@ class ParserBlack d_solver.reset(new api::Solver(&d_options)); } - void tearDown() { - } + void tearDown() { d_solver.reset(nullptr); } private: InputLanguage d_lang; diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 4a30b4179..24dd5ae62 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -145,7 +145,7 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_satSolver = new FakeSatSolver(); d_cnfContext = new context::Context(); d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine); - ResourceManager * rm = d_nodeManager->getResourceManager(); + ResourceManager* rm = d_smt->getResourceManager(); d_cnfStream = new CVC4::prop::TseitinCnfStream( d_satSolver, d_cnfRegistrar, d_cnfContext, rm); } diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index 3fc95b2a5..0a50bae2d 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -48,9 +48,9 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); + d_em = new ExprManager; d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_smt->finalOptionsAreSet(); } diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index c9c897f5f..347289693 100644 --- a/test/unit/theory/sequences_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -46,8 +46,8 @@ class SequencesRewriterWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_em = new ExprManager; + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_smt->finalOptionsAreSet(); d_rewriter = new ExtendedRewriter(true); diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index d2284aa8f..e6110256a 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -40,8 +40,8 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_em = new ExprManager; + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_smt->finalOptionsAreSet(); diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index 2e29d50b8..048d1d707 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -37,8 +37,8 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_em = new ExprManager; + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_nm = NodeManager::currentNM(); |