diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 04:05:19 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 04:05:19 +0000 |
| commit | 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 (patch) | |
| tree | da76170cfa5311ce3b72b25e8e8179a4f1aa6f6c /src/parser/smt2/Smt2.g | |
| parent | 04b89b1a5256a8a70df1615c9a7873a2d870fe82 (diff) | |
* Fix some regressions' expected outputs.
* Ensure Rewriter::init() is called before ::rewrite().
The array type enumerator recently gave us an end-run around
::init(). TheoryEngine no longer calls these, they're done
via static initialization.
* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1bfba3eb4..dbefc0305 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -217,8 +217,7 @@ command returns [CVC4::Command* cmd = NULL] symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); } LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK - { - PARSER_STATE->pushScope(); + { PARSER_STATE->pushScope(); for(std::vector<std::string>::const_iterator i = names.begin(), iend = names.end(); i != iend; @@ -308,13 +307,15 @@ command returns [CVC4::Command* cmd = NULL] ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { - cmd = new EmptyCommand; + cmd = new EmptyCommand(); } else if(n == 1) { - cmd = new PushCommand; + PARSER_STATE->pushScope(); + cmd = new PushCommand(); } else { - CommandSequence* seq = new CommandSequence; + CommandSequence* seq = new CommandSequence(); do { - seq->addCommand(new PushCommand); + PARSER_STATE->pushScope(); + seq->addCommand(new PushCommand()); } while(--n > 0); cmd = seq; } @@ -329,13 +330,15 @@ command returns [CVC4::Command* cmd = NULL] ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { - cmd = new EmptyCommand; + cmd = new EmptyCommand(); } else if(n == 1) { - cmd = new PopCommand; + PARSER_STATE->popScope(); + cmd = new PopCommand(); } else { - CommandSequence* seq = new CommandSequence; + CommandSequence* seq = new CommandSequence(); do { - seq->addCommand(new PopCommand); + PARSER_STATE->popScope(); + seq->addCommand(new PopCommand()); } while(--n > 0); cmd = seq; } |