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.

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");