DatatypeDecl paramConsListSpec =
slv.mkDatatypeDecl("paramlist",
sort); // give the datatype a name
- DatatypeConstructorDecl paramCons("cons");
- DatatypeConstructorDecl paramNil("nil");
+ DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
paramCons.addSelector("head", sort);
paramCons.addSelectorSelf("tail");
paramConsListSpec.addConstructor(paramCons);
DatatypeDecl consListSpec =
slv.mkDatatypeDecl("list"); // give the datatype a name
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", slv.getIntegerSort());
cons.addSelectorSelf("tail");
consListSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil");
consListSpec.addConstructor(nil);
std::cout << "spec is:" << std::endl << consListSpec << std::endl;
<< ">>> Alternatively, use declareDatatype" << std::endl;
std::cout << std::endl;
- DatatypeConstructorDecl cons2("cons");
+ DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons");
cons2.addSelector("head", slv.getIntegerSort());
cons2.addSelectorSelf("tail");
- DatatypeConstructorDecl nil2("nil");
+ DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil");
std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
Sort consListSort2 = slv.declareDatatype("list2", ctors);
test(slv, consListSort2);
# constructor "cons".
sort = slv.mkParamSort("T")
paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort)
- paramCons = pycvc4.DatatypeConstructorDecl("cons")
- paramNil = pycvc4.DatatypeConstructorDecl("nil")
+ paramCons = slv.mkDatatypeConstructorDecl("cons")
+ paramNil = slv.mkDatatypeConstructorDecl("nil")
paramCons.addSelector("head", sort)
paramCons.addSelectorSelf("tail")
paramConsListSpec.addConstructor(paramCons)
# symbols are assigned to its constructors, selectors, and testers.
consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name
- cons = pycvc4.DatatypeConstructorDecl("cons")
+ cons = slv.mkDatatypeConstructorDecl("cons")
cons.addSelector("head", slv.getIntegerSort())
cons.addSelectorSelf("tail")
consListSpec.addConstructor(cons)
- nil = pycvc4.DatatypeConstructorDecl("nil")
+ nil = slv.mkDatatypeConstructorDecl("nil")
consListSpec.addConstructor(nil)
print("spec is {}".format(consListSpec))
print("### Alternatively, use declareDatatype")
- cons2 = pycvc4.DatatypeConstructorDecl("cons")
+ cons2 = slv.mkDatatypeConstructorDecl("cons")
cons2.addSelector("head", slv.getIntegerSort())
cons2.addSelectorSelf("tail")
- nil2 = pycvc4.DatatypeConstructorDecl("nil")
+ nil2 = slv.mkDatatypeConstructorDecl("nil")
ctors = [cons2, nil2]
consListSort2 = slv.declareDatatype("list2", ctors)
test(slv, consListSort2)
CVC4_API_CHECK(isDefinedKind(kind)) \
<< "Invalid kind '" << kindToString(kind) << "'";
-#define CVC4_API_SORT_CHECK_SOLVER(sort)
-
#define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
CVC4_PREDICT_TRUE(cond) \
? (void)0 \
& CVC4ApiExceptionStream().ostream() \
<< "Invalid size of argument '" << #arg << "', expected "
-#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \
- CVC4_PREDICT_TRUE(cond) \
- ? (void)0 \
- : OstreamVoider() \
- & CVC4ApiExceptionStream().ostream() \
- << "Invalid " << what << " '" << arg << "' at index" << idx \
+#define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \
+ CVC4_PREDICT_TRUE(cond) \
+ ? (void)0 \
+ : OstreamVoider() \
+ & CVC4ApiExceptionStream().ostream() \
+ << "Invalid " << what << " '" << arg << "' at index " << idx \
<< ", expected "
#define CVC4_API_SOLVER_TRY_CATCH_BEGIN \
} \
catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \
catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); }
+
+#define CVC4_API_SOLVER_CHECK_SORT(sort) \
+ CVC4_API_CHECK(this == sort.d_solver) \
+ << "Given sort is not associated with this solver";
+
+#define CVC4_API_SOLVER_CHECK_TERM(term) \
+ CVC4_API_CHECK(this == term.d_solver) \
+ << "Given term is not associated with this solver";
+
+#define CVC4_API_SOLVER_CHECK_OP(op) \
+ CVC4_API_CHECK(this == op.d_solver) \
+ << "Given operator is not associated with this solver";
+
} // namespace
/* -------------------------------------------------------------------------- */
{
if (it.d_orig_expr != nullptr)
{
+ d_solver = it.d_solver;
d_orig_expr = it.d_orig_expr;
d_pos = it.d_pos;
}
Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
{
+ d_solver = it.d_solver;
d_orig_expr = it.d_orig_expr;
d_pos = it.d_pos;
return *this;
{
return false;
}
- return (*d_orig_expr == *it.d_orig_expr) && (d_pos == it.d_pos);
+ return (d_solver == it.d_solver && *d_orig_expr == *it.d_orig_expr)
+ && (d_pos == it.d_pos);
}
bool Term::const_iterator::operator!=(const const_iterator& it) const
/* DatatypeConstructorDecl -------------------------------------------------- */
-DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name)
- : d_ctor(new CVC4::DatatypeConstructor(name))
+DatatypeConstructorDecl::DatatypeConstructorDecl()
+ : d_solver(nullptr), d_ctor(nullptr)
+{
+}
+
+DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv,
+ const std::string& name)
+ : d_solver(slv), d_ctor(new CVC4::DatatypeConstructor(name))
{
}
/* DatatypeDecl ------------------------------------------------------------- */
+DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
+
DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
bool isCoDatatype)
- : d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
+ : d_solver(slv),
+ d_dtype(new CVC4::Datatype(slv->getExprManager(), name, isCoDatatype))
{
}
const std::string& name,
Sort param,
bool isCoDatatype)
- : d_dtype(new CVC4::Datatype(slv->getExprManager(),
+ : d_solver(slv),
+ d_dtype(new CVC4::Datatype(slv->getExprManager(),
name,
std::vector<Type>{*param.d_type},
isCoDatatype))
const std::string& name,
const std::vector<Sort>& params,
bool isCoDatatype)
+ : d_solver(slv)
{
std::vector<Type> tparams;
for (const Sort& p : params)
bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
-DatatypeDecl::DatatypeDecl() {}
-
DatatypeDecl::~DatatypeDecl() {}
void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
for (size_t i = 0, size = children.size(); i < size; ++i)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- !children[i].isNull(), "parameter term", children[i], i)
+ !children[i].isNull(), "child term", children[i], i)
<< "non-null term";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == children[i].d_solver, "child term", children[i], i)
+ << "a child term associated to this solver object";
}
std::vector<Expr> echildren = termVectorToExprs(children);
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
std::vector<CVC4::Datatype> datatypes;
- for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; i++)
- {
- CVC4_API_ARG_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
- dtypedecls[i])
+ for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
+ {
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver,
+ "datatype declaration",
+ dtypedecls[i],
+ i)
+ << "a datatype declaration associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
+ "datatype declaration",
+ dtypedecls[i],
+ i)
<< "a datatype declaration with at least one constructor";
datatypes.push_back(dtypedecls[i].getDatatype());
}
+ for (auto& sort : unresolvedSorts)
+ {
+ CVC4_API_SOLVER_CHECK_SORT(sort);
+ }
std::set<Type> utypes = sortSetToTypes(unresolvedSorts);
std::vector<CVC4::DatatypeType> dtypes =
d_exprMgr->mkMutualDatatypeTypes(datatypes, utypes);
std::vector<Type> res;
for (const Sort& s : sorts)
{
+ CVC4_API_SOLVER_CHECK_SORT(s);
res.push_back(*s.d_type);
}
return res;
std::vector<Expr> res;
for (const Term& t : terms)
{
+ CVC4_API_SOLVER_CHECK_TERM(t);
res.push_back(*t.d_expr);
}
return res;
<< "non-null index sort";
CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
<< "non-null element sort";
+ CVC4_API_SOLVER_CHECK_SORT(indexSort);
+ CVC4_API_SOLVER_CHECK_SORT(elemSort);
return Sort(this,
d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_CHECK(this == dtypedecl.d_solver)
+ << "Given datatype declaration is not associated with this solver";
CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
<< "a datatype declaration with at least one constructor";
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
<< "non-null codomain sort";
+ CVC4_API_SOLVER_CHECK_SORT(domain);
+ CVC4_API_SOLVER_CHECK_SORT(codomain);
CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain)
<< "first-class sort as domain sort for function sort";
CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
!sorts[i].isNull(), "parameter sort", sorts[i], i)
<< "non-null sort";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+ << "sort associated to this solver object";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
<< "first-class sort as parameter sort for function sort";
}
CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
<< "non-null codomain sort";
+ CVC4_API_SOLVER_CHECK_SORT(codomain);
CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
<< "first-class sort as codomain sort for function sort";
Assert(!codomain.isFunction()); /* A function sort is not first-class. */
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
!sorts[i].isNull(), "parameter sort", sorts[i], i)
<< "non-null sort";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+ << "sort associated to this solver object";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
<< "first-class sort as parameter sort for predicate sort";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
!p.second.isNull(), "parameter sort", p.second, i)
<< "non-null sort";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == p.second.d_solver, "parameter sort", p.second, i)
+ << "sort associated to this solver object";
i += 1;
f.emplace_back(p.first, *p.second.d_type);
}
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
<< "non-null element sort";
+ CVC4_API_SOLVER_CHECK_SORT(elemSort);
return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
!sorts[i].isNull(), "parameter sort", sorts[i], i)
<< "non-null sort";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+ << "sort associated to this solver object";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
!sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
<< "non-function-like sort as parameter sort for tuple sort";
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
<< "null sort or set sort";
+ CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
+ << "set sort associated to this solver object";
return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
{
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->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
(void)res.getType(true); /* kick off type checking */
{
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->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
Term Solver::mkConstArray(Sort sort, Term val) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_ARG_CHECK_NOT_NULL(sort);
CVC4_API_ARG_CHECK_NOT_NULL(val);
+ CVC4_API_SOLVER_CHECK_SORT(sort);
+ CVC4_API_SOLVER_CHECK_TERM(val);
CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
<< "Value does not match element sort.";
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
+ CVC4_API_SOLVER_CHECK_SORT(sort);
return mkValHelper<CVC4::UninterpretedConstant>(
CVC4::UninterpretedConstant(*sort.d_type, index));
CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
<< "a bit-vector constant with bit-width '" << bw << "'";
CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(val);
CVC4_API_ARG_CHECK_EXPECTED(
val.getSort().isBitVector() && val.d_expr->isConst(), val)
<< "bit-vector constant";
{
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 = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
: d_exprMgr->mkVar(symbol, *sort.d_type);
{
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 = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
: d_exprMgr->mkBoundVar(symbol, *sort.d_type);
CVC4_API_SOLVER_TRY_CATCH_END;
}
+/* Create datatype constructor declarations */
+/* -------------------------------------------------------------------------- */
+
+DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
+ const std::string& name)
+{
+ return DatatypeConstructorDecl(this, name);
+}
+
/* Create datatype declarations */
/* -------------------------------------------------------------------------- */
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(child);
checkMkTerm(kind, 1);
Expr res = d_exprMgr->mkExpr(extToIntKind(kind), *child.d_expr);
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(child1);
+ CVC4_API_SOLVER_CHECK_TERM(child2);
checkMkTerm(kind, 2);
Expr res =
Term Solver::mkTerm(Op op) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_OP(op);
Term res;
if (op.isIndexedHelper())
Term Solver::mkTerm(Op op, Term child) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_OP(op);
CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(child);
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
Expr res;
Term Solver::mkTerm(Op op, Term child1, Term child2) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_OP(op);
CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(child1);
+ CVC4_API_SOLVER_CHECK_TERM(child2);
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
Expr res;
Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_OP(op);
CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
+ CVC4_API_SOLVER_CHECK_TERM(child1);
+ CVC4_API_SOLVER_CHECK_TERM(child2);
+ CVC4_API_SOLVER_CHECK_TERM(child3);
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
Expr res;
Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_OP(op);
for (size_t i = 0, size = children.size(); i < size; ++i)
{
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
- !children[i].isNull(), "parameter term", children[i], i)
+ !children[i].isNull(), "child term", children[i], i)
<< "non-null term";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == children[i].d_solver, "child term", children[i], i)
+ << "child term associated to this solver object";
}
const CVC4::Kind int_kind = extToIntKind(op.d_kind);
std::vector<CVC4::Expr> args;
for (size_t i = 0, size = sorts.size(); i < size; i++)
{
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == terms[i].d_solver, "child term", terms[i], i)
+ << "child term associated to this solver object";
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == sorts[i].d_solver, "child sort", sorts[i], i)
+ << "child sort associated to this solver object";
args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr);
}
/* Non-SMT-LIB commands */
/* -------------------------------------------------------------------------- */
-Term Solver::simplify(const Term& t)
+Term Solver::simplify(const Term& term)
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
- CVC4_API_ARG_CHECK_NOT_NULL(t);
+ CVC4_API_ARG_CHECK_NOT_NULL(term);
+ CVC4_API_SOLVER_CHECK_TERM(term);
- return Term(this, d_smtEngine->simplify(*t.d_expr));
+ return Term(this, d_smtEngine->simplify(*term.d_expr));
CVC4_API_SOLVER_TRY_CATCH_END;
}
<< "Cannot make multiple queries unless incremental solving is enabled "
"(try --incremental)";
CVC4_API_ARG_CHECK_NOT_NULL(term);
+ CVC4_API_SOLVER_CHECK_TERM(term);
CVC4::Result r = d_smtEngine->checkEntailed(*term.d_expr);
return Result(r);
"(try --incremental)";
for (const Term& term : terms)
{
+ CVC4_API_SOLVER_CHECK_TERM(term);
CVC4_API_ARG_CHECK_NOT_NULL(term);
}
*/
void Solver::assertFormula(Term term) const
{
- // CHECK:
- // NodeManager::fromExprManager(d_exprMgr)
- // == NodeManager::fromExprManager(expr.getExprManager())
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_TERM(term);
+ CVC4_API_ARG_CHECK_NOT_NULL(term);
d_smtEngine->assertFormula(*term.d_expr);
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
Result Solver::checkSat(void) const
{
- // CHECK:
- // if d_queryMade -> incremental enabled
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ CVC4_API_CHECK(!d_smtEngine->isQueryMade()
+ || CVC4::options::incrementalSolving())
+ << "Cannot make multiple queries unless incremental solving is enabled "
+ "(try --incremental)";
CVC4::Result r = d_smtEngine->checkSat();
return Result(r);
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
Result Solver::checkSatAssuming(Term assumption) const
{
- // CHECK:
- // if assumptions.size() > 0: incremental enabled?
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ CVC4_API_CHECK(!d_smtEngine->isQueryMade()
+ || CVC4::options::incrementalSolving())
+ << "Cannot make multiple queries unless incremental solving is enabled "
+ "(try --incremental)";
+ CVC4_API_SOLVER_CHECK_TERM(assumption);
CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr);
return Result(r);
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
*/
Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
{
- // CHECK:
- // if assumptions.size() > 0: incremental enabled?
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+ CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
+ || CVC4::options::incrementalSolving())
+ << "Cannot make multiple queries unless incremental solving is enabled "
+ "(try --incremental)";
+ for (const Term& term : assumptions)
+ {
+ CVC4_API_SOLVER_CHECK_TERM(term);
+ CVC4_API_ARG_CHECK_NOT_NULL(term);
+ }
std::vector<Expr> eassumptions = termVectorToExprs(assumptions);
CVC4::Result r = d_smtEngine->checkSat(eassumptions);
return Result(r);
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
const std::string& symbol,
const std::vector<DatatypeConstructorDecl>& ctors) const
{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
<< "a datatype declaration with at least one constructor";
DatatypeDecl dtdecl(this, symbol);
- for (const DatatypeConstructorDecl& ctor : ctors)
+ for (size_t i = 0, size = ctors.size(); i < size; i++)
{
- dtdecl.addConstructor(ctor);
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver,
+ "datatype constructor declaration",
+ ctors[i],
+ i)
+ << "datatype constructor declaration associated to this solver object";
+ dtdecl.addConstructor(ctors[i]);
}
return Sort(this, d_exprMgr->mkDatatypeType(*dtdecl.d_dtype));
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
const std::vector<Sort>& sorts,
Sort sort) const
{
+ CVC4_API_SOLVER_TRY_CATCH_BEGIN;
for (size_t i = 0, size = sorts.size(); i < size; ++i)
{
+ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+ this == sorts[i].d_solver, "parameter sort", sorts[i], i)
+ << "parameter sort associated to this solver object";
CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
<< "first-class sort as parameter sort for function sort";
}
CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
<< "first-class sort as function codomain sort";
+ CVC4_API_SOLVER_CHECK_SORT(sort);
Assert(!sort.isFunction()); /* A function sort is not first-class. */
Type type = *sort.d_type;
if (!sorts.empty())
type = d_exprMgr->mkFunctionType(types, type);
}
return Term(this, d_exprMgr->mkVar(symbol, type));
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
class CVC4_PUBLIC DatatypeConstructorDecl
{
friend class DatatypeDecl;
+ friend class Solver;
public:
/**
- * Constructor.
- * @param name the name of the datatype constructor
- * @return the DatatypeConstructorDecl
+ * Nullary constructor for Cython.
*/
- DatatypeConstructorDecl(const std::string& name);
+ DatatypeConstructorDecl();
/**
* Add datatype selector declaration.
const CVC4::DatatypeConstructor& getDatatypeConstructor(void) const;
private:
+ /**
+ * Constructor.
+ * @param slv the associated solver object
+ * @param name the name of the datatype constructor
+ * @return the DatatypeConstructorDecl
+ */
+ DatatypeConstructorDecl(const Solver* slv, const std::string& name);
+
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/**
* The internal (intermediate) datatype constructor wrapped by this
* datatype constructor declaration.
public:
/**
- * Nullary constructor for Cython
+ * Nullary constructor for Cython.
*/
DatatypeDecl();
/** Is this Datatype declaration parametric? */
bool isParametric() const;
+ /**
+ * @return true if this DatatypeDecl is a null object
+ */
bool isNull() const;
/**
private:
/**
* Constructor.
- * @param slv the solver that created this datatype declaration
+ * @param slv the associated solver object
* @param name the name of the datatype
* @param isCoDatatype true if a codatatype is to be constructed
* @return the DatatypeDecl
/**
* Constructor for parameterized datatype declaration.
* Create sorts parameter with Solver::mkParamSort().
- * @param slv the solver that created this datatype declaration
+ * @param slv the associated solver object
* @param name the name of the datatype
* @param param the sort parameter
* @param isCoDatatype true if a codatatype is to be constructed
/**
* Constructor for parameterized datatype declaration.
* Create sorts parameter with Solver::mkParamSort().
- * @param slv the solver that created this datatype declaration
+ * @param slv the associated solver object
* @param name the name of the datatype
* @param params a list of sort parameters
* @param isCoDatatype true if a codatatype is to be constructed
const std::vector<Sort>& params,
bool isCoDatatype = false);
- // helper for isNull() to avoid calling API functions from other API functions
+ /**
+ * Helper for isNull checks. This prevents calling an API function with
+ * CVC4_API_CHECK_NOT_NULL
+ */
bool isNullHelper() const;
+ /**
+ * The associated solver object.
+ */
+ const Solver* d_solver;
+
/* The internal (intermediate) datatype wrapped by this datatype
* declaration
* This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
*/
Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
+ /* .................................................................... */
+ /* Create datatype constructor declarations */
+ /* .................................................................... */
+
+ DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
+
/* .................................................................... */
/* Create datatype declarations */
/* .................................................................... */
cdef cppclass DatatypeConstructorDecl:
- DatatypeConstructorDecl(const string& name) except +
void addSelector(const string& name, Sort sort) except +
void addSelectorSelf(const string& name) except +
string toString() except +
# default value for symbol defined in cvc4cpp.h
Term mkConst(Sort sort) except +
Term mkVar(Sort sort, const string& symbol) except +
+ DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except +
DatatypeDecl mkDatatypeDecl(const string& name) except +
DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except +
DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except +
cdef class DatatypeConstructorDecl:
- cdef c_DatatypeConstructorDecl* cddc
- def __cinit__(self, str name):
- self.cddc = new c_DatatypeConstructorDecl(name.encode())
+ cdef c_DatatypeConstructorDecl cddc
+
+ def __cinit__(self):
+ pass
def addSelector(self, str name, Sort sort):
self.cddc.addSelector(name.encode(), sort.csort)
+
def addSelectorSelf(self, str name):
self.cddc.addSelectorSelf(name.encode())
pass
def addConstructor(self, DatatypeConstructorDecl ctor):
- self.cdd.addConstructor(ctor.cddc[0])
+ self.cdd.addConstructor(ctor.cddc)
def isParametric(self):
return self.cdd.isParametric()
(<str?> symbol).encode())
return term
+ def mkDatatypeConstructorDecl(self, str name):
+ cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl()
+ ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode())
+ return ddc
+
def mkDatatypeDecl(self, str name, sorts_or_bool=None, isCoDatatype=None):
cdef DatatypeDecl dd = DatatypeDecl()
cdef vector[c_Sort] v
cdef vector[c_DatatypeConstructorDecl] v
for c in ctors:
- v.push_back((<DatatypeConstructorDecl?> c).cddc[0])
+ v.push_back((<DatatypeConstructorDecl?> c).cddc)
sort.csort = self.csolver.declareDatatype(symbol.encode(), v)
return sort
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
api::Term func = PARSER_STATE->mkVar(
*i,
- api::Sort(PARSER_STATE->getSolver(), t.getType()),
+ api::Sort(SOLVER, t.getType()),
ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
PARSER_STATE->defineVar(*i, f);
Command* decl =
}
const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
f2 = SOLVER->mkTerm(
- api::APPLY_SELECTOR,
- api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
- f);
+ api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
}
const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
f2 = SOLVER->mkTerm(
- api::APPLY_SELECTOR,
- api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
- f);
+ api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f);
}
( ( arrayStore[f2]
| DOT ( tupleStore[f2]
PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
}
const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
- f = SOLVER->mkTerm(
- api::APPLY_SELECTOR,
- api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
- f);
+ f = SOLVER->mkTerm(api::APPLY_SELECTOR,
+ api::Term(SOLVER, dt[0][id].getSelector()),
+ f);
}
| k=numeral
{
PARSER_STATE->parseError(ss.str());
}
const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
- f = SOLVER->mkTerm(
- api::APPLY_SELECTOR,
- api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
- f);
+ f = SOLVER->mkTerm(api::APPLY_SELECTOR,
+ api::Term(SOLVER, dt[0][k].getSelector()),
+ f);
}
)
)*
types.push_back(f.getSort());
api::Sort t = SOLVER->mkTupleSort(types);
const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
- args.insert(args.begin(),
- api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
| IDEN_TOK LPAREN formula[f] RPAREN
}
api::Sort dtype = SOLVER->mkTupleSort(types);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- args.insert(
- args.begin(),
- api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
}
api::Sort dtype = SOLVER->mkTupleSort(types);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
f = MK_TERM(api::APPLY_CONSTRUCTOR,
- api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ api::Term(SOLVER, dt[0].getConstructor()));
}
/* empty record literal */
std::vector<std::pair<std::string, api::Sort>>());
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
f = MK_TERM(api::APPLY_CONSTRUCTOR,
- api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ api::Term(SOLVER, dt[0].getConstructor()));
}
/* empty set literal */
| LBRACE RBRACE
}
api::Sort dtype = SOLVER->mkRecordSort(typeIds);
const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
- args.insert(args.begin(),
- api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+ args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
}
std::unique_ptr<CVC4::api::DatatypeConstructorDecl> ctor;
}
: identifier[id,CHECK_UNDECLARED,SYM_SORT]
- {
- ctor.reset(new CVC4::api::DatatypeConstructorDecl(id));
+ {
+ ctor.reset(new CVC4::api::DatatypeConstructorDecl(
+ SOLVER->mkDatatypeConstructorDecl(id)));
}
( LPAREN
selector[&ctor]
PARSER_STATE->getUnresolvedSorts().clear();
- ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
+ ret = api::Sort(SOLVER, datatypeTypes[0]);
};
// SyGuS grammar term.
if (Datatype::datatypeOf(ef).isParametric())
{
type = api::Sort(
- PARSER_STATE->getSolver(),
+ SOLVER,
Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
.getSpecializedConstructorType(expr.getSort().getType()));
}
}
: symbol[id,CHECK_NONE,SYM_VARIABLE]
{
- ctor = new api::DatatypeConstructorDecl(id);
+ ctor = new api::DatatypeConstructorDecl(
+ SOLVER->mkDatatypeConstructorDecl(id));
}
( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
{ // make the constructor
PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
- lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
+ lhs = api::Term(SOLVER, lhs.getExpr().getOperator());
}
| LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
;
PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
- lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
+ lhs = api::Term(SOLVER, lhs.getExpr().getOperator());
}
| LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
;
void DatatypeBlack::testMkDatatypeSort()
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver.getIntegerSort());
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
Datatype d = listSort.getDatatype();
unresTypes.insert(unresList);
DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
- DatatypeConstructorDecl node("node");
+ DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
node.addSelector("left", unresTree);
node.addSelector("right", unresTree);
tree.addConstructor(node);
- DatatypeConstructorDecl leaf("leaf");
+ DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
leaf.addSelector("data", unresList);
tree.addConstructor(leaf);
DatatypeDecl list = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("car", unresTree);
cons.addSelector("cdr", unresTree);
list.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
list.addConstructor(nil);
std::vector<DatatypeDecl> dtdecls;
// create datatype sort to test
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", intSort);
cons.addSelectorSelf("tail");
Sort nullSort;
TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
Datatype dt = dtypeSort.getDatatype();
// create datatype sort to test
DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
- DatatypeConstructorDecl ca("A");
+ DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A");
dtypeSpecEnum.addConstructor(ca);
- DatatypeConstructorDecl cb("B");
+ DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B");
dtypeSpecEnum.addConstructor(cb);
- DatatypeConstructorDecl cc("C");
+ DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C");
dtypeSpecEnum.addConstructor(cc);
Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
Datatype dtEnum = dtypeSortEnum.getDatatype();
// create codatatype
DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
- DatatypeConstructorDecl consStream("cons");
+ DatatypeConstructorDecl consStream =
+ d_solver.mkDatatypeConstructorDecl("cons");
consStream.addSelector("head", intSort);
consStream.addSelectorSelf("tail");
dtypeSpecStream.addConstructor(consStream);
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
TS_ASSERT(dtypeSpec.getName() == std::string("list"));
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", intSort);
cons.addSelectorSelf("tail");
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
Datatype dt = dtypeSort.getDatatype();
void testMkBitVectorSort();
void testMkFloatingPointSort();
void testMkDatatypeSort();
+ void testMkDatatypeSorts();
void testMkFunctionSort();
void testMkOp();
void testMkParamSort();
void testPop3();
void testSimplify();
+
+ void testAssertFormula();
void testCheckEntailed();
void testCheckEntailed1();
void testCheckEntailed2();
+ void testCheckSat();
+ void testCheckSatAssuming();
+ void testCheckSatAssuming1();
+ void testCheckSatAssuming2();
void testSetInfo();
void testSetLogic();
TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort));
TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort));
TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&);
}
void SolverBlack::testMkBitVectorSort()
void SolverBlack::testMkDatatypeSort()
{
DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver->getIntegerSort());
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec));
+
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException&);
+
DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec),
CVC4ApiException&);
}
+void SolverBlack::testMkDatatypeSorts()
+{
+ Solver slv;
+
+ DatatypeDecl dtypeSpec1 = d_solver->mkDatatypeDecl("list1");
+ DatatypeConstructorDecl cons1 = d_solver->mkDatatypeConstructorDecl("cons1");
+ cons1.addSelector("head1", d_solver->getIntegerSort());
+ dtypeSpec1.addConstructor(cons1);
+ DatatypeConstructorDecl nil1 = d_solver->mkDatatypeConstructorDecl("nil1");
+ dtypeSpec1.addConstructor(nil1);
+ DatatypeDecl dtypeSpec2 = d_solver->mkDatatypeDecl("list2");
+ DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons2");
+ cons2.addSelector("head2", d_solver->getIntegerSort());
+ dtypeSpec2.addConstructor(cons2);
+ DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil2");
+ dtypeSpec2.addConstructor(nil2);
+ std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(decls));
+
+ TS_ASSERT_THROWS(slv.mkDatatypeSorts(decls), CVC4ApiException&);
+
+ DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
+ std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
+ TS_ASSERT_THROWS(d_solver->mkDatatypeSorts(throwsDecls), CVC4ApiException&);
+
+ /* with unresolved sorts */
+ Sort unresList = d_solver->mkUninterpretedSort("ulist");
+ std::set<Sort> unresSorts = {unresList};
+ DatatypeDecl ulist = d_solver->mkDatatypeDecl("ulist");
+ DatatypeConstructorDecl ucons = d_solver->mkDatatypeConstructorDecl("ucons");
+ ucons.addSelector("car", unresList);
+ ucons.addSelector("cdr", unresList);
+ ulist.addConstructor(ucons);
+ DatatypeConstructorDecl unil = d_solver->mkDatatypeConstructorDecl("unil");
+ ulist.addConstructor(unil);
+ std::vector<DatatypeDecl> udecls = {ulist};
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(udecls, unresSorts));
+
+ TS_ASSERT_THROWS(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException&);
+
+ /* Note: More tests are in datatype_api_black. */
+}
+
void SolverBlack::testMkFunctionSort()
{
TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort(
{d_solver->getIntegerSort(), d_solver->mkUninterpretedSort("u")},
funSort2),
CVC4ApiException&);
+
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkFunctionSort(d_solver->mkUninterpretedSort("u"),
+ d_solver->getIntegerSort()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
+ d_solver->getIntegerSort()),
+ CVC4ApiException&);
+ std::vector<Sort> sorts1 = {d_solver->getBooleanSort(),
+ slv.getIntegerSort(),
+ d_solver->getIntegerSort()};
+ std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
+ TS_ASSERT_THROWS_NOTHING(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
+ TS_ASSERT_THROWS(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkFunctionSort(sorts2, d_solver->getIntegerSort()),
+ CVC4ApiException&);
}
void SolverBlack::testMkParamSort()
TS_ASSERT_THROWS(
d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}),
CVC4ApiException&);
+
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkPredicateSort({d_solver->getIntegerSort()}),
+ CVC4ApiException&);
}
void SolverBlack::testMkRecordSort()
TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
Sort recSort = d_solver->mkRecordSort(fields);
TS_ASSERT_THROWS_NOTHING(recSort.getDatatype());
+
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkRecordSort(fields), CVC4ApiException&);
}
void SolverBlack::testMkSetSort()
TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getBooleanSort()));
TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getIntegerSort()));
TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->mkBitVectorSort(4)));
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkSetSort(d_solver->mkBitVectorSort(4)),
+ CVC4ApiException&);
}
void SolverBlack::testMkUninterpretedSort()
d_solver->getIntegerSort());
TS_ASSERT_THROWS(d_solver->mkTupleSort({d_solver->getIntegerSort(), funSort}),
CVC4ApiException&);
+
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkTupleSort({d_solver->getIntegerSort()}),
+ CVC4ApiException&);
}
void SolverBlack::testMkBitVector()
TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkVar(boolSort, "x"), CVC4ApiException&);
}
void SolverBlack::testMkBoolean()
d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1));
TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1),
CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkUninterpretedConst(d_solver->getBooleanSort(), 1),
+ CVC4ApiException&);
}
void SolverBlack::testMkAbstractValue()
TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 0, t1), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
+
+ if (CVC4::Configuration::isBuiltWithSymFPU())
+ {
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException&);
+ }
}
void SolverBlack::testMkEmptySet()
{
+ Solver slv;
+ Sort s = d_solver->mkSetSort(d_solver->getBooleanSort());
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
+ TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(s));
TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()),
CVC4ApiException&);
- TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
+ TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
}
void SolverBlack::testMkFalse()
{
TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort()));
TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkSepNil(d_solver->getIntegerSort()), CVC4ApiException&);
}
void SolverBlack::testMkString()
std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
std::vector<Term> v6 = {};
+ Solver slv;
// mkTerm(Kind kind) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI));
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue()));
TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(NOT, a), CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkTerm(NOT, d_solver->mkTrue()), CVC4ApiException&);
// mkTerm(Kind kind, Term child1, Term child2) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, a, b));
TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, Term()), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, d_solver->mkTrue()),
CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkTerm(EQUAL, a, b), CVC4ApiException&);
// mkTerm(Kind kind, Term child1, Term child2, Term child3) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
TS_ASSERT_THROWS(
d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b),
CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ slv.mkTerm(
+ ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue()),
+ CVC4ApiException&);
// mkTerm(Kind kind, const std::vector<Term>& children) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1));
std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
std::vector<Term> v3 = {};
std::vector<Term> v4 = {d_solver->mkReal(5)};
+ Solver slv;
+
// simple operator terms
Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
Op opterm2 = d_solver->mkOp(DIVISIBLE, 1);
- // list datatype
+ // list datatype
Sort sort = d_solver->mkParamSort("T");
DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort);
- DatatypeConstructorDecl cons("cons");
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
cons.addSelector("head", sort);
cons.addSelectorSelf("tail");
listDecl.addConstructor(cons);
listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
Term c = d_solver->mkConst(intListSort, "c");
Datatype list = listSort.getDatatype();
+
// list datatype constructor and selector operator terms
Term consTerm1 = list.getConstructorTerm("cons");
Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException&);
// mkTerm(Op op, Term child) const
TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
TS_ASSERT_THROWS(
d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
// mkTerm(Op op, Term child1, Term child2) const
- TS_ASSERT_THROWS(
- d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
- CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(
d_solver->mkTerm(APPLY_CONSTRUCTOR,
consTerm1,
d_solver->mkReal(0),
d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+ TS_ASSERT_THROWS(
+ d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
+ CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()),
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)),
CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
+ consTerm1,
+ d_solver->mkReal(0),
+ d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
+ CVC4ApiException&);
- // mkTerm(Op op, Term child1, Term child2, Term child3)
- // const
+ // mkTerm(Op op, Term child1, Term child2, Term child3) const
TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
TS_ASSERT_THROWS(
d_solver->mkTerm(
TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v1), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v2), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v3), CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkTerm(opterm2, v4), CVC4ApiException&);
}
void SolverBlack::testMkTrue()
TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->getIntegerSort()},
{d_solver->mkReal("5.3")}),
CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(
+ slv.mkTuple({d_solver->mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
+ CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}),
+ CVC4ApiException&);
}
void SolverBlack::testMkUniverseSet()
{
- TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort()));
+ TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkUniverseSet(d_solver->getBooleanSort()),
+ CVC4ApiException&);
}
void SolverBlack::testMkConst()
TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, ""));
TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
+
+ Solver slv;
+ TS_ASSERT_THROWS(slv.mkConst(boolSort), CVC4ApiException&);
}
void SolverBlack::testMkConstArray()
Term constArr = d_solver->mkConstArray(arrSort, zero);
TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
+ TS_ASSERT_THROWS(d_solver->mkConstArray(Sort(), zero), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, Term()), CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, d_solver->mkBitVector(1, 1)),
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
+ Solver slv;
+ Term zero2 = slv.mkReal(0);
+ Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
+ TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
+ TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
}
void SolverBlack::testDeclareDatatype()
{
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
std::vector<DatatypeConstructorDecl> ctors1 = {nil};
TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
- DatatypeConstructorDecl cons("cons");
- DatatypeConstructorDecl nil2("nil");
+ DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil");
std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
- DatatypeConstructorDecl cons2("cons");
- DatatypeConstructorDecl nil3("nil");
+ DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl nil3 = d_solver->mkDatatypeConstructorDecl("nil");
std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3));
std::vector<DatatypeConstructorDecl> ctors4;
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4),
CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.declareDatatype(std::string("a"), ctors1),
+ CVC4ApiException&);
}
void SolverBlack::testDeclareFun()
CVC4ApiException&);
TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort),
CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.declareFun("f1", {}, bvSort), CVC4ApiException&);
}
void SolverBlack::testDeclareSort()
// Test Datatypes -- more complicated
DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver->getIntegerSort());
cons.addSelectorSelf("tail");
consListSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
consListSpec.addConstructor(nil);
Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
Datatype consList = consListSort.getDatatype();
Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver->getIntegerSort());
cons.addSelectorSelf("tail");
consListSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
consListSpec.addConstructor(nil);
Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b));
TS_ASSERT(d_solver->mkTrue() != x_eq_b);
TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b));
+ Solver slv;
+ TS_ASSERT_THROWS(slv.simplify(x), CVC4ApiException&);
Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
}
+void SolverBlack::testAssertFormula()
+{
+ TS_ASSERT_THROWS_NOTHING(d_solver->assertFormula(d_solver->mkTrue()));
+ TS_ASSERT_THROWS(d_solver->assertFormula(Term()), CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.assertFormula(d_solver->mkTrue()), CVC4ApiException&);
+}
+
void SolverBlack::testCheckEntailed()
{
d_solver->setOption("incremental", "false");
TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
}
void SolverBlack::testCheckEntailed1()
TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
+ Solver slv;
+ TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
}
void SolverBlack::testCheckEntailed2()
TS_ASSERT_THROWS(
d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSat()
+{
+ d_solver->setOption("incremental", "false");
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSat());
+ TS_ASSERT_THROWS(d_solver->checkSat(), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming()
+{
+ d_solver->setOption("incremental", "false");
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+ TS_ASSERT_THROWS(d_solver->checkSatAssuming(d_solver->mkTrue()),
+ CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming1()
+{
+ Sort boolSort = d_solver->getBooleanSort();
+ Term x = d_solver->mkConst(boolSort, "x");
+ Term y = d_solver->mkConst(boolSort, "y");
+ Term z = d_solver->mkTerm(AND, x, y);
+ d_solver->setOption("incremental", "true");
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+ TS_ASSERT_THROWS(d_solver->checkSatAssuming(Term()), CVC4ApiException&);
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(z));
+ Solver slv;
+ TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming2()
+{
+ d_solver->setOption("incremental", "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);
+
+ Term n = Term();
+ // Constants
+ Term x = d_solver->mkConst(uSort, "x");
+ Term y = d_solver->mkConst(uSort, "y");
+ // Functions
+ Term f = d_solver->mkConst(uToIntSort, "f");
+ Term p = d_solver->mkConst(intPredSort, "p");
+ // Values
+ Term zero = d_solver->mkReal(0);
+ Term one = d_solver->mkReal(1);
+ // Terms
+ 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);
+ // Assertions
+ Term assertions =
+ d_solver->mkTerm(AND,
+ std::vector<Term>{
+ d_solver->mkTerm(LEQ, zero, f_x), // 0 <= f(x)
+ d_solver->mkTerm(LEQ, zero, f_y), // 0 <= f(y)
+ d_solver->mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
+ p_0.notTerm(), // not p(0)
+ p_f_y // p(f(y))
+ });
+
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+ d_solver->assertFormula(assertions);
+ TS_ASSERT_THROWS_NOTHING(
+ d_solver->checkSatAssuming(d_solver->mkTerm(DISTINCT, x, y)));
+ TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(
+ {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
+ TS_ASSERT_THROWS(d_solver->checkSatAssuming(n), CVC4ApiException&);
+ TS_ASSERT_THROWS(
+ d_solver->checkSatAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
+ CVC4ApiException&);
+ Solver slv;
+ TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
}
void SolverBlack::testSetLogic()
{
// create datatype sort, check should not fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver.getIntegerSort());
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
Sort intSort = d_solver.getIntegerSort();
// create datatype sort to test
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", intSort);
cons.addSelectorSelf("tail");
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
Datatype dt = dtypeSort.getDatatype();
// instantiate parametric datatype, check should not fail
Sort sort = d_solver.mkParamSort("T");
DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
- DatatypeConstructorDecl paramCons("cons");
- DatatypeConstructorDecl paramNil("nil");
+ DatatypeConstructorDecl paramCons =
+ d_solver.mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
paramCons.addSelector("head", sort);
paramDtypeSpec.addConstructor(paramCons);
paramDtypeSpec.addConstructor(paramNil);
paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
// instantiate non-parametric datatype sort, check should fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver.getIntegerSort());
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
TS_ASSERT_THROWS(
// create parametric datatype, check should not fail
Sort sort = d_solver.mkParamSort("T");
DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
- DatatypeConstructorDecl paramCons("cons");
- DatatypeConstructorDecl paramNil("nil");
+ DatatypeConstructorDecl paramCons =
+ d_solver.mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
paramCons.addSelector("head", sort);
paramDtypeSpec.addConstructor(paramCons);
paramDtypeSpec.addConstructor(paramNil);
TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
// create non-parametric datatype sort, check should fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver.getIntegerSort());
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
{
// create datatype sort, check should not fail
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
- DatatypeConstructorDecl cons("cons");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
cons.addSelector("head", d_solver.getIntegerSort());
dtypeSpec.addConstructor(cons);
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
dtypeSpec.addConstructor(nil);
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
// Test Datatypes Ops
Sort sort = d_solver.mkParamSort("T");
DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
- DatatypeConstructorDecl cons("cons");
- DatatypeConstructorDecl nil("nil");
+ DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+ DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
cons.addSelector("head", sort);
cons.addSelectorSelf("tail");
listDecl.addConstructor(cons);
projects / cvc5.git / commitdiff