This adds the remaining API guards in the Solver object (incl. unit tests).
*/
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;
}
/**
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
<< "'";
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();
<< "'" << domain_sorts.size() << "'";
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",
<< "'" << 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;
}
/**
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())
{
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();
<< "'" << domain_sorts.size() << "'";
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",
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;
}
/**
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 << "'";
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",
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)
}
std::vector<Expr> exprs = termVectorToExprs(terms);
d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs);
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
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());
res.push_back(Term(this, e));
}
return res;
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
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)
res.emplace_back(Term(this, p.first), Term(this, p.second));
}
return res;
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
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;
}
/**
*/
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;
}
/**
*/
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());
res.push_back(Term(this, e));
}
return res;
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
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());
res.push_back(Term(this, e));
}
return res;
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
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;
}
/**
*/
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;
}
/**
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;
}
/**
/**
* ( 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;
}
/**
*/
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"
<< "'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> )
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
{
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 */
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";
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,
std::vector<Type> varTypes;
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)
{
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,
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";
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))
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";
}
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;
}
/**
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)
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. */
/** 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
*/
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;
/** 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;
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();
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()
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),
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()
Term f3 = d_solver->mkConst(bvSort, "f3");
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, 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()
}
}
+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);
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");
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&);
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()
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()
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()
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()
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()
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&);
}
projects / cvc5.git / commitdiff