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

Fixes #7374.

7 files changed, 103 insertions, 19 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 90f6f0d56..f587bbfc0 100644
--- 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 f348ae4e5..b73c1ce27 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -121,6 +121,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 35c21df9c..71b17cef1 100644
--- 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 a15e20998..419167e7e 100644
--- 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
index 000000000..59caef57c
--- /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 1595b0865..44bccd264 100644
--- 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 b466ab33e..c13f3175e 100644
--- 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