diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-31 21:55:40 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-31 21:55:40 +0000 |
| commit | cfb3b789e26fdab73e733825950b24492c6c5e4c (patch) | |
| tree | dec99da95dd6c1dd0def3adaa46d5e7e9e94b4e6 /src/parser | |
| parent | aa21ac1746612b646e464615d4eeb07586f4ed36 (diff) | |
First draft implementation of mkAssociative
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt/Smt.g | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 07dd3de5b..cfe41316c 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -187,6 +187,8 @@ 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) ) { + expr = EXPR_MANAGER->mkAssociative(kind,args); } else { PARSER_STATE->checkArity(kind, args.size()); expr = MK_EXPR(kind, args); |