diff options
Diffstat (limited to 'src/parser')
-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 |
3 files changed, 8 insertions, 6 deletions
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); } |