From 808bb1bd855799535a1b690865dc873793a37f7f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 25 Feb 2020 20:52:10 -0600 Subject: [PATCH] Embed mkAssociative utilities within the API. (#3801) Towards parser/API migration. --- src/api/cvc4cpp.cpp | 100 +++++++++++++++++++---------- src/api/cvc4cpp.h | 10 +++ src/api/cvc4cppkind.h | 84 +++++++++++++----------- src/expr/expr_manager_template.cpp | 16 +++++ src/expr/expr_manager_template.h | 10 +++ src/parser/parser.cpp | 16 ----- src/parser/parser.h | 10 --- src/parser/smt2/smt2.cpp | 4 +- src/parser/tptp/tptp.cpp | 4 +- 9 files changed, 153 insertions(+), 101 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& 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 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 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{child1, child2, child3}); } Term Solver::mkTerm(Kind kind, const std::vector& 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 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& children) const; + /* The expression manager of this solver. */ std::unique_ptr 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& 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& children) */ IMPLIES, @@ -189,11 +191,12 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& 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& 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& 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& 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& 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& 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& 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& 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& 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& 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& 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& children) */ BITVECTOR_COMP, diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 8bf8d9e54..76992e1ba 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1013,6 +1013,22 @@ Expr ExprManager::mkRightAssociative(Kind kind, return n.toExpr(); } +Expr ExprManager::mkChain(Kind kind, const std::vector& children) +{ + if (children.size() == 2) + { + // if this is the case exactly 1 pair will be generated so the + // AND is not required + return mkExpr(kind, children[0], children[1]); + } + std::vector cchildren; + for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++) + { + cchildren.push_back(mkExpr(kind, children[i], children[i + 1])); + } + return mkExpr(kind::AND, cchildren); +} + unsigned ExprManager::minArity(Kind kind) { return metakind::getLowerBoundForKind(kind); } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index c61c7e012..0fd5bb4fa 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -306,6 +306,16 @@ private: */ Expr mkRightAssociative(Kind kind, const std::vector& children); + /** make chain + * + * Given a kind k and arguments t_1, ..., t_n, this returns the + * conjunction of: + * (k t_1 t_2) .... (k t_{n-1} t_n) + * It is expected that k is a kind denoting a predicate, and args is a list + * of terms of size >= 2 such that the terms above are well-typed. + */ + Expr mkChain(Kind kind, const std::vector& children); + /** * Determine whether Exprs of a particular Kind have operators. * @returns true if Exprs of Kind k have operators. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 447fb5d76..663be7f1f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -515,22 +515,6 @@ Expr Parser::mkHoApply(Expr expr, std::vector& args) return expr; } -api::Term Parser::mkChain(api::Kind k, const std::vector& args) -{ - if (args.size() == 2) - { - // if this is the case exactly 1 pair will be generated so the - // AND is not required - return d_solver->mkTerm(k, args[0], args[1]); - } - std::vector children; - for (size_t i = 0, nargsmo = args.size() - 1; i < nargsmo; i++) - { - children.push_back(d_solver->mkTerm(k, args[i], args[i + 1])); - } - return d_solver->mkTerm(api::AND, children); -} - bool Parser::isDeclared(const std::string& name, SymbolType type) { switch (type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index 0c1f3822b..8447eb4dc 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -678,16 +678,6 @@ public: */ Expr mkHoApply(Expr expr, std::vector& args); - /** make chain - * - * Given a kind k and argument terms t_1, ..., t_n, this returns the - * conjunction of: - * (k t_1 t_2) .... (k t_{n-1} t_n) - * It is expected that k is a kind denoting a predicate, and args is a list - * of terms of size >= 2 such that the terms above are well-typed. - */ - api::Term mkChain(api::Kind k, const std::vector& args); - /** * Add an operator to the current legal set. * diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7b7e9dd82..88d8b527b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1897,9 +1897,7 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) || kind == kind::LEQ || kind == kind::GEQ) { /* "chainable", but CVC4 internally only supports 2 args */ - api::Term ret = - mkChain(intToExtKind(kind), api::exprVectorToTerms(args)); - return ret.getExpr(); + return em->mkChain(kind, args); } } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index bf699ae3c..2b1edf15b 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -326,9 +326,7 @@ Expr Tptp::applyParseOp(ParseOp& p, std::vector& args) || kind == kind::LEQ || kind == kind::GEQ) { /* "chainable", but CVC4 internally only supports 2 args */ - api::Term ret = - mkChain(intToExtKind(kind), api::exprVectorToTerms(args)); - return ret.getExpr(); + return em->mkChain(kind, args); } } -- 2.30.2