summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/expr_manager_template.cpp57
-rw-r--r--src/expr/expr_manager_template.h13
-rw-r--r--src/parser/parser.cpp4
-rw-r--r--src/parser/parser.h8
-rw-r--r--src/parser/smt2/Smt2.g65
5 files changed, 96 insertions, 51 deletions
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<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 ) {
@@ -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<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) {
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
@@ -301,6 +301,19 @@ public:
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.
*/
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<Type>& sorts, Type range)
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]);
}
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<Expr>& args, unsigned startIndex = 0);
+ Expr mkHoApply(Expr expr, std::vector<Expr>& 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<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);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback