diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-27 22:04:38 +0000 |
| commit | ad0a71e2782bc291ba9f808d24df2e1d8ca1b41e (patch) | |
| tree | 744a9ae0f10f6dd8837d7e0dcd8bd2b25d34e481 /src/parser/cvc | |
| parent | 51daaee8eb1ee55ee3323c5395a95fd121fe87a8 (diff) | |
* Rename SMT parts (printer, parser) to SMT1
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 82e27401e..4577b504c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -561,6 +561,16 @@ parseExpr returns [CVC4::Expr expr = CVC4::Expr()] */ parseCommand returns [CVC4::Command* cmd = NULL] : c=command { $cmd = c; } + | LPAREN IDENTIFIER + { std::string s = AntlrInput::tokenText($IDENTIFIER); + if(s == "benchmark") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected. Use --lang smt1 for SMT-LIBv1 support."); + } else if(s == "set" || s == "get") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected. Use --lang smt2 for SMT-LIBv2 support."); + } else { + PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name."); + } + } | EOF { $cmd = NULL; } ; |