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/smt/Smt.g | |
| parent | eee91ecc512e94358a02d2aa155764e4cda2e5fa (diff) | |
Fixing failing test in r521
Adding general support for associative operators in SMT v1 and v2
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 5 |
1 files changed, 4 insertions, 1 deletions
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()); |