diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 02:02:07 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-06-01 02:02:07 +0000 |
commit | aad6d724f09fe523d7c1d53e2db959801f28fc3e (patch) | |
tree | 53eddc4dbe8d24751ccd0a0a54a50bd5b2137627 /src/parser/smt2 | |
parent | eee91ecc512e94358a02d2aa155764e4cda2e5fa (diff) |
Fixing failing test in r521
Adding general support for associative operators in SMT v1 and v2
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
1 files changed, 5 insertions, 0 deletions
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); |