Fix sexpr bug with AST output language. (#6329)

When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b29647311c4fc69c42e9e589f082d1d5cbf0498e..435597bc7764db3256a71d28a48c674c94461ede 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6219,8 +6219,7 @@ std::string Solver::getOption(const std::string& option) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  Node res = d_smtEngine->getOption(option);
-  return res.toString();
+  return d_smtEngine->getOption(option);
   ////////
   CVC5_API_TRY_CATCH_END;
 }

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5f85445ff48ad78301220446c33248b9075342b6..55bf68b9ff202cd47ea10d144d9a44c6cbb79a6d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1926,7 +1926,7 @@ void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
 
 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
 
-Node SmtEngine::getOption(const std::string& key) const
+std::string SmtEngine::getOption(const std::string& key) const
 {
   NodeManagerScope nms(getNodeManager());
   NodeManager* nm = d_env->getNodeManager();
@@ -1939,14 +1939,14 @@ Node SmtEngine::getOption(const std::string& key) const
         d_commandVerbosity.find(key.c_str() + 18);
     if (i != d_commandVerbosity.end())
     {
-      return nm->mkConst(Rational(i->second));
+      return i->second.toString();
     }
     i = d_commandVerbosity.find("*");
     if (i != d_commandVerbosity.end())
     {
-      return nm->mkConst(Rational(i->second));
+      return i->second.toString();
     }
-    return nm->mkConst(Rational(2));
+    return "2";
   }
 
   if (Dump.isOn("benchmark"))
@@ -1984,30 +1984,24 @@ Node SmtEngine::getOption(const std::string& key) const
                                     nm->mkConst(Rational(2)));
     }
     result.push_back(defaultVerbosity);
-    return nm->mkNode(Kind::SEXPR, result);
+    return nm->mkNode(Kind::SEXPR, result).toString();
   }
 
-  // parse atom string
   std::string atom = getOptions().getOption(key);
 
-  if (atom == "true")
+  if (atom != "true" && atom != "false")
   {
-    return nm->mkConst<bool>(true);
-  }
-  else if (atom == "false")
-  {
-    return nm->mkConst<bool>(false);
-  }
-  try
-  {
-    Integer z(atom);
-    return nm->mkConst(Rational(z));
-  }
-  catch (std::invalid_argument&)
-  {
-    // Fall through to the next case
+    try
+    {
+      Integer z(atom);
+    }
+    catch (std::invalid_argument&)
+    {
+      atom = "\"" + atom + "\"";
+    }
   }
-  return nm->mkConst(String(atom));
+
+  return atom;
 }
 
 Options& SmtEngine::getOptions() { return d_env->d_options; }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 63ba5f8310ffe2f2abce23c55e091357d10200c9..51eed32b2bff5949cd07bf56d122385d1c29e910 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -317,7 +317,7 @@ class CVC4_EXPORT SmtEngine
    * Get an aspect of the current SMT execution environment.
    * @throw OptionException
    */
-  Node getOption(const std::string& key) const;
+  std::string getOption(const std::string& key) const;
 
   /**
    * Define function func in the current context to be:

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c40174eda125436297f0404b10443c61d2d4a1cb..e84281a0d09ceed926f28dac15cab052742376f9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -710,6 +710,7 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/opt-abd-no-use.smt2
+  regress0/options/ast-and-sexpr.smt2
   regress0/options/invalid_dump.smt2
   regress0/options/set-and-get-options.smt2
   regress0/parallel-let.smt2

diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2
new file mode 100644 (file)
index 0000000..2a46457
--- /dev/null
+++ b/test/regress/regress0/options/ast-and-sexpr.smt2
@@ -0,0 +1,17 @@
+; EXPECT: (SEXPR (SEXPR check-sat (CONST_RATIONAL 2)) (SEXPR * (CONST_RATIONAL 1)))
+; EXPECT: (:status unknown)
+
+; This regression tests uses of s-expressions when the output-language is AST
+
+(set-option :output-language ast)
+
+; Set the verbosity of all commands to 1
+(set-option :command-verbosity (* 1))
+; Set the verbosity of (check-sat) command to 2
+(set-option :command-verbosity (check-sat 2))
+; Get the verbosity of all commands
+(get-option :command-verbosity)
+; There is no SMT option to get the verbosity of a specific command
+
+(set-info :source (0 1 True False x ""))
+(get-info :status)