From aad6d724f09fe523d7c1d53e2db959801f28fc3e Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Tue, 1 Jun 2010 02:02:07 +0000
Subject: [PATCH] Fixing failing test in r521 Adding general support for
 associative operators in SMT v1 and v2

---
 src/expr/expr_manager_template.cpp | 2 ++
 src/parser/smt/Smt.g               | 5 ++++-
 src/parser/smt2/Smt2.g             | 5 +++++
 3 files changed, 11 insertions(+), 1 deletion(-)

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);
-- 
2.30.2