diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-25 20:52:10 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-25 20:52:10 -0600 |
commit | 808bb1bd855799535a1b690865dc873793a37f7f (patch) | |
tree | 178d9bb00cccf12c11c6f7284dc66e0d6c8827ec /src/api | |
parent | 9301607b58a3b74dcea73c500c6391d6a51093f8 (diff) |
Embed mkAssociative utilities within the API. (#3801)
Towards parser/API migration.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 100 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 10 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 84 |
3 files changed, 125 insertions, 69 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 41a374283..622d48ac9 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2390,6 +2390,70 @@ Term Solver::mkTermFromKind(Kind kind) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::mkTermInternal(Kind kind, const std::vector<Term>& children) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + 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) + << "non-null term"; + } + + std::vector<Expr> echildren = termVectorToExprs(children); + CVC4::Kind k = extToIntKind(kind); + Assert(isDefinedIntKind(k)); + + Term res; + if (echildren.size() > 2) + { + if (kind == INTS_DIVISION || kind == XOR || kind == MINUS + || kind == DIVISION || kind == BITVECTOR_XNOR || kind == HO_APPLY) + { + // left-associative, but CVC4 internally only supports 2 args + res = d_exprMgr->mkLeftAssociative(k, echildren); + } + else if (kind == IMPLIES) + { + // right-associative, but CVC4 internally only supports 2 args + res = d_exprMgr->mkRightAssociative(k, echildren); + } + else if (kind == EQUAL || kind == LT || kind == GT || kind == LEQ + || kind == GEQ) + { + // "chainable", but CVC4 internally only supports 2 args + res = d_exprMgr->mkChain(k, echildren); + } + else if (kind::isAssociative(k)) + { + // mkAssociative has special treatment for associative operators with lots + // of children + res = d_exprMgr->mkAssociative(k, echildren); + } + else + { + // default case, must check kind + checkMkTerm(kind, children.size()); + res = d_exprMgr->mkExpr(k, echildren); + } + } + else if (kind::isAssociative(k)) + { + // associative case, same as above + res = d_exprMgr->mkAssociative(k, echildren); + } + else + { + // default case, same as above + checkMkTerm(kind, children.size()); + res = d_exprMgr->mkExpr(k, echildren); + } + + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + CVC4_API_SOLVER_TRY_CATCH_END; +} + /* Helpers for converting vectors. */ /* .......................................................................... */ @@ -3142,43 +3206,13 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) 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_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term"; - checkMkTerm(kind, 3); - - std::vector<Expr> echildren{*child1.d_expr, *child2.d_expr, *child3.d_expr}; - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) - : d_exprMgr->mkExpr(k, echildren); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - - CVC4_API_SOLVER_TRY_CATCH_END; + // need to use internal term call to check e.g. associative construction + return mkTermInternal(kind, std::vector<Term>{child1, child2, child3}); } Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const { - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - 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) - << "non-null term"; - } - checkMkTerm(kind, children.size()); - - std::vector<Expr> echildren = termVectorToExprs(children); - CVC4::Kind k = extToIntKind(kind); - Assert(isDefinedIntKind(k)); - Term res = kind::isAssociative(k) ? d_exprMgr->mkAssociative(k, echildren) - : d_exprMgr->mkExpr(k, echildren); - (void)res.d_expr->getType(true); /* kick off type checking */ - return res; - - CVC4_API_SOLVER_TRY_CATCH_END; + return mkTermInternal(kind, children); } Term Solver::mkTerm(Op op) const diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 103637a7d..3317348fe 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2862,6 +2862,16 @@ class CVC4_PUBLIC Solver */ Term ensureRealSort(Term expr) const; + /** + * Create n-ary term of given kind. This handles the cases of left/right + * associative operators, chainable operators, and cases when the number of + * children exceeds the maximum arity for the kind. + * @param kind the kind of the term + * @param children the children of the term + * @return the Term + */ + Term mkTermInternal(Kind kind, const std::vector<Term>& children) const; + /* The expression manager of this solver. */ std::unique_ptr<ExprManager> d_exprMgr; /* The SMT engine of this solver. */ diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 27c28cec6..591ff9b1e 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -78,18 +78,19 @@ enum CVC4_PUBLIC Kind : int32_t BUILTIN, #endif /** - * Equality. - * Parameters: 2 - * -[1]..[2]: Terms with same sort + * Equality, chainable. + * Parameters: n > 1 + * -[1]..[n]: Terms with same sorts * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ EQUAL, /** * Disequality. * Parameters: n > 1 - * -[1]..[n]: Terms with same sort + * -[1]..[n]: Terms with same sorts * Create with: * mkTerm(Kind kind, Term child1, Term child2) * mkTerm(Kind kind, Term child1, Term child2, Term child3) @@ -173,10 +174,11 @@ enum CVC4_PUBLIC Kind : int32_t AND, /** * Logical implication. - * Parameters: 2 - * -[1]..[2]: Boolean Terms, [1] implies [2] + * Parameters: n > 1 + * -[1]..[n]: Boolean Terms, right associative * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ IMPLIES, @@ -189,11 +191,12 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& children) */ OR, - /* Logical exclusive or. - * Parameters: 2 - * -[1]..[2]: Boolean Terms, [1] xor [2] + /* Logical exclusive or, left associative. + * Parameters: n > 1 + * -[1]..[n]: Boolean Terms, [1] xor ... xor [n] * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ XOR, @@ -255,12 +258,14 @@ enum CVC4_PUBLIC Kind : int32_t PARTIAL_APPLY_UF, #endif /** - * Higher-order applicative encoding of function application. - * Parameters: 2 + * Higher-order applicative encoding of function application, left + * associative. + * Parameters: n > 1 * -[1]: Function to apply - * -[2]: Argument of the function + * -[2] ... [n]: Arguments of the function * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ HO_APPLY, @@ -292,11 +297,12 @@ enum CVC4_PUBLIC Kind : int32_t NONLINEAR_MULT, #endif /** - * Arithmetic subtraction. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real (sorts must match) + * Arithmetic subtraction, left associative. + * Parameters: n + * -[1]..[n]: Terms of sort Integer, Real (sorts must match) * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ MINUS, @@ -309,20 +315,22 @@ enum CVC4_PUBLIC Kind : int32_t */ UMINUS, /** - * Real division, division by 0 undefined - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real + * Real division, division by 0 undefined, left associative. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer, Real * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ DIVISION, /** - * Integer division, division by 0 undefined. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer + * Integer division, division by 0 undefined, left associative. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ INTS_DIVISION, @@ -504,38 +512,41 @@ enum CVC4_PUBLIC Kind : int32_t */ CONST_RATIONAL, /** - * Less than. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real; [1] < [2] + * Less than, chainable. + * Parameters: n + * -[1]..[n]: Terms of sort Integer, Real; [1] < ... < [n] * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ LT, /** - * Less than or equal. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real; [1] <= [2] + * Less than or equal, chainable. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer, Real; [1] <= ... <= [n] * Create with: * mkTerm(Kind kind, Term child1, Term child2) * mkTerm(Kind kind, const std::vector<Term>& children) */ LEQ, /** - * Greater than. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real, [1] > [2] + * Greater than, chainable. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer, Real, [1] > ... > [n] * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ GT, /** - * Greater than or equal. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real; [1] >= [2] + * Greater than or equal, chainable. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer, Real; [1] >= ... >= [n] * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ GEQ, @@ -649,9 +660,9 @@ enum CVC4_PUBLIC Kind : int32_t */ BITVECTOR_NOR, /** - * Bit-wise xnor. - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Bit-wise xnor, left associative. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort (sorts must match) * Create with: * mkTerm(Kind kind, Term child1, Term child2) * mkTerm(Kind kind, const std::vector<Term>& children) @@ -663,6 +674,7 @@ enum CVC4_PUBLIC Kind : int32_t * -[1]..[2]: Terms of bit-vector sort (sorts must match) * Create with: * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) * mkTerm(Kind kind, const std::vector<Term>& children) */ BITVECTOR_COMP, |