diff options
| -rw-r--r-- | src/parser/smt/Smt.g | 11 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/util/options.cpp | 4 | ||||
| -rw-r--r-- | src/util/options.h | 2 |
4 files changed, 21 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 - : '{' ( '\\{' | '\\}' | ~('{' | '}') )* '}' + : '{' ('\\{' | '\\}' | ~('{' | '}'))* '}' ; /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fee77df39..4f28225af 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -362,8 +362,14 @@ void SmtEngine::setLogicInternal(const std::string& s) throw() { // by default, symmetry breaker is on only for QF_UF if(! Options::current()->ufSymmetryBreakerSetByUser) { + Trace("smt") << "setting uf symmetry breaker to " << (s == "QF_UF") << std::endl; NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF"); } + // by default, nonclausal simplification is off for QF_SAT + if(! Options::current()->simplificationModeSetByUser) { + Trace("smt") << "setting simplification mode to <" << s << "> " << (s != "QF_SAT") << std::endl; + NodeManager::currentNM()->getOptions()->simplificationMode = (s == "QF_SAT" ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH); + } // If in arrays, set the UF handler to arrays if(s == "QF_AX") { diff --git a/src/util/options.cpp b/src/util/options.cpp index f9ab0b480..175b7f228 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -78,6 +78,7 @@ Options::Options() : lazyDefinitionExpansion(false), printWinner(false), simplificationMode(SIMPLIFICATION_MODE_BATCH), + simplificationModeSetByUser(false), doStaticLearning(true), interactive(false), interactiveSetByUser(false), @@ -674,10 +675,13 @@ throw(OptionException) { case SIMPLIFICATION_MODE: if(!strcmp(optarg, "batch")) { simplificationMode = SIMPLIFICATION_MODE_BATCH; + simplificationModeSetByUser = true; } else if(!strcmp(optarg, "incremental")) { simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL; + simplificationModeSetByUser = true; } else if(!strcmp(optarg, "none")) { simplificationMode = SIMPLIFICATION_MODE_NONE; + simplificationModeSetByUser = true; } else if(!strcmp(optarg, "help")) { puts(simplificationHelp.c_str()); exit(1); diff --git a/src/util/options.h b/src/util/options.h index 6b8054a13..cdcefa14f 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -123,6 +123,8 @@ struct CVC4_PUBLIC Options { /** When/whether to perform nonclausal simplifications. */ SimplificationMode simplificationMode; + /** Whether the user set the nonclausal simplification mode. */ + bool simplificationModeSetByUser; /** Whether to perform the static learning pass. */ bool doStaticLearning; |