From: Aina Niemetz Date: Tue, 29 Jan 2019 19:47:04 +0000 (-0800) Subject: New C++ API: Fix checks for mkTerm. (#2820) X-Git-Tag: cvc5-1.0.0~4268 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d4870775e67c7878c32c17f10b1217c14dc5869b;p=cvc5.git New C++ API: Fix checks for mkTerm. (#2820) This required fixing the OpTerm handling for mkTerm functions in the API. --- diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index cd34a5130..7070f6748 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -24,9 +24,8 @@ using namespace CVC4::api; int main() { - Solver slv; - slv.setLogic("QF_BV"); // Set the logic + slv.setLogic("QF_BV"); // Set the logic // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. @@ -64,8 +63,9 @@ int main() slv.assertFormula(assumption); // Introduce a new variable for the new value of x after assignment. - Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0) - Term new_x_ = slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0) + Term new_x_ = + slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; @@ -114,9 +114,9 @@ int main() cout << " Expect invalid. " << endl; cout << " CVC4: " << slv.checkValidAssuming(v) << endl; - // Assert that a is odd + // Assert that a is odd OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term lsb_of_a = slv.mkTerm(extract_op, a); + Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a); cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); cout << "Assert " << a_odd << endl; diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 48560e894..14ddcd383 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -57,18 +57,15 @@ void test(Solver& slv, Sort& consListSort) slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); std::cout << "t2 is " << t2 << std::endl - << "simplify(t2) is " << slv.simplify(t2) - << std::endl << std::endl; + << "simplify(t2) is " << slv.simplify(t2) << std::endl + << std::endl; // You can also iterate over a Datatype to get all its constructors, // and over a DatatypeConstructor to get all its "args" (selectors) - for (Datatype::const_iterator i = consList.begin(); - i != consList.end(); - ++i) + for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i) { std::cout << "ctor: " << *i << std::endl; - for (DatatypeConstructor::const_iterator j = (*i).begin(); - j != (*i).end(); + for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end(); ++j) { std::cout << " + arg: " << *j << std::endl; @@ -91,7 +88,8 @@ void test(Solver& slv, Sort& consListSort) // This example builds a simple parameterized list of sort T, with one // constructor "cons". Sort sort = slv.mkParamSort("T"); - DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name + DatatypeDecl paramConsListSpec("paramlist", + sort); // give the datatype a name DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); DatatypeSelectorDecl paramHead("head", sort); @@ -122,7 +120,7 @@ void test(Solver& slv, Sort& consListSort) Term head_a = slv.mkTerm( APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); - std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() + std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " << paramConsList.getConstructorTerm("cons").getSort() << std::endl @@ -145,7 +143,7 @@ int main() // Second, it is "resolved" to an actual sort, at which point function // symbols are assigned to its constructors, selectors, and testers. - DatatypeDecl consListSpec("list"); // give the datatype a name + DatatypeDecl consListSpec("list"); // give the datatype a name DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", slv.getIntegerSort()); DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); @@ -155,8 +153,7 @@ int main() DatatypeConstructorDecl nil("nil"); consListSpec.addConstructor(nil); - std::cout << "spec is:" << std::endl - << consListSpec << std::endl; + std::cout << "spec is:" << std::endl << consListSpec << std::endl; // Keep in mind that "DatatypeDecl" is the specification class for // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. @@ -168,13 +165,13 @@ int main() test(slv, consListSort); - std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl; + std::cout << std::endl + << ">>> Alternatively, use declareDatatype" << std::endl; std::cout << std::endl; - std::vector ctors = { cons, nil }; + std::vector ctors = {cons, nil}; Sort consListSort2 = slv.declareDatatype("list2", ctors); test(slv, consListSort2); - return 0; } diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index 8d31c1b12..96961458e 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -32,16 +32,16 @@ int main() Term x = slv.mkVar("a", bitvector32); OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); - Term x_31_1 = slv.mkTerm(ext_31_1, x); + Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x); OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0); - Term x_30_0 = slv.mkTerm(ext_30_0, x); + Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x); OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31); - Term x_31_31 = slv.mkTerm(ext_31_31, x); + Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x); OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term x_0_0 = slv.mkTerm(ext_0_0, x); + Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x); Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); cout << " Asserting: " << eq << endl; diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 123613797..ddb17c3a7 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1444,6 +1444,14 @@ DatatypeSelector::DatatypeSelector(const CVC4::DatatypeConstructorArg& stor) DatatypeSelector::~DatatypeSelector() {} +bool DatatypeSelector::isResolved() const { return d_stor->isResolved(); } + +OpTerm DatatypeSelector::getSelectorTerm() const +{ + CVC4_API_CHECK(isResolved()) << "Expected resolved datatype selector."; + return d_stor->getSelector(); +} + std::string DatatypeSelector::toString() const { std::stringstream ss; @@ -1478,10 +1486,10 @@ DatatypeConstructor::~DatatypeConstructor() {} bool DatatypeConstructor::isResolved() const { return d_ctor->isResolved(); } -Term DatatypeConstructor::getConstructorTerm() const +OpTerm DatatypeConstructor::getConstructorTerm() const { CVC4_API_CHECK(isResolved()) << "Expected resolved datatype constructor."; - return Term(d_ctor->getConstructor()); + return OpTerm(d_ctor->getConstructor()); } DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const @@ -1498,7 +1506,7 @@ DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const return (*d_ctor)[name]; } -Term DatatypeConstructor::getSelectorTerm(const std::string& name) const +OpTerm DatatypeConstructor::getSelectorTerm(const std::string& name) const { // CHECK: cons with name exists? // CHECK: is resolved? @@ -1627,7 +1635,7 @@ DatatypeConstructor Datatype::getConstructor(const std::string& name) const return (*d_dtype)[name]; } -Term Datatype::getConstructorTerm(const std::string& name) const +OpTerm Datatype::getConstructorTerm(const std::string& name) const { // CHECK: cons with name exists? // CHECK: is resolved? @@ -2451,40 +2459,41 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const << "Only operator-style terms are created with mkTerm(), " "to create variables and constants see mkVar(), mkBoundVar(), " "and mkConst()."; - if (nchildren) - { - const uint32_t n = - nchildren - (mk == CVC4::kind::metakind::PARAMETERIZED ? 1 : 0); - CVC4_API_KIND_CHECK_EXPECTED(n >= minArity(kind) && n <= maxArity(kind), - kind) - << "Terms with kind " << kindToString(kind) << " must have at least " - << minArity(kind) << " children and at most " << maxArity(kind) - << " children (the one under construction has " << n << ")"; - } + CVC4_API_KIND_CHECK_EXPECTED( + nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind) + << "Terms with kind " << kindToString(kind) << " must have at least " + << minArity(kind) << " children and at most " << maxArity(kind) + << " children (the one under construction has " << nchildren << ")"; } -void Solver::checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const +void Solver::checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const { - const Kind kind = opTerm.getKind(); Assert(isDefinedIntKind(extToIntKind(kind))); const CVC4::Kind int_kind = extToIntKind(kind); - const CVC4::Kind int_op_kind = + const CVC4::Kind int_op_kind = opTerm.d_expr->getKind(); + const CVC4::Kind int_op_to_kind = NodeManager::operatorToKind(opTerm.d_expr->getNode()); - CVC4_API_ARG_CHECK_EXPECTED(int_kind == kind::BUILTIN - || CVC4::kind::metaKindOf(int_op_kind) - == kind::metakind::PARAMETERIZED, - opTerm) + CVC4_API_ARG_CHECK_EXPECTED( + int_kind == int_op_to_kind + || (kind == APPLY_CONSTRUCTOR + && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND) + || (kind == APPLY_SELECTOR + && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND) + || (kind == APPLY_UF && int_op_to_kind == CVC4::Kind::UNDEFINED_KIND), + kind) + << "kind that matches kind associated with given operator term"; + CVC4_API_ARG_CHECK_EXPECTED( + int_op_kind == CVC4::kind::BUILTIN + || CVC4::kind::metaKindOf(int_kind) == kind::metakind::PARAMETERIZED, + opTerm) << "This term constructor is for parameterized kinds only"; - if (nchildren) - { - uint32_t min_arity = ExprManager::minArity(int_op_kind); - uint32_t max_arity = ExprManager::maxArity(int_op_kind); - CVC4_API_KIND_CHECK_EXPECTED( - nchildren >= min_arity && nchildren <= max_arity, kind) - << "Terms with kind " << kindToString(kind) << " must have at least " - << min_arity << " children and at most " << max_arity - << " children (the one under construction has " << nchildren << ")"; - } + uint32_t min_arity = ExprManager::minArity(int_kind); + uint32_t max_arity = ExprManager::maxArity(int_kind); + CVC4_API_KIND_CHECK_EXPECTED(nchildren >= min_arity && nchildren <= max_arity, + kind) + << "Terms with kind " << kindToString(kind) << " must have at least " + << min_arity << " children and at most " << max_arity + << " children (the one under construction has " << nchildren << ")"; } Term Solver::mkTerm(Kind kind) const @@ -2611,13 +2620,30 @@ Term Solver::mkTerm(Kind kind, const std::vector& children) const } } -Term Solver::mkTerm(OpTerm opTerm, Term child) const +Term Solver::mkTerm(Kind kind, OpTerm opTerm) const +{ + try + { + checkMkOpTerm(kind, opTerm, 0); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + } + catch (const CVC4::TypeCheckingException& e) + { + throw CVC4ApiException(e.getMessage()); + } +} + +Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child) const { try { CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term"; - checkMkOpTerm(opTerm, 1); - Term res = d_exprMgr->mkExpr(*opTerm.d_expr, *child.d_expr); + checkMkOpTerm(kind, opTerm, 1); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, *child.d_expr); (void)res.d_expr->getType(true); /* kick off type checking */ return res; } @@ -2627,15 +2653,16 @@ Term Solver::mkTerm(OpTerm opTerm, Term child) const } } -Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const +Term Solver::mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const { try { CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term"; CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term"; - checkMkOpTerm(opTerm, 2); - Term res = - d_exprMgr->mkExpr(*opTerm.d_expr, *child1.d_expr, *child2.d_expr); + checkMkOpTerm(kind, opTerm, 2); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr( + int_kind, *opTerm.d_expr, *child1.d_expr, *child2.d_expr); (void)res.d_expr->getType(true); /* kick off type checking */ return res; } @@ -2645,16 +2672,21 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2) const } } -Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const +Term Solver::mkTerm( + Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const { try { 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"; - checkMkOpTerm(opTerm, 3); - Term res = d_exprMgr->mkExpr( - *opTerm.d_expr, *child1.d_expr, *child2.d_expr, *child3.d_expr); + checkMkOpTerm(kind, opTerm, 3); + const CVC4::Kind int_kind = extToIntKind(kind); + Term res = d_exprMgr->mkExpr(int_kind, + *opTerm.d_expr, + *child1.d_expr, + *child2.d_expr, + *child3.d_expr); (void)res.d_expr->getType(true); /* kick off type checking */ return res; } @@ -2664,7 +2696,9 @@ Term Solver::mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const } } -Term Solver::mkTerm(OpTerm opTerm, const std::vector& children) const +Term Solver::mkTerm(Kind kind, + OpTerm opTerm, + const std::vector& children) const { try { @@ -2674,9 +2708,10 @@ Term Solver::mkTerm(OpTerm opTerm, const std::vector& children) const !children[i].isNull(), "parameter term", children[i], i) << "non-null term"; } - checkMkOpTerm(opTerm, children.size()); + checkMkOpTerm(kind, opTerm, children.size()); + const CVC4::Kind int_kind = extToIntKind(kind); std::vector echildren = termVectorToExprs(children); - Term res = d_exprMgr->mkExpr(*opTerm.d_expr, echildren); + Term res = d_exprMgr->mkExpr(int_kind, *opTerm.d_expr, echildren); (void)res.d_expr->getType(true); /* kick off type checking */ return res; } @@ -2691,16 +2726,26 @@ Term Solver::mkTuple(const std::vector& sorts, { CVC4_API_CHECK(sorts.size() == terms.size()) << "Expected the same number of sorts and elements"; - std::vector args; - for (size_t i = 0, size = sorts.size(); i < size; i++) + try { - args.push_back(ensureTermSort(terms[i], sorts[i])); - } + std::vector args; + for (size_t i = 0, size = sorts.size(); i < size; i++) + { + args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_expr); + } - Sort s = mkTupleSort(sorts); - Datatype dt = s.getDatatype(); - args.insert(args.begin(), dt[0].getConstructorTerm()); - return mkTerm(APPLY_CONSTRUCTOR, args); + Sort s = mkTupleSort(sorts); + Datatype dt = s.getDatatype(); + Term res = d_exprMgr->mkExpr(extToIntKind(APPLY_CONSTRUCTOR), + *dt[0].getConstructorTerm().d_expr, + args); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + } + catch (const CVC4::TypeCheckingException& e) + { + throw CVC4ApiException(e.getMessage()); + } } std::vector Solver::termVectorToExprs( @@ -3458,28 +3503,32 @@ void Solver::setOption(const std::string& option, } } -Term Solver::ensureTermSort(const Term& t, const Sort& s) const +Term Solver::ensureTermSort(const Term& term, const Sort& sort) const { - CVC4_API_CHECK(t.getSort() == s || (t.getSort().isInteger() && s.isReal())) + CVC4_API_CHECK(term.getSort() == sort + || (term.getSort().isInteger() && sort.isReal())) << "Expected conversion from Int to Real"; - if (t.getSort() == s) + Sort t = term.getSort(); + if (term.getSort() == sort) { - return t; + return term; } // Integers are reals, too - Assert(t.getSort().isReal()); - Term res = t; - if (t.getSort().isInteger()) + Assert(t.isReal()); + Term res = term; + if (t.isInteger()) { // Must cast to Real to ensure correct type is passed to parametric type // constructors. We do this cast using division with 1. This has the // advantage wrt using TO_REAL since (constant) division is always included // in the theory. - res = mkTerm(DIVISION, *t.d_expr, mkReal(1)); + res = Term(d_exprMgr->mkExpr(extToIntKind(DIVISION), + *res.d_expr, + d_exprMgr->mkConst(CVC4::Rational(1)))); } - Assert(res.getSort() == s); + Assert(res.getSort() == sort); return res; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index a06f2e415..b8da070fc 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1099,6 +1099,17 @@ class CVC4_PUBLIC DatatypeSelector */ ~DatatypeSelector(); + /** + * @return true if this datatype selector has been resolved. + */ + bool isResolved() const; + + /** + * Get the selector operator of this datatype selector. + * @return the selector operator + */ + OpTerm getSelectorTerm() const; + /** * @return a string representation of this datatype selector */ @@ -1154,7 +1165,7 @@ class CVC4_PUBLIC DatatypeConstructor * Get the constructor operator of this datatype constructor. * @return the constructor operator */ - Term getConstructorTerm() const; + OpTerm getConstructorTerm() const; /** * Get the datatype selector with the given name. @@ -1173,7 +1184,7 @@ class CVC4_PUBLIC DatatypeConstructor * @param name the name of the datatype selector * @return a term representing the datatype selector with the given name */ - Term getSelectorTerm(const std::string& name) const; + OpTerm getSelectorTerm(const std::string& name) const; /** * @return a string representation of this datatype constructor @@ -1320,7 +1331,7 @@ class CVC4_PUBLIC Datatype * similarly-named constructors, the * first is returned. */ - Term getConstructorTerm(const std::string& name) const; + OpTerm getConstructorTerm(const std::string& name) const; /** Get the number of constructors for this Datatype. */ size_t getNumConstructors() const; @@ -1725,43 +1736,59 @@ class CVC4_PUBLIC Solver Term mkTerm(Kind kind, const std::vector& children) const; /** - * Create unary term from a given operator term. + * Create nullary term of given kind from a given operator term. + * Create operator terms with mkOpTerm(). + * @param kind the kind of the term + * @param the operator term + * @return the Term + */ + Term mkTerm(Kind kind, OpTerm opTerm) const; + + /** + * Create unary term of given kind from a given operator term. * Create operator terms with mkOpTerm(). + * @param kind the kind of the term * @param the operator term * @child the child of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, Term child) const; + Term mkTerm(Kind kind, OpTerm opTerm, Term child) const; /** - * Create binary term from a given operator term. + * Create binary term of given kind from a given operator term. + * @param kind the kind of the term * Create operator terms with mkOpTerm(). * @param the operator term * @child1 the first child of the term * @child2 the second child of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, Term child1, Term child2) const; + Term mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const; /** - * Create ternary term from a given operator term. + * Create ternary term of given kind from a given operator term. * Create operator terms with mkOpTerm(). + * @param kind the kind of the term * @param the operator term * @child1 the first child of the term * @child2 the second child of the term * @child3 the third child of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const; + Term mkTerm( + Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) const; /** - * Create n-ary term from a given operator term. + * Create n-ary term of given kind from a given operator term. * Create operator terms with mkOpTerm(). + * @param kind the kind of the term * @param the operator term * @children the children of the term * @return the Term */ - Term mkTerm(OpTerm opTerm, const std::vector& children) const; + Term mkTerm(Kind kind, + OpTerm opTerm, + const std::vector& children) const; /** * Create a tuple term. Terms are automatically converted if sorts are @@ -2485,7 +2512,7 @@ class CVC4_PUBLIC Solver /* Helper to convert a vector of sorts to internal types. */ std::vector termVectorToExprs(const std::vector& vector) const; /* Helper to check for API misuse in mkTerm functions. */ - void checkMkOpTerm(OpTerm opTerm, uint32_t nchildren) const; + void checkMkOpTerm(Kind kind, OpTerm opTerm, uint32_t nchildren) const; /* Helper to check for API misuse in mkOpTerm functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; /* Helper for mk-functions that call d_exprMgr->mkConst(). */ diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index a7f6926bb..4e69ddfe1 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1649,30 +1649,32 @@ enum CVC4_PUBLIC Kind : int32_t /** * Constructor application. * Paramters: n > 0 - * -[1]: Constructor + * -[1]: Constructor (operator term) * -[2]..[n]: Parameters to the constructor * Create with: - * mkTerm(Kind kind) - * mkTerm(Kind kind, Term child) - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, Term child1, Term child2, Term child3) - * mkTerm(Kind kind, const std::vector& children) + * mkTerm(Kind kind, OpTerm opTerm) + * mkTerm(Kind kind, OpTerm opTerm, Term child) + * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) + * mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, OpTerm opTerm, const std::vector& children) */ - APPLY_SELECTOR, + APPLY_CONSTRUCTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Datatype term (undefined if mis-applied) + * -[1]: Selector (operator term) + * -[2]: Datatype term (undefined if mis-applied) * Create with: - * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, OpTerm opTerm, Term child) */ - APPLY_CONSTRUCTOR, + APPLY_SELECTOR, /** * Datatype selector application. * Parameters: 1 - * -[1]: Datatype term (defined rigidly if mis-applied) + * -[1]: Selector (operator term) + * -[2]: Datatype term (defined rigidly if mis-applied) * Create with: - * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, OpTerm opTerm, Term child) */ APPLY_SELECTOR_TOTAL, /** diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index e6b89b498..d0d36508f 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -301,21 +301,30 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, } } -Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { +Expr ExprManager::mkExpr(Kind kind, const std::vector& children) +{ + const size_t nchildren = children.size(); const kind::MetaKind mk = kind::metaKindOf(kind); - const unsigned n = children.size() - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); PrettyCheckArgument( - mk == kind::metakind::PARAMETERIZED || - mk == kind::metakind::OPERATOR, kind, + mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR, + kind, "Only operator-style expressions are made with mkExpr(); " "to make variables and constants, see mkVar(), mkBoundVar(), " "and mkConst()."); PrettyCheckArgument( - n >= minArity(kind) && n <= maxArity(kind), kind, - "Exprs with kind %s must have at least %u children and " - "at most %u children (the one under construction has %u)", - kind::kindToString(kind).c_str(), - minArity(kind), maxArity(kind), n); + mk != kind::metakind::PARAMETERIZED || nchildren > 0, + kind, + "Terms with kind %s must have an operator expression as first argument", + kind::kindToString(kind).c_str()); + const size_t n = nchildren - (mk == kind::metakind::PARAMETERIZED ? 1 : 0); + PrettyCheckArgument(n >= minArity(kind) && n <= maxArity(kind), + kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), + maxArity(kind), + n); NodeManagerScope nms(d_nodeManager); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index d2226f278..fcc68d981 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -69,6 +69,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkSepNil(); void testMkString(); void testMkTerm(); + void testMkTermFromOpTerm(); void testMkTrue(); void testMkTuple(); void testMkUninterpretedConst(); @@ -537,9 +538,7 @@ void SolverBlack::testMkTerm() std::vector v3 = {a, d_solver->mkTrue()}; std::vector v4 = {d_solver->mkReal(1), d_solver->mkReal(2)}; std::vector v5 = {d_solver->mkReal(1), Term()}; - OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1); - OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); - OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); + std::vector v6 = {}; // mkTerm(Kind kind) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI)); @@ -584,33 +583,112 @@ void SolverBlack::testMkTerm() TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1)); TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v2), CVC4ApiException&); TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&); +} - // mkTerm(OpTerm opTerm, Term child) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); +void SolverBlack::testMkTermFromOpTerm() +{ + Sort bv32 = d_solver->mkBitVectorSort(32); + Term a = d_solver->mkVar("a", bv32); + Term b = d_solver->mkVar("b", bv32); + std::vector v1 = {d_solver->mkReal(1), d_solver->mkReal(2)}; + std::vector v2 = {d_solver->mkReal(1), Term()}; + std::vector v3 = {}; + // simple operator terms + OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1); + OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); + OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); + // list datatype + Sort sort = d_solver->mkParamSort("T"); + DatatypeDecl listDecl("paramlist", sort); + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil("nil"); + DatatypeSelectorDecl head("head", sort); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + listDecl.addConstructor(cons); + listDecl.addConstructor(nil); + Sort listSort = d_solver->mkDatatypeSort(listDecl); + Sort intListSort = + listSort.instantiate(std::vector{d_solver->getIntegerSort()}); + Term c = d_solver->declareFun("c", intListSort); + Datatype list = listSort.getDatatype(); + // list datatype constructor and selector operator terms + OpTerm consTerm1 = list.getConstructorTerm("cons"); + OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm(); + OpTerm nilTerm1 = list.getConstructorTerm("nil"); + OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm(); + OpTerm headTerm1 = list["cons"].getSelectorTerm("head"); + OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); + OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail"); + OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm(); + + // mkTerm(Kind kind, OpTerm opTerm) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1), + CVC4ApiException&); - // mkTerm(OpTerm opTerm, Term child1, Term child2) const + // mkTerm(Kind kind, OpTerm opTerm, Term child) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a)); TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), + d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c)); + TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()), CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), + CVC4ApiException&); - // mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const + // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( - opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); + CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); + 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(BITVECTOR_EXTRACT, opterm1, a, b), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)), + CVC4ApiException&); + + // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) + // const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, + opterm3, + d_solver->mkReal(1), + d_solver->mkReal(1), + d_solver->mkReal(2))); + TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a), + CVC4ApiException&); TS_ASSERT_THROWS( d_solver->mkTerm( - opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), + CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), CVC4ApiException&); // mkTerm(OpTerm opTerm, const std::vector& children) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v4)); - TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v5), CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1)); + TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&); } void SolverBlack::testMkTrue()