Fixing failing test in r521

Adding general support for associative operators in SMT v1 and v2

3 files changed, 11 insertions, 1 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 59dbf77e5..8cfd50f08 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -252,6 +252,8 @@ Expr ExprManager::mkVar(const Type& type) {
 
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
+  Assert( metakind::isAssociative(kind), "Illegal kind in mkAssociative" );
+
   NodeManagerScope nms(d_nodeManager);
   const unsigned int max = maxArity(kind);
   const unsigned int min = minArity(kind);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index cfe41316c..9c609d0d4 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -60,6 +60,7 @@ namespace CVC4 {
 @parser::postinclude {
 #include "expr/expr.h"
 #include "expr/kind.h"
+#include "expr/metakind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -187,7 +188,9 @@ annotatedFormula[CVC4::Expr& expr]
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
-      } else if( (kind == CVC4::kind::AND || kind == CVC4::kind::OR) ) {
+      } else if( CVC4::kind::metakind::isAssociative(kind) && 
+                 args.size() > EXPR_MANAGER->maxArity(kind) ) {
+    	/* Special treatment for associative operators with lots of children */
         expr = EXPR_MANAGER->mkAssociative(kind,args);
       } else {
         PARSER_STATE->checkArity(kind, args.size());
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 105976628..b8557665e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -74,6 +74,7 @@ namespace CVC4 {
 @parser::postinclude {
 #include "expr/expr.h"
 #include "expr/kind.h"
+#include "expr/metakind.h"
 #include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -209,6 +210,10 @@ term[CVC4::Expr& expr]
         /* Unary AND/OR can be replaced with the argument.
 	       It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
+	 } else if( CVC4::kind::metakind::isAssociative(kind) && 
+                 args.size() > EXPR_MANAGER->maxArity(kind) ) {
+    	/* Special treatment for associative operators with lots of children */
+        expr = EXPR_MANAGER->mkAssociative(kind,args);
       } else {
         PARSER_STATE->checkOperator(kind, args.size());
         expr = MK_EXPR(kind, args);