diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-03-21 20:51:02 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-03-21 20:51:02 +0000 |
| commit | f40ec39fe48f83e1cc1a31f9e18635687bd63c76 (patch) | |
| tree | daba20eb93798b196a8fb324438152fba7f8e867 /src/parser/smt/Smt.g | |
| parent | 84f26af22566f7c10dea45b399b944cb50b5e317 (diff) | |
Disable nonclausal simplification for QF_SAT benchmarks by default.
(Can be overridden with --simplification=batch, for example.)
Diffstat (limited to 'src/parser/smt/Smt.g')
| -rw-r--r-- | src/parser/smt/Smt.g | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 932d9be78..53a05a9a4 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -533,7 +533,14 @@ annotation[CVC4::Command*& smt_command] } : attribute[key] ( USER_VALUE - { smt_command = new SetInfoCommand(key, AntlrInput::tokenText($USER_VALUE)); } + { std::string value = AntlrInput::tokenText($USER_VALUE); + Assert(*value.begin() == '{'); + Assert(*value.rbegin() == '}'); + 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); + value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end()); + smt_command = new SetInfoCommand(key, value); } )? { if(smt_command == NULL) { smt_command = new EmptyCommand(std::string("annotation: ") + key); @@ -715,7 +722,7 @@ FLET_IDENTIFIER * with an open brace and end with closed brace. */ USER_VALUE - : '{' ( '\\{' | '\\}' | ~('{' | '}') )* '}' + : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}' ; /** |