diff options
| author | François Bobot <francois@bobot.eu> | 2012-11-30 11:35:02 +0000 |
|---|---|---|
| committer | François Bobot <francois@bobot.eu> | 2012-11-30 11:35:02 +0000 |
| commit | 4643949ff4f1586935dfc2607931f26604422b50 (patch) | |
| tree | 26c983d56bea5b5112d70ef60766ff4ca99c71f0 /src | |
| parent | c157f7e381d4fa2a713796b42a10562112952904 (diff) | |
fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
just after the bindings
Do it before the release in order to not break user files later
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 39149ec89..87cf2083d 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -532,9 +532,9 @@ rewriterulesCommand[CVC4::Command*& cmd] } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK term[head, expr2] term[body, expr2] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK { args.clear(); args.push_back(head); @@ -573,10 +573,10 @@ rewriterulesCommand[CVC4::Command*& cmd] } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } + LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK LPAREN_TOK (termList[guards,expr])? RPAREN_TOK LPAREN_TOK (termList[heads,expr])? RPAREN_TOK term[body, expr2] - LPAREN_TOK ( pattern[expr] { triggers.push_back( expr ); } )* RPAREN_TOK { args.clear(); /* heads */ |