diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-06-04 11:07:41 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-04 11:07:41 -0700 |
commit | f0169b253759632aee0d21db916fe68702c66116 (patch) | |
tree | f806af9648d17b9fed38897330b208b58a0f5184 | |
parent | c5bf818456ebe2dee833fecd4a0970f0105919f0 (diff) |
New C++ Api: Second and last batch of API guards. (#4563)
This adds the remaining API guards in the Solver object (incl. unit tests).
-rw-r--r-- | src/api/cvc4cpp.cpp | 294 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 102 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 48 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 334 |
4 files changed, 634 insertions, 144 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index f225da333..734fcddae 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4194,8 +4194,10 @@ Term Solver::declareFun(const std::string& symbol, */ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol)); return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity)); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4206,26 +4208,28 @@ Term Solver::defineFun(const std::string& symbol, Sort sort, Term term) const { - // CHECK: - // for bv in bound_vars: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(bv.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) - // CHECK: not recursive + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as codomain sort for function sort"; - // CHECK: - // for v in bound_vars: is bound var std::vector<Type> domain_types; for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + bound_vars[i], + i) + << "a bound variable"; CVC4::Type t = bound_vars[i].d_expr->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; domain_types.push_back(t); } + CVC4_API_SOLVER_CHECK_SORT(sort); CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; @@ -4238,17 +4242,14 @@ Term Solver::defineFun(const std::string& symbol, std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr); return Term(this, fun); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::defineFun(Term fun, const std::vector<Term>& bound_vars, Term term) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(bv.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts(); size_t size = bound_vars.size(); @@ -4257,6 +4258,15 @@ Term Solver::defineFun(Term fun, for (size_t i = 0; i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + bound_vars[i], + i) + << "a bound variable"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( domain_sorts[i] == bound_vars[i].getSort(), "sort of parameter", bound_vars[i], @@ -4264,16 +4274,15 @@ Term Solver::defineFun(Term fun, << "'" << domain_sorts[i] << "'"; } Sort codomain = fun.getSort().getFunctionCodomainSort(); + CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_CHECK(codomain == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << codomain << "'"; - // CHECK: not recursive - // CHECK: - // for v in bound_vars: is bound var std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr); return fun; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4284,29 +4293,33 @@ Term Solver::defineFunRec(const std::string& symbol, Sort sort, Term term) const { - // CHECK: - // for bv in bound_vars: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(bv.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) << "first-class sort as function codomain sort"; Assert(!sort.isFunction()); /* A function sort is not first-class. */ - // CHECK: - // for v in bound_vars: is bound var std::vector<Type> domain_types; for (size_t i = 0, size = bound_vars.size(); i < size; ++i) { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + bound_vars[i], + i) + << "a bound variable"; CVC4::Type t = bound_vars[i].d_expr->getType(); CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( t.isFirstClass(), "sort of parameter", bound_vars[i], i) << "first-class sort of parameter of defined function"; domain_types.push_back(t); } + CVC4_API_SOLVER_CHECK_SORT(sort); CVC4_API_CHECK(sort == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << sort << "'"; + CVC4_API_SOLVER_CHECK_TERM(term); Type type = *sort.d_type; if (!domain_types.empty()) { @@ -4316,18 +4329,14 @@ Term Solver::defineFunRec(const std::string& symbol, std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr); return Term(this, fun); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::defineFunRec(Term fun, const std::vector<Term>& bound_vars, Term term) const { - // CHECK: - // for bv in bound_vars: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(bv.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts(); size_t size = bound_vars.size(); @@ -4336,21 +4345,30 @@ Term Solver::defineFunRec(Term fun, for (size_t i = 0; i < size; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + bound_vars[i], + i) + << "a bound variable"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( domain_sorts[i] == bound_vars[i].getSort(), "sort of parameter", bound_vars[i], i) << "'" << domain_sorts[i] << "'"; } + CVC4_API_SOLVER_CHECK_TERM(term); Sort codomain = fun.getSort().getFunctionCodomainSort(); CVC4_API_CHECK(codomain == term.getSort()) << "Invalid sort of function body '" << term << "', expected '" << codomain << "'"; - // CHECK: - // for v in bound_vars: is bound var std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr); return fun; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4360,15 +4378,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, const std::vector<std::vector<Term>>& bound_vars, const std::vector<Term>& terms) const { - // CHECK: - // for f in funs: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(f.getExprManager()) - // for bv in bound_vars: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(bv.getExprManager()) - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; size_t funs_size = funs.size(); CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars) << "'" << funs_size << "'"; @@ -4378,13 +4388,30 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, const std::vector<Term>& bvars = bound_vars[j]; const Term& term = terms[j]; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == fun.d_solver, "function", fun, j) + << "function associated to this solver object"; CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; + CVC4_API_SOLVER_CHECK_TERM(term); + std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts(); size_t size = bvars.size(); CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars) << "'" << domain_sorts.size() << "'"; for (size_t i = 0; i < size; ++i) { + for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == bvars[k].d_solver, "bound variable", bvars[k], k) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + bvars[k], + k) + << "a bound variable"; + } CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( domain_sorts[i] == bvars[i].getSort(), "sort of parameter", @@ -4397,8 +4424,6 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, codomain == term.getSort(), "sort of function body", term, j) << "'" << codomain << "'"; } - // CHECK: - // for bv in bound_vars (for v in bv): is bound var std::vector<Expr> efuns = termVectorToExprs(funs); std::vector<std::vector<Expr>> ebound_vars; for (const auto& v : bound_vars) @@ -4407,6 +4432,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, } std::vector<Expr> exprs = termVectorToExprs(terms); d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4422,6 +4448,7 @@ void Solver::echo(std::ostream& out, const std::string& str) const */ std::vector<Term> Solver::getAssertions(void) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; std::vector<Expr> assertions = d_smtEngine->getAssertions(); /* Can not use * return std::vector<Term>(assertions.begin(), assertions.end()); @@ -4432,6 +4459,7 @@ std::vector<Term> Solver::getAssertions(void) const res.push_back(Term(this, e)); } return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4439,8 +4467,11 @@ std::vector<Term> Solver::getAssertions(void) const */ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const { - // CHECK: produce-models set - // CHECK: result sat + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::produceAssignments()) + << "Cannot get assignment unless assignment generation is enabled " + "(try --produce-assignments)"; std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment(); std::vector<std::pair<Term, Term>> res; for (const auto& p : assignment) @@ -4448,6 +4479,7 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const res.emplace_back(Term(this, p.first), Term(this, p.second)); } return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4455,8 +4487,12 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const */ std::string Solver::getInfo(const std::string& flag) const { - // CHECK: flag valid? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag)) + << "Unrecognized flag for getInfo."; + return d_smtEngine->getInfo(flag).toString(); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4464,9 +4500,10 @@ std::string Solver::getInfo(const std::string& flag) const */ std::string Solver::getOption(const std::string& option) const { - // CHECK: option exists? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; SExpr res = d_smtEngine->getOption(option); return res.toString(); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4474,9 +4511,18 @@ std::string Solver::getOption(const std::string& option) const */ std::vector<Term> Solver::getUnsatAssumptions(void) const { - // CHECK: incremental? - // CHECK: option produce-unsat-assumptions set? - // CHECK: last check sat/valid result is unsat/invalid + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::incrementalSolving()) + << "Cannot get unsat assumptions unless incremental solving is enabled " + "(try --incremental)"; + CVC4_API_CHECK(CVC4::options::unsatAssumptions()) + << "Cannot get unsat assumptions unless explicitly enabled " + "(try --produce-unsat-assumptions)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() + == SmtEngine::SmtMode::SMT_MODE_UNSAT) + << "Cannot get unsat assumptions unless in unsat mode."; + std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions(); /* Can not use * return std::vector<Term>(uassumptions.begin(), uassumptions.end()); @@ -4487,6 +4533,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const res.push_back(Term(this, e)); } return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4494,7 +4541,14 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const */ std::vector<Term> Solver::getUnsatCore(void) const { - // CHECK: result unsat? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::unsatCores()) + << "Cannot get unsat core unless explicitly enabled " + "(try --produce-unsat-cores)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() + == SmtEngine::SmtMode::SMT_MODE_UNSAT) + << "Cannot get unsat core unless in unsat mode."; UnsatCore core = d_smtEngine->getUnsatCore(); /* Can not use * return std::vector<Term>(core.begin(), core.end()); @@ -4505,6 +4559,7 @@ std::vector<Term> Solver::getUnsatCore(void) const res.push_back(Term(this, e)); } return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4512,10 +4567,10 @@ std::vector<Term> Solver::getUnsatCore(void) const */ Term Solver::getValue(Term term) const { - // CHECK: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(expr.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_SOLVER_CHECK_TERM(term); return Term(this, d_smtEngine->getValue(*term.d_expr)); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4523,17 +4578,25 @@ Term Solver::getValue(Term term) const */ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { - // CHECK: - // for e in exprs: - // NodeManager::fromExprManager(d_exprMgr) - // == NodeManager::fromExprManager(e.getExprManager()) + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::produceModels()) + << "Cannot get value unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() + != SmtEngine::SmtMode::SMT_MODE_UNSAT) + << "Cannot get value when in unsat mode."; std::vector<Term> res; - for (const Term& t : terms) + for (size_t i = 0, n = terms.size(); i < n; ++i) { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == terms[i].d_solver, "term", terms[i], i) + << "term associated to this solver object"; /* Can not use emplace_back here since constructor is private. */ - res.push_back(Term(this, d_smtEngine->getValue(*t.d_expr))); + res.push_back(Term(this, d_smtEngine->getValue(*terms[i].d_expr))); } return res; + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4558,8 +4621,16 @@ void Solver::pop(uint32_t nscopes) const void Solver::printModel(std::ostream& out) const { - // CHECK: produce-models? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::produceModels()) + << "Cannot get value unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() + != SmtEngine::SmtMode::SMT_MODE_UNSAT) + << "Cannot get value when in unsat mode."; out << *d_smtEngine->getModel(); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4583,22 +4654,11 @@ void Solver::push(uint32_t nscopes) const /** * ( reset-assertions ) */ -void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); } - -// TODO: issue #2781 -void Solver::setLogicHelper(const std::string& logic) const +void Solver::resetAssertions(void) const { - CVC4_API_CHECK(!d_smtEngine->isFullyInited()) - << "Invalid call to 'setLogic', solver is already fully initialized"; - try - { - CVC4::LogicInfo logic_info(logic); - d_smtEngine->setLogic(logic_info); - } - catch (CVC4::IllegalArgumentException& e) - { - throw CVC4ApiException(e.getMessage()); - } + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + d_smtEngine->resetAssertions(); + CVC4_API_SOLVER_TRY_CATCH_END; } /** @@ -4606,6 +4666,7 @@ void Solver::setLogicHelper(const std::string& logic) const */ void Solver::setInfo(const std::string& keyword, const std::string& value) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED( keyword == "source" || keyword == "category" || keyword == "difficulty" || keyword == "filename" || keyword == "license" || keyword == "name" @@ -4625,12 +4686,21 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const << "'sat', 'unsat' or 'unknown'"; d_smtEngine->setInfo(keyword, value); + CVC4_API_SOLVER_TRY_CATCH_END; } /** * ( set-logic <symbol> ) */ -void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); } +void Solver::setLogic(const std::string& logic) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(!d_smtEngine->isFullyInited()) + << "Invalid call to 'setLogic', solver is already fully initialized"; + CVC4::LogicInfo logic_info(logic); + d_smtEngine->setLogic(logic_info); + CVC4_API_SOLVER_TRY_CATCH_END; +} /** * ( set-option <option> ) @@ -4638,16 +4708,11 @@ void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); } void Solver::setOption(const std::string& option, const std::string& value) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_smtEngine->isFullyInited()) << "Invalid call to 'setOption', solver is already fully initialized"; - try - { - d_smtEngine->setOption(option, value); - } - catch (CVC4::OptionException& e) - { - throw CVC4ApiException(e.getMessage()); - } + d_smtEngine->setOption(option, value); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::ensureTermSort(const Term& term, const Sort& sort) const @@ -4684,6 +4749,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(sort); + CVC4_API_SOLVER_CHECK_SORT(sort); Expr res = d_exprMgr->mkBoundVar(symbol, *sort.d_type); (void)res.getType(true); /* kick off type checking */ @@ -4698,12 +4764,22 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars, const std::vector<Term>& ntSymbols) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols) << "non-empty vector"; for (size_t i = 0, n = boundVars.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == boundVars[i].d_solver, "bound variable", boundVars[i], i) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + boundVars[i], + i) + << "a bound variable"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !boundVars[i].isNull(), "parameter term", boundVars[i], i) << "non-null term"; } @@ -4711,11 +4787,21 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars, for (size_t i = 0, n = ntSymbols.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == ntSymbols[i].d_solver, "term", ntSymbols[i], i) + << "term associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + ntSymbols[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + ntSymbols[i], + i) + << "a bound variable"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i) << "non-null term"; } return Grammar(this, boundVars, ntSymbols); + CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::synthFun(const std::string& symbol, @@ -4764,10 +4850,20 @@ Term Solver::synthFunHelper(const std::string& symbol, for (size_t i = 0, n = boundVars.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == boundVars[i].d_solver, "bound variable", boundVars[i], i) + << "bound variable associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE, + "bound variable", + boundVars[i], + i) + << "a bound variable"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !boundVars[i].isNull(), "parameter term", boundVars[i], i) << "non-null term"; varTypes.push_back(boundVars[i].d_expr->getType()); } + CVC4_API_SOLVER_CHECK_SORT(sort); if (g != nullptr) { @@ -4796,12 +4892,15 @@ Term Solver::synthFunHelper(const std::string& symbol, void Solver::addSygusConstraint(Term term) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_SOLVER_CHECK_TERM(term); CVC4_API_ARG_CHECK_EXPECTED( term.d_expr->getType() == d_exprMgr->booleanType(), term) << "boolean term"; d_smtEngine->assertSygusConstraint(*term.d_expr); + CVC4_API_SOLVER_TRY_CATCH_END; } void Solver::addSygusInvConstraint(Term inv, @@ -4809,10 +4908,15 @@ void Solver::addSygusInvConstraint(Term inv, Term trans, Term post) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(inv); + CVC4_API_SOLVER_CHECK_TERM(inv); CVC4_API_ARG_CHECK_NOT_NULL(pre); + CVC4_API_SOLVER_CHECK_TERM(pre); CVC4_API_ARG_CHECK_NOT_NULL(trans); + CVC4_API_SOLVER_CHECK_TERM(trans); CVC4_API_ARG_CHECK_NOT_NULL(post); + CVC4_API_SOLVER_CHECK_TERM(post); CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv) << "a function"; @@ -4847,13 +4951,21 @@ void Solver::addSygusInvConstraint(Term inv, d_smtEngine->assertSygusInvConstraint( *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr); + CVC4_API_SOLVER_TRY_CATCH_END; } -Result Solver::checkSynth() const { return d_smtEngine->checkSynth(); } +Result Solver::checkSynth() const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + return d_smtEngine->checkSynth(); + CVC4_API_SOLVER_TRY_CATCH_END; +} Term Solver::getSynthSolution(Term term) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_NOT_NULL(term); + CVC4_API_SOLVER_CHECK_TERM(term); std::map<CVC4::Expr, CVC4::Expr> map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) @@ -4865,16 +4977,21 @@ Term Solver::getSynthSolution(Term term) const CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term"; return Term(this, it->second); + CVC4_API_SOLVER_TRY_CATCH_END; } std::vector<Term> Solver::getSynthSolutions( const std::vector<Term>& terms) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector"; for (size_t i = 0, n = terms.size(); i < n; ++i) { CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == terms[i].d_solver, "parameter term", terms[i], i) + << "parameter term associated to this solver object"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( !terms[i].isNull(), "parameter term", terms[i], i) << "non-null term"; } @@ -4899,11 +5016,14 @@ std::vector<Term> Solver::getSynthSolutions( } return synthSolution; + CVC4_API_SOLVER_TRY_CATCH_END; } void Solver::printSynthSolution(std::ostream& out) const { + CVC4_API_SOLVER_TRY_CATCH_BEGIN; d_smtEngine->printSynthSolution(out); + CVC4_API_SOLVER_TRY_CATCH_END; } /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3c0a2cd8f..9e382cdcf 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1022,72 +1022,110 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) throw UnrecognizedOptionException(); } -CVC4::SExpr SmtEngine::getInfo(const std::string& key) const { +bool SmtEngine::isValidGetInfoFlag(const std::string& key) const +{ + if (key == "all-statistics" || key == "error-behavior" || key == "name" + || key == "version" || key == "authors" || key == "status" + || key == "reason-unknown" || key == "assertion-stack-levels" + || key == "all-options") + { + return true; + } + return false; +} +CVC4::SExpr SmtEngine::getInfo(const std::string& key) const +{ SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; - if(key == "all-statistics") { + if (!isValidGetInfoFlag(key)) + { + throw UnrecognizedOptionException(); + } + if (key == "all-statistics") + { vector<SExpr> stats; - for(StatisticsRegistry::const_iterator i = NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->begin(); - i != NodeManager::fromExprManager(d_exprManager)->getStatisticsRegistry()->end(); - ++i) { + for (StatisticsRegistry::const_iterator i = + NodeManager::fromExprManager(d_exprManager) + ->getStatisticsRegistry() + ->begin(); + i + != NodeManager::fromExprManager(d_exprManager) + ->getStatisticsRegistry() + ->end(); + ++i) + { vector<SExpr> v; v.push_back((*i).first); v.push_back((*i).second); stats.push_back(v); } - for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin(); - i != d_statisticsRegistry->end(); - ++i) { + for (StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin(); + i != d_statisticsRegistry->end(); + ++i) + { vector<SExpr> v; v.push_back((*i).first); v.push_back((*i).second); stats.push_back(v); } return SExpr(stats); - } else if(key == "error-behavior") { + } + if (key == "error-behavior") + { return SExpr(SExpr::Keyword("immediate-exit")); - } else if(key == "name") { + } + if (key == "name") + { return SExpr(Configuration::getName()); - } else if(key == "version") { + } + if (key == "version") + { return SExpr(Configuration::getVersionString()); - } else if(key == "authors") { + } + if (key == "authors") + { return SExpr(Configuration::about()); - } else if(key == "status") { + } + if (key == "status") + { // sat | unsat | unknown - switch(d_status.asSatisfiabilityResult().isSat()) { - case Result::SAT: - return SExpr(SExpr::Keyword("sat")); - case Result::UNSAT: - return SExpr(SExpr::Keyword("unsat")); - default: - return SExpr(SExpr::Keyword("unknown")); - } - } else if(key == "reason-unknown") { - if(!d_status.isNull() && d_status.isUnknown()) { + switch (d_status.asSatisfiabilityResult().isSat()) + { + case Result::SAT: return SExpr(SExpr::Keyword("sat")); + case Result::UNSAT: return SExpr(SExpr::Keyword("unsat")); + default: return SExpr(SExpr::Keyword("unknown")); + } + } + if (key == "reason-unknown") + { + if (!d_status.isNull() && d_status.isUnknown()) + { stringstream ss; ss << d_status.whyUnknown(); string s = ss.str(); transform(s.begin(), s.end(), s.begin(), ::tolower); return SExpr(SExpr::Keyword(s)); - } else { + } + else + { throw RecoverableModalException( "Can't get-info :reason-unknown when the " "last result wasn't unknown!"); } - } else if(key == "assertion-stack-levels") { + } + if (key == "assertion-stack-levels") + { AlwaysAssert(d_userLevels.size() <= std::numeric_limits<unsigned long int>::max()); return SExpr(static_cast<unsigned long int>(d_userLevels.size())); - } else if(key == "all-options") { - // get the options, like all-statistics - std::vector< std::vector<std::string> > current_options = - Options::current()->getOptions(); - return SExpr::parseListOfListOfAtoms(current_options); - } else { - throw UnrecognizedOptionException(); } + Assert(key == "all-options"); + // get the options, like all-statistics + std::vector<std::vector<std::string>> current_options = + Options::current()->getOptions(); + return SExpr::parseListOfListOfAtoms(current_options); } void SmtEngine::debugCheckFormals(const std::vector<Expr>& formals, Expr func) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 672bec821..75737b603 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -141,6 +141,27 @@ class CVC4_PUBLIC SmtEngine public: /* ....................................................................... */ + /** + * The current mode of the solver, which is an extension of Figure 4.1 on + * page 52 of the SMT-LIB version 2.6 standard + * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf + */ + enum SmtMode + { + // the initial state of the solver + SMT_MODE_START, + // normal state of the solver, after assert/push/pop/declare/define + SMT_MODE_ASSERT, + // immediately after a check-sat returning "sat" + SMT_MODE_SAT, + // immediately after a check-sat returning "unknown" + SMT_MODE_SAT_UNKNOWN, + // immediately after a check-sat returning "unsat" + SMT_MODE_UNSAT, + // immediately after a successful call to get-abduct + SMT_MODE_ABDUCT + }; + /** Construct an SmtEngine with the given expression manager. */ SmtEngine(ExprManager* em); /** Destruct the SMT engine. */ @@ -162,6 +183,9 @@ class CVC4_PUBLIC SmtEngine /** Return the user context level. */ size_t getNumUserLevels() { return d_userLevels.size(); } + /** Return the current mode of the solver. */ + SmtMode getSmtMode() { return d_smtMode; } + /** * Set the logic of the script. * @throw ModalException, LogicException @@ -189,6 +213,9 @@ class CVC4_PUBLIC SmtEngine */ void setInfo(const std::string& key, const CVC4::SExpr& value); + /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */ + bool isValidGetInfoFlag(const std::string& key) const; + /** Query information about the SMT environment. */ CVC4::SExpr getInfo(const std::string& key) const; @@ -838,27 +865,6 @@ class CVC4_PUBLIC SmtEngine /** The types for the recursive function definitions */ typedef context::CDList<Node> NodeList; - /** - * The current mode of the solver, which is an extension of Figure 4.1 on - * page 52 of the SMT-LIB version 2.6 standard - * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf - */ - enum SmtMode - { - // the initial state of the solver - SMT_MODE_START, - // normal state of the solver, after assert/push/pop/declare/define - SMT_MODE_ASSERT, - // immediately after a check-sat returning "sat" - SMT_MODE_SAT, - // immediately after a check-sat returning "unknown" - SMT_MODE_SAT_UNKNOWN, - // immediately after a check-sat returning "unsat" - SMT_MODE_UNSAT, - // immediately after a successful call to get-abduct - SMT_MODE_ABDUCT - }; - // disallow copy/assignment SmtEngine(const SmtEngine&) = delete; SmtEngine& operator=(const SmtEngine&) = delete; diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 7e925df54..43554088f 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -88,13 +88,28 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFunsRec(); void testUFIteration(); + + void testGetInfo(); void testGetOp(); + void testGetOption(); + void testGetUnsatAssumptions1(); + void testGetUnsatAssumptions2(); + void testGetUnsatAssumptions3(); + void testGetUnsatCore1(); + void testGetUnsatCore2(); + void testGetUnsatCore3(); + void testGetValue1(); + void testGetValue2(); + void testGetValue3(); void testPush1(); void testPush2(); void testPop1(); void testPop2(); void testPop3(); + void testPrintModel1(); + void testPrintModel2(); + void testPrintModel3(); void testSimplify(); @@ -990,17 +1005,36 @@ void SolverBlack::testDefineFun() TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1)); TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver->defineFun("ff", {v1, b2}, bvSort, v1), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun("fff", {b1}, bvSort, v3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun("ffff", {b1}, funSort2, v3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun("fffff", {b1, b3}, bvSort, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFun(f1, {v1, b11}, v1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1}, v1), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun(f1, {b1, b11}, v3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun(f2, {b1}, v2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFun(f3, {b1}, v1), CVC4ApiException&); + + Solver slv; + Sort bvSort2 = slv.mkBitVectorSort(32); + Term v12 = slv.mkConst(bvSort2, "v1"); + Term b12 = slv.mkVar(bvSort2, "b1"); + Term b22 = slv.mkVar(slv.getIntegerSort(), "b2"); + TS_ASSERT_THROWS(slv.defineFun("f", {}, bvSort, v12), CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFun("f", {}, bvSort2, v1), CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFun("ff", {b1, b22}, bvSort2, v12), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b2}, bvSort2, v12), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b22}, bvSort, v12), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFun("ff", {b12, b22}, bvSort2, v1), + CVC4ApiException&); } void SolverBlack::testDefineFunRec() @@ -1024,6 +1058,8 @@ void SolverBlack::testDefineFunRec() TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1)); TS_ASSERT_THROWS(d_solver->defineFunRec("fff", {b1}, bvSort, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec("ff", {b1, v2}, bvSort, v1), + CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFunRec("ffff", {b1}, funSort2, v3), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1), @@ -1035,6 +1071,24 @@ void SolverBlack::testDefineFunRec() CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFunRec(f2, {b1}, v2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFunRec(f3, {b1}, v1), CVC4ApiException&); + + Solver slv; + Sort bvSort2 = slv.mkBitVectorSort(32); + Term v12 = slv.mkConst(bvSort2, "v1"); + Term b12 = slv.mkVar(bvSort2, "b1"); + Term b22 = slv.mkVar(slv.getIntegerSort(), "b2"); + TS_ASSERT_THROWS_NOTHING(slv.defineFunRec("f", {}, bvSort2, v12)); + TS_ASSERT_THROWS_NOTHING(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12)); + TS_ASSERT_THROWS(slv.defineFunRec("f", {}, bvSort, v12), CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFunRec("f", {}, bvSort2, v1), CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b22}, bvSort, v12), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1), + CVC4ApiException&); } void SolverBlack::testDefineFunsRec() @@ -1058,6 +1112,9 @@ void SolverBlack::testDefineFunsRec() TS_ASSERT_THROWS_NOTHING( d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); TS_ASSERT_THROWS( + d_solver->defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS( d_solver->defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), @@ -1068,6 +1125,42 @@ void SolverBlack::testDefineFunsRec() TS_ASSERT_THROWS( d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), CVC4ApiException&); + + Solver slv; + Sort uSort2 = slv.mkUninterpretedSort("u"); + Sort bvSort2 = slv.mkBitVectorSort(32); + Sort funSort12 = slv.mkFunctionSort({bvSort2, bvSort2}, bvSort2); + Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort()); + Term b12 = slv.mkVar(bvSort2, "b1"); + Term b112 = slv.mkVar(bvSort2, "b1"); + Term b42 = slv.mkVar(uSort2, "b4"); + Term v12 = slv.mkConst(bvSort2, "v1"); + Term v22 = slv.mkConst(slv.getIntegerSort(), "v2"); + Term f12 = slv.mkConst(funSort12, "f1"); + Term f22 = slv.mkConst(funSort22, "f2"); + TS_ASSERT_THROWS_NOTHING( + slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22})); + TS_ASSERT_THROWS( + slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}), + CVC4ApiException&); + TS_ASSERT_THROWS( + slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}), + CVC4ApiException&); } void SolverBlack::testUFIteration() @@ -1090,6 +1183,12 @@ void SolverBlack::testUFIteration() } } +void SolverBlack::testGetInfo() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->getInfo("name")); + TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&); +} + void SolverBlack::testGetOp() { Sort bv32 = d_solver->mkBitVectorSort(32); @@ -1132,6 +1231,164 @@ void SolverBlack::testGetOp() TS_ASSERT_EQUALS(listhead.getOp(), Op(d_solver.get(), APPLY_SELECTOR)); } +void SolverBlack::testGetOption() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->getOption("incremental")); + TS_ASSERT_THROWS(d_solver->getOption("asdf"), CVC4ApiException&); +} + +void SolverBlack::testGetUnsatAssumptions1() +{ +#if IS_PROOFS_BUILD + d_solver->setOption("incremental", "false"); + d_solver->checkSatAssuming(d_solver->mkFalse()); + TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&); +#endif +} + +void SolverBlack::testGetUnsatAssumptions2() +{ +#if IS_PROOFS_BUILD + d_solver->setOption("incremental", "true"); + d_solver->setOption("produce-unsat-assumptions", "false"); + d_solver->checkSatAssuming(d_solver->mkFalse()); + TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&); +#endif +} + +void SolverBlack::testGetUnsatAssumptions3() +{ +#if IS_PROOFS_BUILD + d_solver->setOption("incremental", "true"); + d_solver->setOption("produce-unsat-assumptions", "true"); + d_solver->checkSatAssuming(d_solver->mkFalse()); + TS_ASSERT_THROWS_NOTHING(d_solver->getUnsatAssumptions()); + d_solver->checkSatAssuming(d_solver->mkTrue()); + TS_ASSERT_THROWS(d_solver->getUnsatAssumptions(), CVC4ApiException&); +#endif +} + +void SolverBlack::testGetUnsatCore1() +{ +#if IS_PROOFS_BUILD + d_solver->setOption("incremental", "false"); + d_solver->assertFormula(d_solver->mkFalse()); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getUnsatCore(), CVC4ApiException&); +#endif +} + +void SolverBlack::testGetUnsatCore2() +{ +#if IS_PROOFS_BUILD + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-unsat-cores", "false"); + d_solver->assertFormula(d_solver->mkFalse()); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getUnsatCore(), CVC4ApiException&); +#endif +} + +void SolverBlack::testGetUnsatCore3() +{ +#if IS_PROOFS_BUILD + d_solver->setOption("incremental", "true"); + d_solver->setOption("produce-unsat-cores", "true"); + + Sort uSort = d_solver->mkUninterpretedSort("u"); + Sort intSort = d_solver->getIntegerSort(); + Sort boolSort = d_solver->getBooleanSort(); + Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort); + Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort); + std::vector<Term> unsat_core; + + Term x = d_solver->mkConst(uSort, "x"); + Term y = d_solver->mkConst(uSort, "y"); + Term f = d_solver->mkConst(uToIntSort, "f"); + Term p = d_solver->mkConst(intPredSort, "p"); + Term zero = d_solver->mkReal(0); + Term one = d_solver->mkReal(1); + Term f_x = d_solver->mkTerm(APPLY_UF, f, x); + Term f_y = d_solver->mkTerm(APPLY_UF, f, y); + Term sum = d_solver->mkTerm(PLUS, f_x, f_y); + Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero); + Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y); + d_solver->assertFormula(d_solver->mkTerm(GT, zero, f_x)); + d_solver->assertFormula(d_solver->mkTerm(GT, zero, f_y)); + d_solver->assertFormula(d_solver->mkTerm(GT, sum, one)); + d_solver->assertFormula(p_0); + d_solver->assertFormula(p_f_y.notTerm()); + TS_ASSERT(d_solver->checkSat().isUnsat()); + + TS_ASSERT_THROWS_NOTHING(unsat_core = d_solver->getUnsatCore()); + + d_solver->resetAssertions(); + for (const auto& t : unsat_core) + { + d_solver->assertFormula(t); + } + Result res = d_solver->checkSat(); + TS_ASSERT(res.isUnsat()); +#endif +} + +void SolverBlack::testGetValue1() +{ + d_solver->setOption("produce-models", "false"); + Term t = d_solver->mkTrue(); + d_solver->assertFormula(t); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getValue(t), CVC4ApiException&); +} + +void SolverBlack::testGetValue2() +{ + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkFalse(); + d_solver->assertFormula(t); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getValue(t), CVC4ApiException&); +} + +void SolverBlack::testGetValue3() +{ + d_solver->setOption("produce-models", "true"); + Sort uSort = d_solver->mkUninterpretedSort("u"); + Sort intSort = d_solver->getIntegerSort(); + Sort boolSort = d_solver->getBooleanSort(); + Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort); + Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort); + std::vector<Term> unsat_core; + + Term x = d_solver->mkConst(uSort, "x"); + Term y = d_solver->mkConst(uSort, "y"); + Term z = d_solver->mkConst(uSort, "z"); + Term f = d_solver->mkConst(uToIntSort, "f"); + Term p = d_solver->mkConst(intPredSort, "p"); + Term zero = d_solver->mkReal(0); + Term one = d_solver->mkReal(1); + Term f_x = d_solver->mkTerm(APPLY_UF, f, x); + Term f_y = d_solver->mkTerm(APPLY_UF, f, y); + Term sum = d_solver->mkTerm(PLUS, f_x, f_y); + Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero); + Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y); + + d_solver->assertFormula(d_solver->mkTerm(LEQ, zero, f_x)); + d_solver->assertFormula(d_solver->mkTerm(LEQ, zero, f_y)); + d_solver->assertFormula(d_solver->mkTerm(LEQ, sum, one)); + d_solver->assertFormula(p_0.notTerm()); + d_solver->assertFormula(p_f_y); + TS_ASSERT(d_solver->checkSat().isSat()); + TS_ASSERT_THROWS_NOTHING(d_solver->getValue(x)); + TS_ASSERT_THROWS_NOTHING(d_solver->getValue(y)); + TS_ASSERT_THROWS_NOTHING(d_solver->getValue(z)); + TS_ASSERT_THROWS_NOTHING(d_solver->getValue(sum)); + TS_ASSERT_THROWS_NOTHING(d_solver->getValue(p_f_y)); + + Solver slv; + TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&); +} + void SolverBlack::testPush1() { d_solver->setOption("incremental", "true"); @@ -1168,6 +1425,32 @@ 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::testSetInfo() { TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&); @@ -1483,20 +1766,30 @@ void SolverBlack::testMkSygusVar() TS_ASSERT_THROWS(d_solver->mkSygusVar(Sort()), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkSygusVar(d_solver->getNullSort(), "a"), CVC4ApiException&); + Solver slv; + TS_ASSERT_THROWS(slv.mkSygusVar(boolSort), CVC4ApiException&); } void SolverBlack::testMkSygusGrammar() { Term nullTerm; Term boolTerm = d_solver->mkBoolean(true); - Term intTerm = d_solver->mkReal(1); + Term boolVar = d_solver->mkVar(d_solver->getBooleanSort()); + Term intVar = d_solver->mkVar(d_solver->getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({}, {intTerm})); - TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({boolTerm}, {intTerm})); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({}, {intVar})); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSygusGrammar({boolVar}, {intVar})); TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {}), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {nullTerm}), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkSygusGrammar({nullTerm}, {intTerm}), + TS_ASSERT_THROWS(d_solver->mkSygusGrammar({}, {boolTerm}), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkSygusGrammar({boolTerm}, {intVar}), CVC4ApiException&); + Solver slv; + Term boolVar2 = slv.mkVar(slv.getBooleanSort()); + Term intVar2 = slv.mkVar(slv.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(slv.mkSygusGrammar({boolVar2}, {intVar2})); + TS_ASSERT_THROWS(slv.mkSygusGrammar({boolVar}, {intVar2}), CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkSygusGrammar({boolVar2}, {intVar}), CVC4ApiException&); } void SolverBlack::testSynthFun() @@ -1528,6 +1821,13 @@ void SolverBlack::testSynthFun() TS_ASSERT_THROWS(d_solver->synthFun("f5", {}, boolToBool), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->synthFun("f6", {x}, boolean, g2), CVC4ApiException&); + Solver slv; + Term x2 = slv.mkVar(slv.getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(slv.synthFun("f1", {x2}, slv.getBooleanSort())); + TS_ASSERT_THROWS(slv.synthFun("", {}, d_solver->getBooleanSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.synthFun("f1", {x}, d_solver->getBooleanSort()), + CVC4ApiException&); } void SolverBlack::testSynthInv() @@ -1564,6 +1864,9 @@ void SolverBlack::testAddSygusConstraint() TS_ASSERT_THROWS_NOTHING(d_solver->addSygusConstraint(boolTerm)); TS_ASSERT_THROWS(d_solver->addSygusConstraint(nullTerm), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->addSygusConstraint(intTerm), CVC4ApiException&); + + Solver slv; + TS_ASSERT_THROWS(slv.addSygusConstraint(boolTerm), CVC4ApiException&); } void SolverBlack::testAddSygusInvConstraint() @@ -1619,6 +1922,23 @@ void SolverBlack::testAddSygusInvConstraint() TS_ASSERT_THROWS(d_solver->addSygusInvConstraint(inv, pre, trans, trans), CVC4ApiException&); + Solver slv; + Sort boolean2 = slv.getBooleanSort(); + Sort real2 = slv.getRealSort(); + Term inv22 = slv.declareFun("inv", {real2}, boolean2); + Term pre22 = slv.declareFun("pre", {real2}, boolean2); + Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2); + Term post22 = slv.declareFun("post", {real2}, boolean2); + TS_ASSERT_THROWS_NOTHING( + slv.addSygusInvConstraint(inv22, pre22, trans22, post22)); + TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv, pre22, trans22, post22), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre, trans22, post22), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre22, trans, post22), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.addSygusInvConstraint(inv22, pre22, trans22, post), + CVC4ApiException&); } void SolverBlack::testGetSynthSolution() @@ -1639,6 +1959,9 @@ void SolverBlack::testGetSynthSolution() TS_ASSERT_THROWS(d_solver->getSynthSolution(nullTerm), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->getSynthSolution(x), CVC4ApiException&); + + Solver slv; + TS_ASSERT_THROWS(slv.getSynthSolution(f), CVC4ApiException&); } void SolverBlack::testGetSynthSolutions() @@ -1661,4 +1984,7 @@ void SolverBlack::testGetSynthSolutions() TS_ASSERT_THROWS(d_solver->getSynthSolutions({}), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->getSynthSolutions({nullTerm}), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->getSynthSolutions({x}), CVC4ApiException&); + + Solver slv; + TS_ASSERT_THROWS(slv.getSynthSolutions({x}), CVC4ApiException&); } |