diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-20 14:49:55 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-20 14:49:55 -0600 |
commit | 798524d033f69153d4bf6604e08c69a571771ae8 (patch) | |
tree | d00e5a0f67a2b03f1cdbd289d3d3ae2ba7146c63 /test/unit | |
parent | 89420525dd8417f32446aa9cd9a18ecd211cc119 (diff) |
Updates to API in preparation for using symbol manager for model (#5481)
printModel no longer makes sense if the list of declared symbols is managed outside the solver.
Also, mkConst needs a variant to distinguish a provided name of "" vs. a name that is not provided.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/solver_black.h | 31 |
1 files changed, 1 insertions, 30 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index f292acc88..b3af67a8c 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -141,9 +141,6 @@ class SolverBlack : public CxxTest::TestSuite void testPop1(); void testPop2(); void testPop3(); - void testPrintModel1(); - void testPrintModel2(); - void testPrintModel3(); void testBlockModel1(); void testBlockModel2(); @@ -194,7 +191,7 @@ void SolverBlack::testRecoverableException() d_solver->setOption("produce-models", "true"); Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); d_solver->assertFormula(x.eqTerm(x).notTerm()); - TS_ASSERT_THROWS(d_solver->printModel(std::cout), + TS_ASSERT_THROWS(d_solver->getValue(x), CVC4ApiRecoverableException&); } @@ -1864,32 +1861,6 @@ void SolverBlack::testPop3() TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&); } -void SolverBlack::testPrintModel1() -{ - d_solver->setOption("produce-models", "false"); - Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); - d_solver->assertFormula(x.eqTerm(x)); - TS_ASSERT_THROWS(d_solver->printModel(std::cout), CVC4ApiException&); -} - -void SolverBlack::testPrintModel2() -{ - d_solver->setOption("produce-models", "true"); - Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - d_solver->checkSat(); - TS_ASSERT_THROWS(d_solver->printModel(std::cout), CVC4ApiException&); -} - -void SolverBlack::testPrintModel3() -{ - d_solver->setOption("produce-models", "true"); - Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); - d_solver->assertFormula(x.eqTerm(x)); - d_solver->checkSat(); - TS_ASSERT_THROWS_NOTHING(d_solver->printModel(std::cout)); -} - void SolverBlack::testBlockModel1() { d_solver->setOption("produce-models", "true"); |