diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-02 09:09:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-02 09:09:15 -0700 |
commit | 50edf184492d20f4acb7b8d82f3843f3146f77d5 (patch) | |
tree | 2a1bbdbd59dc7aefca114b108c646eb6f2dd933e /test | |
parent | b826fc8ae95fc13c4e2be45e39961199392a4dda (diff) |
New C++ API: Keep reference to solver object in non-solver objects. (#4549)
This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/op_black.h | 2 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 6 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 14 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.h | 2 |
4 files changed, 12 insertions, 12 deletions
diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h index e99e8daf2..27ca7bb88 100644 --- a/test/unit/api/op_black.h +++ b/test/unit/api/op_black.h @@ -52,7 +52,7 @@ void OpBlack::testIsNull() void OpBlack::testOpFromKind() { - Op plus(PLUS); + Op plus(&d_solver, PLUS); TS_ASSERT(!plus.isIndexed()); TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 07b5c5aec..90d4c10c1 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -978,13 +978,13 @@ void SolverBlack::testGetOp() Term listhead = d_solver->mkTerm(APPLY_SELECTOR, headTerm, listcons1); TS_ASSERT(listnil.hasOp()); - TS_ASSERT_EQUALS(listnil.getOp(), APPLY_CONSTRUCTOR); + TS_ASSERT_EQUALS(listnil.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR)); TS_ASSERT(listcons1.hasOp()); - TS_ASSERT_EQUALS(listcons1.getOp(), APPLY_CONSTRUCTOR); + TS_ASSERT_EQUALS(listcons1.getOp(), Op(d_solver.get(), APPLY_CONSTRUCTOR)); TS_ASSERT(listhead.hasOp()); - TS_ASSERT_EQUALS(listhead.getOp(), APPLY_SELECTOR); + TS_ASSERT_EQUALS(listhead.getOp(), Op(d_solver.get(), APPLY_SELECTOR)); } void SolverBlack::testPush1() diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 78d6ee5cc..d8f022201 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -175,10 +175,10 @@ void TermBlack::testGetOp() Term extb = d_solver.mkTerm(ext, b); TS_ASSERT(ab.hasOp()); - TS_ASSERT_EQUALS(ab.getOp(), Op(SELECT)); + TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT)); TS_ASSERT(!ab.getOp().isIndexed()); // can compare directly to a Kind (will invoke Op constructor) - TS_ASSERT_EQUALS(ab.getOp(), SELECT); + TS_ASSERT_EQUALS(ab.getOp(), Op(&d_solver, SELECT)); TS_ASSERT(extb.hasOp()); TS_ASSERT(extb.getOp().isIndexed()); TS_ASSERT_EQUALS(extb.getOp(), ext); @@ -189,7 +189,7 @@ void TermBlack::testGetOp() TS_ASSERT(!f.hasOp()); TS_ASSERT_THROWS(f.getOp(), CVC4ApiException&); TS_ASSERT(fx.hasOp()); - TS_ASSERT_EQUALS(fx.getOp(), APPLY_UF); + TS_ASSERT_EQUALS(fx.getOp(), Op(&d_solver, APPLY_UF)); std::vector<Term> children(fx.begin(), fx.end()); // testing rebuild from op and children TS_ASSERT_EQUALS(fx, d_solver.mkTerm(fx.getOp(), children)); @@ -225,10 +225,10 @@ void TermBlack::testGetOp() TS_ASSERT(headTerm.hasOp()); TS_ASSERT(tailTerm.hasOp()); - TS_ASSERT_EQUALS(nilTerm.getOp(), APPLY_CONSTRUCTOR); - TS_ASSERT_EQUALS(consTerm.getOp(), APPLY_CONSTRUCTOR); - TS_ASSERT_EQUALS(headTerm.getOp(), APPLY_SELECTOR); - TS_ASSERT_EQUALS(tailTerm.getOp(), APPLY_SELECTOR); + TS_ASSERT_EQUALS(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + TS_ASSERT_EQUALS(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR)); + TS_ASSERT_EQUALS(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); + TS_ASSERT_EQUALS(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR)); // Test rebuilding children.clear(); diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 44bb9293b..2962439ff 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -111,7 +111,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite TS_ASSERT(parser != NULL); api::Term e = parser->nextExpression(); - TS_ASSERT_EQUALS(e, d_solver->getExprManager()->mkConst(true)); + TS_ASSERT_EQUALS(e, d_solver->mkTrue()); e = parser->nextExpression(); TS_ASSERT(e.isNull()); |