Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

diff --git a/library_versions b/library_versions
index eac360c34fa8bc8d0758445ab0a2ff51ccdb5800..7174f7b0b1d355c4dbf26ec9fb63ca83261432ce 100644 (file)
--- 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 908ad05e2339e6a75a356c551ca6e4b7541245a8..ab4b13d4ca43fd9c8754de8e6d821838d4b750ef 100644 (file)
--- 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 a22e34c21a62cfaffaa6445bcca47530bd96373f..8266bb1edc27ab93204caace9dc2e0c4c93da2ff 100644 (file)
--- 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 dc9de86621a09a76b5f9a357888187fcab821609..cbd0b510e30eb81070206f333f84fdde856f2d68 100644 (file)
--- 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());
   }