summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/api/datatypes-new.cpp12
-rwxr-xr-xexamples/api/python/datatypes.py12
-rw-r--r--src/api/cvc4cpp.cpp210
-rw-r--r--src/api/cvc4cpp.h47
-rw-r--r--src/api/python/cvc4.pxd2
-rw-r--r--src/api/python/cvc4.pxi17
-rw-r--r--src/parser/cvc/Cvc.g43
-rw-r--r--src/parser/smt2/Smt2.g7
-rw-r--r--src/parser/tptp/Tptp.g4
-rw-r--r--test/unit/api/datatype_api_black.h29
-rw-r--r--test/unit/api/solver_black.h286
-rw-r--r--test/unit/api/sort_black.h30
-rw-r--r--test/unit/api/term_black.h4
13 files changed, 559 insertions, 144 deletions
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 9cfc7992c..500cb0710 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -91,8 +91,8 @@ void test(Solver& slv, Sort& consListSort)
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);
@@ -144,11 +144,11 @@ int main()
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;
@@ -167,10 +167,10 @@ int main()
<< ">>> 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);
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index ded268d69..1a67f5661 100755
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -65,8 +65,8 @@ def test(slv, consListSort):
# 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)
@@ -102,11 +102,11 @@ if __name__ == "__main__":
# 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))
@@ -122,10 +122,10 @@ if __name__ == "__main__":
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)
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0bfb9a325..f225da333 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -702,8 +702,6 @@ class CVC4ApiExceptionStream
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 \
@@ -726,12 +724,12 @@ class CVC4ApiExceptionStream
& 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 \
@@ -741,6 +739,19 @@ class CVC4ApiExceptionStream
} \
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
/* -------------------------------------------------------------------------- */
@@ -1612,6 +1623,7 @@ Term::const_iterator::const_iterator(const const_iterator& it)
{
if (it.d_orig_expr != nullptr)
{
+ d_solver = it.d_solver;
d_orig_expr = it.d_orig_expr;
d_pos = it.d_pos;
}
@@ -1619,6 +1631,7 @@ Term::const_iterator::const_iterator(const const_iterator& it)
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;
@@ -1630,7 +1643,8 @@ bool Term::const_iterator::operator==(const const_iterator& it) const
{
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
@@ -1756,8 +1770,14 @@ size_t TermHashFunction::operator()(const Term& t) 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))
{
}
@@ -1804,10 +1824,13 @@ std::ostream& operator<<(std::ostream& out,
/* 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))
{
}
@@ -1815,7 +1838,8 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
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))
@@ -1826,6 +1850,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
const std::string& name,
const std::vector<Sort>& params,
bool isCoDatatype)
+ : d_solver(slv)
{
std::vector<Type> tparams;
for (const Sort& p : params)
@@ -1838,8 +1863,6 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
-DatatypeDecl::DatatypeDecl() {}
-
DatatypeDecl::~DatatypeDecl() {}
void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
@@ -2683,8 +2706,11 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
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);
@@ -2749,13 +2775,24 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
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);
@@ -2778,6 +2815,7 @@ std::vector<Type> Solver::sortVectorToTypes(
std::vector<Type> res;
for (const Sort& s : sorts)
{
+ CVC4_API_SOLVER_CHECK_SORT(s);
res.push_back(*s.d_type);
}
return res;
@@ -2789,6 +2827,7 @@ std::vector<Expr> Solver::termVectorToExprs(
std::vector<Expr> res;
for (const Term& t : terms)
{
+ CVC4_API_SOLVER_CHECK_TERM(t);
res.push_back(*t.d_expr);
}
return res;
@@ -2877,6 +2916,8 @@ Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
<< "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));
@@ -2908,6 +2949,8 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
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";
@@ -2934,6 +2977,8 @@ Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
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)
@@ -2957,11 +3002,15 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
!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. */
@@ -2991,6 +3040,9 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
!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";
}
@@ -3012,6 +3064,9 @@ Sort Solver::mkRecordSort(
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);
}
@@ -3026,6 +3081,7 @@ Sort Solver::mkSetSort(Sort elemSort) const
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));
@@ -3059,6 +3115,9 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
!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";
}
@@ -3207,6 +3266,8 @@ Term Solver::mkEmptySet(Sort s) const
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));
@@ -3217,6 +3278,7 @@ Term Solver::mkSepNil(Sort sort) const
{
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 */
@@ -3272,6 +3334,7 @@ Term Solver::mkUniverseSet(Sort sort) const
{
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);
@@ -3324,7 +3387,10 @@ Term Solver::mkBitVector(uint32_t size, std::string& s, uint32_t base) const
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.";
@@ -3405,6 +3471,7 @@ Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
{
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));
@@ -3448,6 +3515,7 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
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";
@@ -3465,6 +3533,7 @@ Term Solver::mkConst(Sort sort, const std::string& symbol) const
{
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);
@@ -3481,6 +3550,7 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
{
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);
@@ -3490,6 +3560,15 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
CVC4_API_SOLVER_TRY_CATCH_END;
}
+/* Create datatype constructor declarations */
+/* -------------------------------------------------------------------------- */
+
+DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
+ const std::string& name)
+{
+ return DatatypeConstructorDecl(this, name);
+}
+
/* Create datatype declarations */
/* -------------------------------------------------------------------------- */
@@ -3526,6 +3605,7 @@ Term Solver::mkTerm(Kind kind, Term child) const
{
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);
@@ -3540,6 +3620,8 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
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 =
@@ -3564,6 +3646,7 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
Term Solver::mkTerm(Op op) const
{
CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+ CVC4_API_SOLVER_CHECK_OP(op);
Term res;
if (op.isIndexedHelper())
@@ -3585,7 +3668,9 @@ Term Solver::mkTerm(Op op) const
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;
@@ -3607,8 +3692,11 @@ Term Solver::mkTerm(Op op, Term child) const
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;
@@ -3630,9 +3718,13 @@ Term Solver::mkTerm(Op op, Term child1, Term child2) const
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;
@@ -3656,11 +3748,15 @@ Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
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);
@@ -3690,6 +3786,12 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts,
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);
}
@@ -3913,12 +4015,13 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
/* 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;
}
@@ -3932,6 +4035,7 @@ Result Solver::checkEntailed(Term term) const
<< "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);
@@ -3949,6 +4053,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
"(try --incremental)";
for (const Term& term : terms)
{
+ CVC4_API_SOLVER_CHECK_TERM(term);
CVC4_API_ARG_CHECK_NOT_NULL(term);
}
@@ -3967,10 +4072,11 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
*/
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;
}
/**
@@ -3978,10 +4084,15 @@ void Solver::assertFormula(Term term) const
*/
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;
}
/**
@@ -3989,10 +4100,16 @@ Result Solver::checkSat(void) const
*/
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;
}
/**
@@ -4000,11 +4117,21 @@ Result Solver::checkSatAssuming(Term assumption) const
*/
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;
}
/**
@@ -4014,14 +4141,21 @@ Sort Solver::declareDatatype(
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;
}
/**
@@ -4031,14 +4165,19 @@ Term Solver::declareFun(const std::string& symbol,
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())
@@ -4047,6 +4186,7 @@ Term Solver::declareFun(const std::string& symbol,
type = d_exprMgr->mkFunctionType(types, type);
}
return Term(this, d_exprMgr->mkVar(symbol, type));
+ CVC4_API_SOLVER_TRY_CATCH_END;
}
/**
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 87be7b74c..855ba4400 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1167,14 +1167,13 @@ class DatatypeIterator;
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.
@@ -1199,6 +1198,19 @@ class CVC4_PUBLIC DatatypeConstructorDecl
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.
* This is a shared_ptr rather than a unique_ptr since
@@ -1219,7 +1231,7 @@ class CVC4_PUBLIC DatatypeDecl
public:
/**
- * Nullary constructor for Cython
+ * Nullary constructor for Cython.
*/
DatatypeDecl();
@@ -1240,6 +1252,9 @@ class CVC4_PUBLIC DatatypeDecl
/** Is this Datatype declaration parametric? */
bool isParametric() const;
+ /**
+ * @return true if this DatatypeDecl is a null object
+ */
bool isNull() const;
/**
@@ -1257,7 +1272,7 @@ class CVC4_PUBLIC DatatypeDecl
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
@@ -1269,7 +1284,7 @@ class CVC4_PUBLIC 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
@@ -1282,7 +1297,7 @@ class CVC4_PUBLIC 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 params a list of sort parameters
* @param isCoDatatype true if a codatatype is to be constructed
@@ -1292,9 +1307,17 @@ class CVC4_PUBLIC DatatypeDecl
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
@@ -2680,6 +2703,12 @@ class CVC4_PUBLIC Solver
Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
/* .................................................................... */
+ /* Create datatype constructor declarations */
+ /* .................................................................... */
+
+ DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
+
+ /* .................................................................... */
/* Create datatype declarations */
/* .................................................................... */
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 1c7071958..2ca4b3645 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -54,7 +54,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
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 +
@@ -160,6 +159,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
# 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 +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index fa5313f0e..e742e0061 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -134,12 +134,14 @@ cdef class DatatypeConstructor:
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())
@@ -156,7 +158,7 @@ cdef class DatatypeDecl:
pass
def addConstructor(self, DatatypeConstructorDecl ctor):
- self.cdd.addConstructor(ctor.cddc[0])
+ self.cdd.addConstructor(ctor.cddc)
def isParametric(self):
return self.cdd.isParametric()
@@ -675,6 +677,11 @@ cdef class Solver:
(<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
@@ -790,7 +797,7 @@ cdef class Solver:
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
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index fdb6a081c..e604c7769 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
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 =
@@ -1654,9 +1654,7 @@ tupleStore[CVC4::api::Term& f]
}
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]
@@ -1689,9 +1687,7 @@ recordStore[CVC4::api::Term& f]
}
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]
@@ -1835,10 +1831,9 @@ postfixTerm[CVC4::api::Term& f]
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
{
@@ -1853,10 +1848,9 @@ postfixTerm[CVC4::api::Term& f]
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);
}
)
)*
@@ -1896,8 +1890,7 @@ relationTerm[CVC4::api::Term& 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
@@ -2147,9 +2140,7 @@ simpleTerm[CVC4::api::Term& f]
}
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);
}
}
@@ -2160,7 +2151,7 @@ simpleTerm[CVC4::api::Term& f]
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 */
@@ -2170,7 +2161,7 @@ simpleTerm[CVC4::api::Term& f]
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
@@ -2268,8 +2259,7 @@ simpleTerm[CVC4::api::Term& f]
}
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);
}
@@ -2377,8 +2367,9 @@ constructorDef[CVC4::api::DatatypeDecl& type]
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]
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f29e03380..62bf7e974 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
PARSER_STATE->getUnresolvedSorts().clear();
- ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
+ ret = api::Sort(SOLVER, datatypeTypes[0]);
};
// SyGuS grammar term.
@@ -1798,7 +1798,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
if (Datatype::datatypeOf(ef).isParametric())
{
type = api::Sort(
- PARSER_STATE->getSolver(),
+ SOLVER,
Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
.getSpecializedConstructorType(expr.getSort().getType()));
}
@@ -2521,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type]
}
: 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
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c1d60ca31..e26709595 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
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
;
@@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
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
;
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index b404dfb13..c9eaf103e 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -43,10 +43,10 @@ void DatatypeBlack::tearDown() {}
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();
@@ -75,22 +75,22 @@ void DatatypeBlack::testMkDatatypeSorts()
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;
@@ -130,13 +130,13 @@ void DatatypeBlack::testDatatypeStructs()
// 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();
@@ -152,11 +152,11 @@ void DatatypeBlack::testDatatypeStructs()
// 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();
@@ -165,7 +165,8 @@ void DatatypeBlack::testDatatypeStructs()
// 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);
@@ -204,11 +205,11 @@ void DatatypeBlack::testDatatypeNames()
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();
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 90d4c10c1..7e925df54 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -39,6 +39,7 @@ class SolverBlack : public CxxTest::TestSuite
void testMkBitVectorSort();
void testMkFloatingPointSort();
void testMkDatatypeSort();
+ void testMkDatatypeSorts();
void testMkFunctionSort();
void testMkOp();
void testMkParamSort();
@@ -96,9 +97,15 @@ class SolverBlack : public CxxTest::TestSuite
void testPop3();
void testSimplify();
+
+ void testAssertFormula();
void testCheckEntailed();
void testCheckEntailed1();
void testCheckEntailed2();
+ void testCheckSat();
+ void testCheckSatAssuming();
+ void testCheckSatAssuming1();
+ void testCheckSatAssuming2();
void testSetInfo();
void testSetLogic();
@@ -173,6 +180,8 @@ void SolverBlack::testMkArraySort()
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()
@@ -191,17 +200,64 @@ void SolverBlack::testMkFloatingPointSort()
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(
@@ -228,6 +284,23 @@ void SolverBlack::testMkFunctionSort()
{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()
@@ -246,6 +319,10 @@ void SolverBlack::testMkPredicateSort()
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()
@@ -259,6 +336,9 @@ 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()
@@ -266,6 +346,9 @@ 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()
@@ -288,6 +371,10 @@ void SolverBlack::testMkTupleSort()
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()
@@ -332,6 +419,8 @@ void SolverBlack::testMkVar()
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()
@@ -352,6 +441,9 @@ void SolverBlack::testMkUninterpretedConst()
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()
@@ -393,13 +485,23 @@ void SolverBlack::testMkFloatingPoint()
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()
@@ -558,6 +660,8 @@ void SolverBlack::testMkSepNil()
{
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()
@@ -592,6 +696,7 @@ void SolverBlack::testMkTerm()
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));
@@ -603,6 +708,7 @@ void SolverBlack::testMkTerm()
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));
@@ -610,6 +716,7 @@ void SolverBlack::testMkTerm()
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(
@@ -626,6 +733,10 @@ void SolverBlack::testMkTerm()
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));
@@ -643,15 +754,17 @@ void SolverBlack::testMkTermFromOp()
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);
@@ -661,6 +774,7 @@ void SolverBlack::testMkTermFromOp()
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();
@@ -684,6 +798,7 @@ void SolverBlack::testMkTermFromOp()
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));
@@ -695,24 +810,29 @@ void SolverBlack::testMkTermFromOp()
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(
@@ -724,6 +844,7 @@ void SolverBlack::testMkTermFromOp()
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()
@@ -747,12 +868,22 @@ void SolverBlack::testMkTuple()
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()
@@ -768,6 +899,9 @@ 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()
@@ -778,23 +912,29 @@ 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;
@@ -802,6 +942,9 @@ void SolverBlack::testDeclareDatatype()
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()
@@ -817,6 +960,8 @@ 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()
@@ -959,11 +1104,11 @@ void SolverBlack::testGetOp()
// 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();
@@ -1059,11 +1204,11 @@ void SolverBlack::testSimplify()
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);
@@ -1081,6 +1226,8 @@ void SolverBlack::testSimplify()
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));
@@ -1123,12 +1270,22 @@ void SolverBlack::testSimplify()
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()
@@ -1142,6 +1299,8 @@ 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()
@@ -1191,6 +1350,91 @@ 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()
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 42d2dcb25..437b5cf26 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -63,10 +63,10 @@ void SortBlack::testGetDatatype()
{
// 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());
@@ -80,11 +80,11 @@ void SortBlack::testDatatypeSorts()
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();
@@ -121,8 +121,9 @@ void SortBlack::testInstantiate()
// 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);
@@ -131,10 +132,10 @@ void SortBlack::testInstantiate()
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(
@@ -265,8 +266,9 @@ void SortBlack::testGetDatatypeParamSorts()
// 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);
@@ -274,10 +276,10 @@ void SortBlack::testGetDatatypeParamSorts()
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&);
@@ -287,10 +289,10 @@ void SortBlack::testGetDatatypeArity()
{
// 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());
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index d8f022201..a3cbd028f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -197,8 +197,8 @@ void TermBlack::testGetOp()
// 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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback