diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-04-06 22:06:52 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-04-06 22:06:52 +0000 |
| commit | 7237456b4e2e5a119feacf98f52ec9e55d7a62a5 (patch) | |
| tree | ea510f4987dadcdbbb361684445419e4939cdf00 /src/parser/smt2 | |
| parent | 6a5fb6d945b109921cb9b6117f4ede0b6d110c08 (diff) | |
* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)
Diffstat (limited to 'src/parser/smt2')
| -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 926ce1718..d478bd843 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -405,9 +405,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] std::string s; } : INTEGER_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } + { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } + { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } | str[s] { sexpr = SExpr(s); } | SYMBOL |