From 11110b87cb70d9c4a6dc486319adbb7dfa59fedb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 27 Aug 2018 12:26:14 -0500 Subject: [PATCH] Make division chainable in the smt2 parser (#2367) --- src/expr/expr_manager_template.cpp | 57 +++++++++------- src/expr/expr_manager_template.h | 13 ++++ src/parser/parser.cpp | 4 +- src/parser/parser.h | 8 +-- src/parser/smt2/Smt2.g | 65 ++++++++++++------- test/regress/Makefile.tests | 1 + .../regress/regress0/arith/div-chainable.smt2 | 12 ++++ 7 files changed, 109 insertions(+), 51 deletions(-) create mode 100644 test/regress/regress0/arith/div-chainable.smt2 diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5d5c1ef68..e6b89b498 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -928,21 +928,21 @@ Expr ExprManager::mkAssociative(Kind kind, "Illegal kind in mkAssociative: %s", kind::kindToString(kind).c_str()); - NodeManagerScope nms(d_nodeManager); const unsigned int max = maxArity(kind); - const unsigned int min = minArity(kind); unsigned int numChildren = children.size(); /* If the number of children is within bounds, then there's nothing to do. */ if( numChildren <= max ) { return mkExpr(kind,children); } + NodeManagerScope nms(d_nodeManager); + const unsigned int min = minArity(kind); std::vector::const_iterator it = children.begin() ; std::vector::const_iterator end = children.end() ; /* The new top-level children and the children of each sub node */ - std::vector newChildren; + std::vector newChildren; std::vector subChildren; while( it != end && numChildren > max ) { @@ -953,39 +953,50 @@ Expr ExprManager::mkAssociative(Kind kind, subChildren.push_back(it->getNode()); } Node subNode = d_nodeManager->mkNode(kind,subChildren); - newChildren.push_back(subNode); + newChildren.push_back(subNode.toExpr()); subChildren.clear(); } - /* If there's children left, "top off" the Expr. */ + // add the leftover children if(numChildren > 0) { - /* If the leftovers are too few, just copy them into newChildren; - * otherwise make a new sub-node */ - if(numChildren < min) { - for(; it != end; ++it) { - newChildren.push_back(it->getNode()); - } - } else { - for(; it != end; ++it) { - subChildren.push_back(it->getNode()); - } - Node subNode = d_nodeManager->mkNode(kind, subChildren); - newChildren.push_back(subNode); + for (; it != end; ++it) + { + newChildren.push_back(*it); } } - /* It's inconceivable we could have enough children for this to fail - * (more than 2^32, in most cases?). */ - AlwaysAssert( newChildren.size() <= max, - "Too many new children in mkAssociative" ); - /* It would be really weird if this happened (it would require * min > 2, for one thing), but let's make sure. */ AlwaysAssert( newChildren.size() >= min, "Too few new children in mkAssociative" ); - return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) ); + // recurse + return mkAssociative(kind, newChildren); +} + +Expr ExprManager::mkLeftAssociative(Kind kind, + const std::vector& children) +{ + NodeManagerScope nms(d_nodeManager); + Node n = children[0]; + for (unsigned i = 1, size = children.size(); i < size; i++) + { + n = d_nodeManager->mkNode(kind, n, children[i].getNode()); + } + return n.toExpr(); +} + +Expr ExprManager::mkRightAssociative(Kind kind, + const std::vector& children) +{ + NodeManagerScope nms(d_nodeManager); + Node n = children[children.size() - 1]; + for (unsigned i = children.size() - 1; i > 0;) + { + n = d_nodeManager->mkNode(kind, children[--i].getNode(), n); + } + return n.toExpr(); } unsigned ExprManager::minArity(Kind kind) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index dce1a57a5..4e0ab700c 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -300,6 +300,19 @@ public: */ Expr mkAssociative(Kind kind, const std::vector& children); + /** + * Create an Expr by applying an binary left-associative operator to the + * children. For example, mkLeftAssociative( f, { a, b, c } ) returns + * f( f( a, b ), c ). + */ + Expr mkLeftAssociative(Kind kind, const std::vector& children); + /** + * Create an Expr by applying an binary right-associative operator to the + * children. For example, mkRightAssociative( f, { a, b, c } ) returns + * f( a, f( b, c ) ). + */ + Expr mkRightAssociative(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 182abb89b..8ddefb2f4 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -505,9 +505,9 @@ Type Parser::mkFlatFunctionType(std::vector& sorts, Type range) return getExprManager()->mkFunctionType(sorts, range); } -Expr Parser::mkHoApply(Expr expr, std::vector& args, unsigned startIndex) +Expr Parser::mkHoApply(Expr expr, std::vector& args) { - for (unsigned i = startIndex; i < args.size(); i++) + for (unsigned i = 0; i < args.size(); i++) { expr = getExprManager()->mkExpr(HO_APPLY, expr, args[i]); } diff --git a/src/parser/parser.h b/src/parser/parser.h index b0519691c..f22fc3789 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -634,17 +634,17 @@ public: /** make higher-order apply * * This returns the left-associative curried application of (function) expr to - * the arguments in args, starting at index startIndex. + * the arguments in args. * * For example, mkHoApply( f, { a, b }, 0 ) returns * (HO_APPLY (HO_APPLY f a) b) * * If args is non-empty, the expected type of expr is (-> T0 ... Tn T), where - * args[i-startIndex].getType() = Ti - * for each i where startIndex <= i < args.size(). If expr is not of this + * args[i].getType() = Ti + * for each i where 0 <= i < args.size(). If expr is not of this * type, the expression returned by this method will not be well typed. */ - Expr mkHoApply(Expr expr, std::vector& args, unsigned startIndex = 0); + Expr mkHoApply(Expr expr, std::vector& args); /** * Add an operator to the current legal set. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5e068948f..40166a641 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1807,19 +1807,16 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] expr = EXPR_MANAGER->mkAssociative(kind, args); } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) { expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); - } else if( ( kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS ) && - args.size() > 2 ) { + } + else if ((kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS + || kind == CVC4::kind::DIVISION) + && args.size() > 2) + { /* left-associative, but CVC4 internally only supports 2 args */ - expr = args[0]; - for(size_t i = 1; i < args.size(); ++i) { - expr = MK_EXPR(kind, expr, args[i]); - } + expr = EXPR_MANAGER->mkLeftAssociative(kind,args); } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) { /* right-associative, but CVC4 internally only supports 2 args */ - expr = args[args.size() - 1]; - for(size_t i = args.size() - 1; i > 0;) { - expr = MK_EXPR(kind, args[--i], expr); - } + expr = EXPR_MANAGER->mkRightAssociative(kind,args); } else if( ( kind == CVC4::kind::EQUAL || kind == CVC4::kind::LT || kind == CVC4::kind::GT || kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) && @@ -1959,19 +1956,43 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types."); } } - if(isBuiltinOperator) { - PARSER_STATE->checkOperator(kind, args.size()); + Kind lassocKind = CVC4::kind::UNDEFINED_KIND; + if (args.size() >= 2) + { + if (kind == CVC4::kind::INTS_DIVISION) + { + // Builtin operators that are not tokenized, are left associative, + // but not internally variadic must set this. + lassocKind = kind; + } + else + { + // may be partially applied function, in this case we use HO_APPLY + Type argt = args[0].getType(); + if (argt.isFunction()) + { + unsigned arity = static_cast(argt).getArity(); + if (args.size() - 1 < arity) + { + Debug("parser") << "Partial application of " << args[0]; + Debug("parser") << " : #argTypes = " << arity; + Debug("parser") << ", #args = " << args.size() - 1 << std::endl; + // must curry the partial application + lassocKind = CVC4::kind::HO_APPLY; + } + } + } } - // may be partially applied function, in this case we should use HO_APPLY - if( args.size()>=2 && args[0].getType().isFunction() && - (args.size()-1)<((FunctionType)args[0].getType()).getArity() ){ - Debug("parser") << "Partial application of " << args[0]; - Debug("parser") << " : #argTypes = " << ((FunctionType)args[0].getType()).getArity(); - Debug("parser") << ", #args = " << args.size()-1 << std::endl; - // must curry the application - expr = args[0]; - expr = PARSER_STATE->mkHoApply( expr, args, 1 ); - }else{ + if (lassocKind != CVC4::kind::UNDEFINED_KIND) + { + expr = EXPR_MANAGER->mkLeftAssociative(lassocKind, args); + } + else + { + if (isBuiltinOperator) + { + PARSER_STATE->checkOperator(kind, args.size()); + } expr = MK_EXPR(kind, args); } } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index f707da219..17a302192 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -15,6 +15,7 @@ REG0_TESTS = \ regress0/arith/div.04.smt2 \ regress0/arith/div.05.smt2 \ regress0/arith/div.07.smt2 \ + regress0/arith/div-chainable.smt2 \ regress0/arith/fuzz_3-eq.smt \ regress0/arith/integers/arith-int-042.cvc \ regress0/arith/integers/arith-int-042.min.cvc \ diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2 new file mode 100644 index 000000000..9ddc80e98 --- /dev/null +++ b/test/regress/regress0/arith/div-chainable.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --rewrite-divk +; EXPECT: sat +(set-logic QF_LIA) +(set-info :status sat) + +(declare-fun x () Int) + +(assert (= (div 4 2 1) 2)) + +(assert (= (div x 2 1) 2)) + +(check-sat) -- 2.30.2