"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<Expr>::const_iterator it = children.begin() ;
std::vector<Expr>::const_iterator end = children.end() ;
/* The new top-level children and the children of each sub node */
- std::vector<Node> newChildren;
+ std::vector<Expr> newChildren;
std::vector<Node> subChildren;
while( it != end && numChildren > max ) {
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<Expr>& 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<Expr>& 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) {
*/
Expr mkAssociative(Kind kind, const std::vector<Expr>& 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<Expr>& 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<Expr>& children);
+
/**
* Determine whether Exprs of a particular Kind have operators.
* @returns true if Exprs of Kind k have operators.
return getExprManager()->mkFunctionType(sorts, range);
}
-Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex)
+Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& 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]);
}
/** 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<Expr>& args, unsigned startIndex = 0);
+ Expr mkHoApply(Expr expr, std::vector<Expr>& args);
/**
* Add an operator to the current legal set.
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 ) &&
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<FunctionType>(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);
}
}
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 \
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff