Remove uses of SExpr class. (#6035)

This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.

4 files changed, 70 insertions, 85 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f10191c75..9227c3703 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2572,18 +2572,19 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out,
 /* class SetInfoCommand                                                       */
 /* -------------------------------------------------------------------------- */
 
-SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr)
-    : d_flag(flag), d_sexpr(sexpr)
+SetInfoCommand::SetInfoCommand(const std::string& flag,
+                               const std::string& value)
+    : d_flag(flag), d_value(value)
 {
 }
 
-std::string SetInfoCommand::getFlag() const { return d_flag; }
-const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; }
+const std::string& SetInfoCommand::getFlag() const { return d_flag; }
+const std::string& SetInfoCommand::getValue() const { return d_value; }
 void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->setInfo(d_flag, d_sexpr);
+    solver->setInfo(d_flag, d_value);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (api::CVC4ApiRecoverableException&)
@@ -2599,7 +2600,7 @@ void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 
 Command* SetInfoCommand::clone() const
 {
-  return new SetInfoCommand(d_flag, d_sexpr);
+  return new SetInfoCommand(d_flag, d_value);
 }
 
 std::string SetInfoCommand::getCommandName() const { return "set-info"; }
@@ -2609,7 +2610,7 @@ void SetInfoCommand::toStream(std::ostream& out,
                               size_t dag,
                               OutputLanguage language) const
 {
-  Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr);
+  Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_value);
 }
 
 /* -------------------------------------------------------------------------- */
@@ -2672,18 +2673,19 @@ void GetInfoCommand::toStream(std::ostream& out,
 /* class SetOptionCommand                                                     */
 /* -------------------------------------------------------------------------- */
 
-SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr)
-    : d_flag(flag), d_sexpr(sexpr)
+SetOptionCommand::SetOptionCommand(const std::string& flag,
+                                   const std::string& value)
+    : d_flag(flag), d_value(value)
 {
 }
 
-std::string SetOptionCommand::getFlag() const { return d_flag; }
-const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; }
+const std::string& SetOptionCommand::getFlag() const { return d_flag; }
+const std::string& SetOptionCommand::getValue() const { return d_value; }
 void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->setOption(d_flag, d_sexpr);
+    solver->setOption(d_flag, d_value);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (api::CVC4ApiRecoverableException&)
@@ -2698,7 +2700,7 @@ void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 
 Command* SetOptionCommand::clone() const
 {
-  return new SetOptionCommand(d_flag, d_sexpr);
+  return new SetOptionCommand(d_flag, d_value);
 }
 
 std::string SetOptionCommand::getCommandName() const { return "set-option"; }
@@ -2708,7 +2710,7 @@ void SetOptionCommand::toStream(std::ostream& out,
                                 size_t dag,
                                 OutputLanguage language) const
 {
-  Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr);
+  Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_value);
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index a88b7e022..c11012944 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1298,13 +1298,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command
 {
  protected:
   std::string d_flag;
-  std::string d_sexpr;
+  std::string d_value;
 
  public:
-  SetInfoCommand(std::string flag, const std::string& sexpr);
+  SetInfoCommand(const std::string& flag, const std::string& value);
 
-  std::string getFlag() const;
-  const std::string& getSExpr() const;
+  const std::string& getFlag() const;
+  const std::string& getValue() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
@@ -1343,13 +1343,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command
 {
  protected:
   std::string d_flag;
-  std::string d_sexpr;
+  std::string d_value;
 
  public:
-  SetOptionCommand(std::string flag, const std::string& sexpr);
+  SetOptionCommand(const std::string& flag, const std::string& value);
 
-  std::string getFlag() const;
-  const std::string& getSExpr() const;
+  const std::string& getFlag() const;
+  const std::string& getValue() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ed5e73d5d..80d7b96fa 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -435,53 +435,51 @@ void SmtEngine::setLogicInternal()
   d_userLogic.lock();
 }
 
-void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
+void SmtEngine::setInfo(const std::string& key, const std::string& value)
 {
   SmtScope smts(this);
 
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
 
-  if(Dump.isOn("benchmark")) {
-    if(key == "status") {
-      string s = value.getValue();
+  if (Dump.isOn("benchmark"))
+  {
+    if (key == "status")
+    {
       Result::Sat status =
-          (s == "sat") ? Result::SAT
-                       : ((s == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
+          (value == "sat")
+              ? Result::SAT
+              : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
       getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus(
           getOutputManager().getDumpOut(), status);
-    } else {
+    }
+    else
+    {
       getOutputManager().getPrinter().toStreamCmdSetInfo(
           getOutputManager().getDumpOut(), key, value);
     }
   }
 
-  // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
-  if (key == "source" || key == "category" || key == "difficulty"
-      || key == "notes" || key == "name" || key == "license")
+  if (key == "filename")
   {
-    // ignore these
-    return;
-  }
-  else if (key == "filename")
-  {
-    d_state->setFilename(value.getValue());
-    return;
+    d_state->setFilename(value);
   }
   else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser())
   {
     language::input::Language ilang = language::input::LANG_AUTO;
-    if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
-        (value.isRational() && value.getRationalValue() == Rational(2)) ||
-        value.getValue() == "2" ||
-        value.getValue() == "2.0" ) {
+
+    if (value == "2" || value == "2.0")
+    {
       ilang = language::input::LANG_SMTLIB_V2_0;
-    } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
-               value.getValue() == "2.5" ) {
+    }
+    else if (value == "2.5")
+    {
       ilang = language::input::LANG_SMTLIB_V2_5;
-    } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
-               value.getValue() == "2.6" ) {
+    }
+    else if (value == "2.6")
+    {
       ilang = language::input::LANG_SMTLIB_V2_6;
     }
+
     options::inputLanguage.set(ilang);
     // also update the output language
     if (!options::outputLanguage.wasSetByUser())
@@ -493,18 +491,10 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
         *options::out() << language::SetLanguage(olang);
       }
     }
-    return;
-  } else if(key == "status") {
-    string s;
-    if(value.isAtom()) {
-      s = value.getValue();
-    }
-    if(s != "sat" && s != "unsat" && s != "unknown") {
-      throw OptionException("argument to (set-info :status ..) must be "
-                            "`sat' or `unsat' or `unknown'");
-    }
-    d_state->notifyExpectedStatus(s);
-    return;
+  }
+  else if (key == "status")
+  {
+    d_state->notifyExpectedStatus(value);
   }
 }
 
@@ -1913,16 +1903,9 @@ void SmtEngine::setUserAttribute(const std::string& attr,
   te->setUserAttribute(attr, expr, expr_values, str_value);
 }
 
-void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
+void SmtEngine::setOption(const std::string& key, const std::string& value)
 {
-  // Always check whether the SmtEngine has been initialized (which is done
-  // upon entering Assert mode the first time). No option can  be set after
-  // initialized.
-  if (d_state->isFullyInited())
-  {
-    throw ModalException("SmtEngine::setOption called after initialization.");
-  }
-  NodeManagerScope nms(d_nodeManager);
+    NodeManagerScope nms(d_nodeManager);
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
   if(Dump.isOn("benchmark")) {
@@ -1931,28 +1914,29 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
   }
 
   if(key == "command-verbosity") {
-    if(!value.isAtom()) {
-      const vector<SExpr>& cs = value.getChildren();
-      if(cs.size() == 2 &&
-         (cs[0].isKeyword() || cs[0].isString()) &&
-         cs[1].isInteger()) {
-        string c = cs[0].getValue();
-        const Integer& v = cs[1].getIntegerValue();
-        if(v < 0 || v > 2) {
-          throw OptionException("command-verbosity must be 0, 1, or 2");
-        }
-        d_commandVerbosity[c] = v;
-        return;
+    size_t fstIndex = value.find(" ");
+    size_t sndIndex = value.find(" ", fstIndex + 1);
+    if (sndIndex == std::string::npos)
+    {
+      string c = value.substr(1, fstIndex - 1);
+      int v =
+          std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1));
+      if (v < 0 || v > 2)
+      {
+        throw OptionException("command-verbosity must be 0, 1, or 2");
       }
+      d_commandVerbosity[c] = v;
+      return;
     }
     throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
   }
 
-  if(!value.isAtom()) {
+  if (value.find(" ") != std::string::npos)
+  {
     throw OptionException("bad value for :" + key);
   }
 
-  string optionarg = value.getValue();
+  std::string optionarg = value;
   d_options.setOption(key, optionarg);
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 53a5b7f2f..8974e5e60 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -218,9 +218,8 @@ class CVC4_PUBLIC SmtEngine
 
   /**
    * Set information about the script executing.
-   * @throw OptionException, ModalException
    */
-  void setInfo(const std::string& key, const CVC4::SExpr& value);
+  void setInfo(const std::string& key, const std::string& value);
 
   /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */
   bool isValidGetInfoFlag(const std::string& key) const;
@@ -232,7 +231,7 @@ class CVC4_PUBLIC SmtEngine
    * Set an aspect of the current SMT execution environment.
    * @throw OptionException, ModalException
    */
-  void setOption(const std::string& key, const CVC4::SExpr& value);
+  void setOption(const std::string& key, const std::string& value);
 
   /** Set is internal subsolver.
    *