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.

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 307c307096eb430efb41015e54869978ae7c62b0..0ac33c6dc6ca40bbbadccbd74748dcc714e7cff2 100644 (file)
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -106,10 +106,6 @@ int main()
        << endl;
   prefixPrintGetValue(slv, assertions);
 
-  cout << endl << endl << "Alternatively, print the model." << endl << endl;
-
-  slv.printModel(cout);
-
   cout << endl;
   cout << "You can also use nested loops to iterate over terms." << endl;
   for (Term::const_iterator it = assertions.begin();

diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index ed3fe0be59e3ec2c13de53e41c1f359a0203c2b4..f063d8c4e0af42a163a9cb4437aeb090d7d4503f 100644 (file)
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -86,9 +86,6 @@ if __name__ == "__main__":
           " slv.getValue(...) on all terms")
     prefixPrintGetValue(slv, assertions)
 
-    print("Alternatively, print the model", "\n")
-    slv.printModel()
-
     print()
     print("You can also use nested loops to iterate over terms")
     for a in assertions:

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 1112530d359bf2621f99ab078f2727d9ab35e434..16ec0935c80f5bfb44e77cc4c4fd10ab1d5c7760 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4143,8 +4143,21 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
   CVC4_API_SOLVER_CHECK_SORT(sort);
 
-  Expr res = symbol.empty() ? d_exprMgr->mkVar(sort.d_type->toType())
-                            : d_exprMgr->mkVar(symbol, sort.d_type->toType());
+  Expr res = d_exprMgr->mkVar(symbol, sort.d_type->toType());
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+Term Solver::mkConst(Sort sort) const
+{
+  NodeManagerScope scope(getNodeManager());
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+  CVC4_API_SOLVER_CHECK_SORT(sort);
+
+  Expr res = d_exprMgr->mkVar(sort.d_type->toType());
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);
 
@@ -5323,19 +5336,6 @@ bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-void Solver::printModel(std::ostream& out) const
-{
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
-  CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
-      << "Cannot get value unless model generation is enabled "
-         "(try --produce-models)";
-  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
-      << "Can only get value after sat or unknown response.";
-  out << *d_smtEngine->getModel();
-  CVC4_API_SOLVER_TRY_CATCH_END;
-}
-
 void Solver::blockModel() const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index db57af121987fea23c6d2cdde5b06b78efc56434..eb55e4007cfb4dd8d8b37f2cb1cbcc5ac862a7ee 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2829,7 +2829,15 @@ class CVC4_PUBLIC Solver
    * @param symbol the name of the constant
    * @return the first-order constant
    */
-  Term mkConst(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkConst(Sort sort, const std::string& symbol) const;
+  /**
+   * Create (first-order) constant (0-arity function symbol), with a default
+   * symbol name.
+   *
+   * @param sort the sort of the constant
+   * @return the first-order constant
+   */
+  Term mkConst(Sort sort) const;
 
   /**
    * Create a bound variable to be used in a binder (i.e. a quantifier, a
@@ -3233,13 +3241,6 @@ class CVC4_PUBLIC Solver
    */
   bool getAbduct(Term conj, Grammar& g, Term& output) const;
 
-  /**
-   * Print the model of a satisfiable query to the given output stream.
-   * Requires to enable option 'produce-models'.
-   * @param out the output stream
-   */
-  void printModel(std::ostream& out) const;
-
   /**
    * Block the current model. Can be called only if immediately preceded by a
    * SAT or INVALID query.

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 29f997394180891253957ae3c762a913d5723b0d..19e7eb09226e7597bacdd7b8272e7a03c9a230dd 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -239,7 +239,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term getSeparationHeap() except +
         Term getSeparationNilTerm() except +
         void pop(uint32_t nscopes) except +
-        void printModel(ostream& out)
         void push(uint32_t nscopes) except +
         void reset() except +
         void resetAssertions() except +

diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index f945228dd62d97bf9757dbe9f2e083f2890004ff..c44fc08af73d377950e6f033f6d6680a489a64fc 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -1133,9 +1133,6 @@ cdef class Solver:
     def pop(self, nscopes=1):
         self.csolver.pop(nscopes)
 
-    def printModel(self):
-        self.csolver.printModel(cout)
-
     def push(self, nscopes=1):
         self.csolver.push(nscopes)
 

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index f292acc880e1e7c47a96e1c307e6097f8e07ff2f..b3af67a8cf77c82cab10cd7acf84b7f5ea631111 100644 (file)
--- 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");