diff options
| -rw-r--r-- | src/main/command_executor.cpp | 2 | ||||
| -rw-r--r-- | src/parser/smt1/smt1.cpp | 2 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 10 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | src/theory/logic_info.cpp | 14 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 6 |
7 files changed, 23 insertions, 17 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index f9055f56c..64025fc04 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -254,7 +254,7 @@ void CommandExecutor::printStatsFilterZeros(std::ostream& out, std::getline(iss, statValue, '\n'); double curFloat; - bool isFloat = (std::istringstream(statValue) >> curFloat); + bool isFloat = static_cast<bool>(std::istringstream(statValue) >> curFloat); if( (isFloat && curFloat == 0) || statValue == " \"0\"" || diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp index 50f62009a..015129f10 100644 --- a/src/parser/smt1/smt1.cpp +++ b/src/parser/smt1/smt1.cpp @@ -62,6 +62,8 @@ std::hash_map<const std::string, Smt1::Logic, CVC4::StringHashFunction> Smt1::ne logicMap["UFLRA"] = UFLRA; logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; + logicMap["QF_ALL"] = QF_ALL_SUPPORTED; + logicMap["ALL"] = ALL_SUPPORTED; return logicMap; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 27c5a62bd..ff34fd9a3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -272,7 +272,7 @@ command [CVC4::PtrCloser<CVC4::Command>* cmd] } PARSER_STATE->setLogic(name); if( PARSER_STATE->sygus() ){ - cmd->reset(new SetBenchmarkLogicCommand("ALL_SUPPORTED")); + cmd->reset(new SetBenchmarkLogicCommand("ALL")); }else{ cmd->reset(new SetBenchmarkLogicCommand(name)); } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 8db344f92..2e2481a6e 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -370,7 +370,7 @@ void Smt2::setLogic(std::string name) { name = "UFSLIA"; } else if(name == "SAT") { name = "UF"; - } else if(name == "ALL_SUPPORTED") { + } else if(name == "ALL" || name == "ALL_SUPPORTED") { //no change } else { std::stringstream ss; @@ -456,14 +456,14 @@ void Smt2::checkThatLogicIsSet() { setLogic("LIA"); } else { warning("No set-logic command was given before this point."); - warning("CVC4 will assume the non-standard ALL_SUPPORTED logic."); + warning("CVC4 will make all theories available."); warning("Consider setting a stricter logic for (likely) better performance."); - warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED)."); + warning("To suppress this warning in the future use (set-logic ALL)."); - setLogic("ALL_SUPPORTED"); + setLogic("ALL"); } - Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); + Command* c = new SetBenchmarkLogicCommand("ALL"); c->setMuted(true); preemptCommand(c); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 38347508c..5fc96aa6e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1645,7 +1645,7 @@ void SmtEngine::setDefaults() { // Set decision mode based on logic (if not set by user) if(!options::decisionMode.wasSetByUser()) { decision::DecisionMode decMode = - // ALL_SUPPORTED + // ALL d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION : ( // QF_BV (not d_logic.isQuantified() && @@ -1676,7 +1676,7 @@ void SmtEngine::setDefaults() { ); bool stoponly = - // ALL_SUPPORTED + // ALL d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false : ( // QF_AUFLIA (not d_logic.isQuantified() && diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 6ac1c5e32..0e4ccf0f7 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -242,9 +242,9 @@ std::string LogicInfo::getLogicString() const { qf_all_supported.disableQuantifiers(); qf_all_supported.lock(); if(hasEverything()) { - d_logicString = "ALL_SUPPORTED"; + d_logicString = "ALL"; } else if(*this == qf_all_supported) { - d_logicString = "QF_ALL_SUPPORTED"; + d_logicString = "QF_ALL"; } else { size_t seen = 0; // make sure we support all the active theories @@ -341,11 +341,21 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableEverything(); disableQuantifiers(); p += 16; + } else if(!strcmp(p, "QF_ALL")) { + // the "all theories included" logic, no quantifiers + enableEverything(); + disableQuantifiers(); + p += 6; } else if(!strcmp(p, "ALL_SUPPORTED")) { // the "all theories included" logic, with quantifiers enableEverything(); enableQuantifiers(); p += 13; + } else if(!strcmp(p, "ALL")) { + // the "all theories included" logic, with quantifiers + enableEverything(); + enableQuantifiers(); + p += 3; } else { if(!strncmp(p, "QF_", 3)) { disableQuantifiers(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 26e6908da..8b44b5cac 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -646,12 +646,6 @@ void TheoryStrings::check(Effort e) { bool polarity; TNode atom; - /*if(getLogicInfo().hasEverything()) { - WarningOnce() << "WARNING: strings not supported in default configuration (ALL_SUPPORTED).\n" - << "To suppress this warning in the future use proper logic symbol, e.g. (set-logic QF_S)." << std::endl; - } - }*/ - if( !done() && !hasTerm( d_emptyString ) ) { preRegisterTerm( d_emptyString ); } |