diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-06-30 21:03:52 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-06-30 21:03:52 +0000 |
| commit | af25c3f8498198dd6dd114c3b4ef39af54611e1e (patch) | |
| tree | 6f0f8e84685bf58dcd003e9f3da630e58163873e | |
| parent | 5f8b41a0b896c2224ac4fc3b13eba7c370764df6 (diff) | |
Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),
when --strict-parsing is off (which it is by default). The danoint benchmarks
have such monsters.
| -rw-r--r-- | src/parser/smt/Smt.g | 4 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index b03188b3c..2a3a79125 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -218,6 +218,10 @@ annotatedFormula[CVC4::Expr& expr] args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); + } else if(!PARSER_STATE->strictModeEnabled() && + kind == CVC4::kind::MINUS && args.size() == 1) { + /* Special fix-up for unary minus improperly used in some benchmarks */ + expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); } else { PARSER_STATE->checkArity(kind, args.size()); expr = MK_EXPR(kind, args); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a8dfbfeab..091e6c93c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -765,7 +765,7 @@ POUND_TOK : '#'; SELECT_TOK : 'select'; STAR_TOK : '*'; STORE_TOK : 'store'; -TILDE_TOK : '~'; +// TILDE_TOK : '~'; XOR_TOK : 'xor'; CONCAT_TOK : 'concat'; |