Fixing failing test in r521

Adding general support for associative operators in SMT v1 and v2

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 59dbf77e5efa53ff0e68aaf0f01f9084a05bc114..8cfd50f0854ec6bc92c41198f35accce470c3356 100644 (file)
--- 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 cfe41316c3784ef62a8032d1d06fd00987ef9156..9c609d0d41911b88282ba01742cf0bc7759bceac 100644 (file)
--- 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 10597662862114592f6ecfa2af4450610bc31678..b8557665ec90fdccfdc8b27ffb6d685673210115 100644 (file)
--- 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);