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/smt/Smt.g | |
| 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/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 53a05a9a4..5a80083b3 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -536,6 +536,7 @@ annotation[CVC4::Command*& smt_command] { std::string value = AntlrInput::tokenText($USER_VALUE); Assert(*value.begin() == '{'); Assert(*value.rbegin() == '}'); + // trim whitespace value.erase(value.begin(), value.begin() + 1); value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); value.erase(value.end() - 1); |