From 798524d033f69153d4bf6604e08c69a571771ae8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Nov 2020 14:49:55 -0600 Subject: [PATCH] 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. --- examples/api/combination.cpp | 4 ---- examples/api/python/combination.py | 3 --- src/api/cvc4cpp.cpp | 30 ++++++++++++++--------------- src/api/cvc4cpp.h | 17 ++++++++-------- src/api/python/cvc4.pxd | 1 - src/api/python/cvc4.pxi | 3 --- test/unit/api/solver_black.h | 31 +----------------------------- 7 files changed, 25 insertions(+), 64 deletions(-) diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 307c30709..0ac33c6dc 100644 --- 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 ed3fe0be5..f063d8c4e 100644 --- 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 1112530d3..16ec0935c 100644 --- 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 db57af121..eb55e4007 100644 --- 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 29f997394..19e7eb092 100644 --- 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 f945228dd..c44fc08af 100644 --- 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 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"); -- 2.30.2