Print `unsupported` for unrecognized flags. (#7384)

Fixes #7374.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 90f6f0d5647688f10037d975b3ec6cfe1d06e0d3..f587bbfc0c10f140c621a1de8d80cae33d873fb4 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -855,6 +855,27 @@ class CVC5ApiRecoverableExceptionStream
   std::stringstream d_stream;
 };
 
+class CVC5ApiUnsupportedExceptionStream
+{
+ public:
+  CVC5ApiUnsupportedExceptionStream() {}
+  /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
+   * a destructor that throws an exception and in C++11 all destructors
+   * default to noexcept(true) (else this triggers a call to std::terminate). */
+  ~CVC5ApiUnsupportedExceptionStream() noexcept(false)
+  {
+    if (std::uncaught_exceptions() == 0)
+    {
+      throw CVC5ApiUnsupportedException(d_stream.str());
+    }
+  }
+
+  std::ostream& ostream() { return d_stream; }
+
+ private:
+  std::stringstream d_stream;
+};
+
 #define CVC5_API_TRY_CATCH_BEGIN \
   try                            \
   {
@@ -6917,8 +6938,8 @@ std::vector<Term> Solver::getAssertions(void) const
 std::string Solver::getInfo(const std::string& flag) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_RECOVERABLE_CHECK(d_slv->isValidGetInfoFlag(flag))
-      << "Unrecognized flag for getInfo.";
+  CVC5_API_UNSUPPORTED_CHECK(d_slv->isValidGetInfoFlag(flag))
+      << "Unrecognized flag: " << flag << ".";
   //////// all checks before this line
   return d_slv->getInfo(flag);
   ////////
@@ -6927,11 +6948,14 @@ std::string Solver::getInfo(const std::string& flag) const
 
 std::string Solver::getOption(const std::string& option) const
 {
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  return d_slv->getOption(option);
-  ////////
-  CVC5_API_TRY_CATCH_END;
+  try
+  {
+    return d_slv->getOption(option);
+  }
+  catch (OptionException& e)
+  {
+    throw CVC5ApiUnsupportedException(e.getMessage());
+  }
 }
 
 // Supports a visitor from a list of lambdas
@@ -7564,13 +7588,14 @@ void Solver::resetAssertions(void) const
 void Solver::setInfo(const std::string& keyword, const std::string& value) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
+  CVC5_API_UNSUPPORTED_CHECK(
       keyword == "source" || keyword == "category" || keyword == "difficulty"
-          || keyword == "filename" || keyword == "license" || keyword == "name"
-          || keyword == "notes" || keyword == "smt-lib-version"
-          || keyword == "status",
-      keyword)
-      << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
+      || keyword == "filename" || keyword == "license" || keyword == "name"
+      || keyword == "notes" || keyword == "smt-lib-version"
+      || keyword == "status")
+      << "Unrecognized keyword: " << keyword
+      << ", expected 'source', 'category', 'difficulty', "
+         "'filename', 'license', 'name', "
          "'notes', 'smt-lib-version' or 'status'";
   CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(
       keyword != "smt-lib-version" || value == "2" || value == "2.0"
@@ -7603,6 +7628,11 @@ void Solver::setOption(const std::string& option,
                        const std::string& value) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  std::vector<std::string> options = options::getNames();
+  CVC5_API_UNSUPPORTED_CHECK(
+      option.find("command-verbosity") != std::string::npos
+      || std::find(options.cbegin(), options.cend(), option) != options.cend())
+      << "Unrecognized option: " << option << '.';
   static constexpr auto mutableOpts = {"diagnostic-output-channel",
                                        "print-success",
                                        "regular-output-channel",

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index f348ae4e5e1d694c2d8103030adc1c67ac797934..b73c1ce27af8504670202b242d60587625636250 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -120,6 +120,31 @@ class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException
   }
 };
 
+/**
+ * Exception for unsupported command arguments.
+ * If thrown, API objects can still be used.
+ */
+class CVC5_EXPORT CVC5ApiUnsupportedException : public CVC5ApiRecoverableException
+{
+ public:
+  /**
+   * Construct with message from a string.
+   * @param str The error message.
+   */
+  CVC5ApiUnsupportedException(const std::string& str)
+      : CVC5ApiRecoverableException(str)
+  {
+  }
+  /**
+   * Construct with message from a string stream.
+   * @param stream The error message.
+   */
+  CVC5ApiUnsupportedException(const std::stringstream& stream)
+      : CVC5ApiRecoverableException(stream.str())
+  {
+  }
+};
+
 /**
  * An option-related API exception.
  * If thrown, API objects can still be used.

diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h
index 35c21df9c9e0e8c1deae07ca8b0323b8cf469ca7..71b17cef119a000e481121b92e03253d53e25cb6 100644 (file)
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -43,6 +43,14 @@ namespace api {
   CVC5_PREDICT_TRUE(cond)                \
   ? (void)0 : OstreamVoider() & CVC5ApiRecoverableExceptionStream().ostream()
 
+/**
+ * The base check macro for throwing unsupported exceptions.
+ * Throws a CVC5ApiUnsupportedException if 'cond' is false.
+ */
+#define CVC5_API_UNSUPPORTED_CHECK(cond) \
+  CVC5_PREDICT_TRUE(cond)                \
+  ? (void)0 : OstreamVoider() & CVC5ApiUnsupportedExceptionStream().ostream()
+
 /* -------------------------------------------------------------------------- */
 /* Not null checks.                                                           */
 /* -------------------------------------------------------------------------- */

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index a15e209989134a93fac5d6779a7058b82bd6e5a2..419167e7ec05b9ff5938c15851c10bec00b0e13b 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2557,11 +2557,15 @@ void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
     solver->setInfo(d_flag, d_value);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (api::CVC5ApiRecoverableException&)
+  catch (api::CVC5ApiUnsupportedException&)
   {
     // As per SMT-LIB spec, silently accept unknown set-info keys
     d_commandStatus = CommandSuccess::instance();
   }
+  catch (api::CVC5ApiRecoverableException& e)
+  {
+    d_commandStatus = new CommandRecoverableFailure(e.getMessage());
+  }
   catch (exception& e)
   {
     d_commandStatus = new CommandFailure(e.what());
@@ -2599,9 +2603,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
     d_result = sexprToString(solver->mkTerm(api::SEXPR, v));
     d_commandStatus = CommandSuccess::instance();
   }
+  catch (api::CVC5ApiUnsupportedException&)
+  {
+    d_commandStatus = new CommandUnsupported();
+  }
   catch (api::CVC5ApiRecoverableException& e)
   {
-    d_commandStatus = new CommandRecoverableFailure(e.what());
+    d_commandStatus = new CommandRecoverableFailure(e.getMessage());
   }
   catch (exception& e)
   {
@@ -2658,10 +2666,14 @@ void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
     solver->setOption(d_flag, d_value);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (api::CVC5ApiRecoverableException&)
+  catch (api::CVC5ApiUnsupportedException&)
   {
     d_commandStatus = new CommandUnsupported();
   }
+  catch (api::CVC5ApiRecoverableException& e)
+  {
+    d_commandStatus = new CommandRecoverableFailure(e.getMessage());
+  }
   catch (exception& e)
   {
     d_commandStatus = new CommandFailure(e.what());
@@ -2696,7 +2708,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
     d_result = solver->getOption(d_flag);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (api::CVC5ApiRecoverableException&)
+  catch (api::CVC5ApiUnsupportedException&)
   {
     d_commandStatus = new CommandUnsupported();
   }

diff --git a/test/regress/regress0/smtlib/issue7374.smt2 b/test/regress/regress0/smtlib/issue7374.smt2
new file mode 100644 (file)
index 0000000..59caef5
--- /dev/null
+++ b/test/regress/regress0/smtlib/issue7374.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsupported
+; EXPECT: unsupported
+; EXPECT: unsupported
+
+(set-logic QF_SAT)
+(set-info :zzz true)
+(get-info :zzz)
+(set-option :zzz true)
+(get-option :zzz)

diff --git a/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2 b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
index 1595b086533c2c547389c999ca69df8a0d3cc2f0..44bccd26431efae995ba3cb0638c095b3d2a6444 100644 (file)
--- a/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
+++ b/test/regress/regress1/abduction/abduction_1255.corecstrs.readable.smt2
@@ -3,7 +3,7 @@
 ; EXIT: 0
 
 
-(set-info :smt-lib-version |2.6|)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :source |
 Generated by: Andrew Reynolds

diff --git a/test/regress/regress1/abduction/abduction_streq.readable.smt2 b/test/regress/regress1/abduction/abduction_streq.readable.smt2
index b466ab33e66d6d2b384064cd778ee5d206a0379f..c13f3175e186c4b5f7cac49a9e4aa4ebf6d47694 100644 (file)
--- a/test/regress/regress1/abduction/abduction_streq.readable.smt2
+++ b/test/regress/regress1/abduction/abduction_streq.readable.smt2
@@ -2,7 +2,7 @@
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
 
-(set-info :smt-lib-version |2.6|)
+(set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :source |
 Generated by: Andrew Reynolds