From d6ef5385a8759d708b75077ec7e919eff783a6cf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 17 May 2013 10:19:54 -0400 Subject: [PATCH] Better error on invalid logic strings. Thanks to David Cok for reporting this issue. --- library_versions | 1 + src/smt/smt_engine.cpp | 16 ++++++++-------- src/smt/smt_engine.h | 4 ++-- src/theory/logic_info.cpp | 7 ++++++- 4 files changed, 17 insertions(+), 11 deletions(-) diff --git a/library_versions b/library_versions index eac360c34..7174f7b0b 100644 --- a/library_versions +++ b/library_versions @@ -53,3 +53,4 @@ 1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.3-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 +# note: SmtEngine::setLogicString() exceptions have changed, bump library version on next release? diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 908ad05e2..ab4b13d4c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -792,21 +792,21 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { SmtScope smts(this); - d_logic = logic; setLogicInternal(); } -void SmtEngine::setLogic(const std::string& s) throw(ModalException) { +void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicException) { SmtScope smts(this); - - setLogic(LogicInfo(s)); + try { + setLogic(LogicInfo(s)); + } catch(IllegalArgumentException& e) { + throw LogicException(e.what()); + } } -void SmtEngine::setLogic(const char* logic) throw(ModalException){ - SmtScope smts(this); - - setLogic(LogicInfo(string(logic))); +void SmtEngine::setLogic(const char* logic) throw(ModalException, LogicException) { + setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a22e34c21..8266bb1ed 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -350,12 +350,12 @@ public: /** * Set the logic of the script. */ - void setLogic(const std::string& logic) throw(ModalException); + void setLogic(const std::string& logic) throw(ModalException, LogicException); /** * Set the logic of the script. */ - void setLogic(const char* logic) throw(ModalException); + void setLogic(const char* logic) throw(ModalException, LogicException); /** * Set the logic of the script. diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index dc9de8662..cbd0b510e 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -241,7 +241,12 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc } if(*p != '\0') { stringstream err; - err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString; + err << "LogicInfo::setLogicString(): "; + if(p == logicString) { + err << "cannot parse logic string: " << logicString; + } else { + err << "junk (\"" << p << "\") at end of logic string: " << logicString; + } IllegalArgument(logicString, err.str().c_str()); } -- 2.30.2