Eliminate more uses of SExpr. (#6149)

This PR eliminates all remaining uses of SExpr outside of statistics.

13 files changed, 103 insertions, 56 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 4ccff9930..e87e6176b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -6229,7 +6229,7 @@ std::string Solver::getOption(const std::string& option) const
 {
   CVC4_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  SExpr res = d_smtEngine->getOption(option);
+  Node res = d_smtEngine->getOption(option);
   return res.toString();
   ////////
   CVC4_API_TRY_CATCH_END;
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 001da12db..846bef5be 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -252,7 +252,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         //     "--tear-down-incremental incompatible with --incremental");
         // }
 
-        // cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
+        // cmd.reset(new SetOptionCommand("incremental", "false"));
         // cmd->setMuted(true);
         // pExecutor->doCommand(cmd);
       }
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index b7997cafa..c12c1efc6 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -538,7 +538,6 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) {
 #include "parser/antlr_input.h"
 #include "parser/antlr_tracing.h"
 #include "parser/parser.h"
-#include "util/integer.h"
 
 }/* @lexer::includes */
 
@@ -551,6 +550,7 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) {
 #include "parser/antlr_tracing.h"
 #include "parser/parser.h"
 #include "smt/command.h"
+#include "util/rational.h"
 
 namespace CVC4 {
   class Expr;
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 0449f13ce..a7fe65f67 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -34,7 +34,6 @@
 namespace CVC4 {
 
 class Command;
-class SExpr;
 
 namespace api {
 class Solver;
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 06b263e51..17fd66848 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -25,7 +25,6 @@
 #include "options/language.h"
 #include "smt/model.h"
 #include "util/result.h"
-#include "util/sexpr.h"
 
 namespace CVC4 {
 
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 664bc2bf9..26ccf5821 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -245,7 +245,6 @@ class Smt2Printer : public CVC4::Printer
                           TNode n,
                           int toDepth,
                           TypeNode tn) const;
-  void toStream(std::ostream& out, const SExpr& sexpr) const;
   void toStream(std::ostream& out, const DType& dt) const;
   /**
    * To stream model sort. This prints the appropriate output for type
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 4fe88ceec..5d27c2eb8 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,7 +38,6 @@
 #include "smt/model.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
-#include "util/sexpr.h"
 #include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
@@ -1641,15 +1640,15 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
     // of whether terms is empty.
     std::vector<api::Term> values = solver->getValue(terms);
     Assert(values.size() == names.size());
-    std::vector<SExpr> sexprs;
+    std::vector<api::Term> sexprs;
     for (size_t i = 0, nterms = terms.size(); i < nterms; i++)
     {
-      std::vector<SExpr> ss;
-      ss.emplace_back(SExpr::Keyword(names[i]));
-      ss.emplace_back(SExpr::Keyword(values[i].toString()));
-      sexprs.emplace_back(ss);
+      // Treat the expression name as a variable name as opposed to a string
+      // constant to avoid printing double quotes around the name.
+      api::Term name = solver->mkVar(solver->getBooleanSort(), names[i]);
+      sexprs.push_back(solver->mkTerm(api::SEXPR, name, values[i]));
     }
-    d_result = SExpr(sexprs);
+    d_result = solver->mkTerm(api::SEXPR, sexprs);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (api::CVC4ApiRecoverableException& e)
@@ -1666,7 +1665,7 @@ void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-SExpr GetAssignmentCommand::getResult() const { return d_result; }
+api::Term GetAssignmentCommand::getResult() const { return d_result; }
 void GetAssignmentCommand::printResult(std::ostream& out,
                                        uint32_t verbosity) const
 {
diff --git a/src/smt/command.h b/src/smt/command.h
index 78e7c4071..1017a74c9 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -29,7 +29,7 @@
 
 #include "api/cvc4cpp.h"
 #include "cvc4_export.h"
-#include "util/sexpr.h"
+#include "options/language.h"
 
 namespace CVC4 {
 
@@ -930,12 +930,12 @@ class CVC4_EXPORT GetValueCommand : public Command
 class CVC4_EXPORT GetAssignmentCommand : public Command
 {
  protected:
-  SExpr d_result;
+  api::Term d_result;
 
  public:
   GetAssignmentCommand();
 
-  SExpr getResult() const;
+  api::Term getResult() const;
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
diff --git a/src/smt/env.h b/src/smt/env.h
index e8f73a4f2..c777a7755 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -22,7 +22,6 @@
 
 #include "options/options.h"
 #include "theory/logic_info.h"
-#include "util/sexpr.h"
 #include "util/statistics.h"
 
 namespace CVC4 {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index aac8ceab7..3493aae11 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1928,12 +1928,14 @@ void SmtEngine::setOption(const std::string& key, const std::string& value)
   NodeManagerScope nms(getNodeManager());
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
-  if(Dump.isOn("benchmark")) {
+  if (Dump.isOn("benchmark"))
+  {
     getPrinter().toStreamCmdSetOption(
         getOutputManager().getDumpOut(), key, value);
   }
 
-  if(key == "command-verbosity") {
+  if (key == "command-verbosity")
+  {
     size_t fstIndex = value.find(" ");
     size_t sndIndex = value.find(" ", fstIndex + 1);
     if (sndIndex == std::string::npos)
@@ -1948,7 +1950,8 @@ void SmtEngine::setOption(const std::string& key, const std::string& value)
       d_commandVerbosity[c] = v;
       return;
     }
-    throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
+    throw OptionException(
+        "command-verbosity value must be a tuple (command-name integer)");
   }
 
   if (value.find(" ") != std::string::npos)
@@ -1964,59 +1967,88 @@ void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
 
 bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
 
-CVC4::SExpr SmtEngine::getOption(const std::string& key) const
+Node SmtEngine::getOption(const std::string& key) const
 {
   NodeManagerScope nms(getNodeManager());
+  NodeManager* nm = d_env->getNodeManager();
 
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
 
-  if(key.length() >= 18 &&
-     key.compare(0, 18, "command-verbosity:") == 0) {
-    map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18);
-    if(i != d_commandVerbosity.end()) {
-      return SExpr((*i).second);
+  if (key.length() >= 18 && key.compare(0, 18, "command-verbosity:") == 0)
+  {
+    map<string, Integer>::const_iterator i =
+        d_commandVerbosity.find(key.c_str() + 18);
+    if (i != d_commandVerbosity.end())
+    {
+      return nm->mkConst(Rational(i->second));
     }
     i = d_commandVerbosity.find("*");
-    if(i != d_commandVerbosity.end()) {
-      return SExpr((*i).second);
+    if (i != d_commandVerbosity.end())
+    {
+      return nm->mkConst(Rational(i->second));
     }
-    return SExpr(Integer(2));
+    return nm->mkConst(Rational(2));
   }
 
-  if(Dump.isOn("benchmark")) {
+  if (Dump.isOn("benchmark"))
+  {
     getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
   }
 
-  if(key == "command-verbosity") {
-    vector<SExpr> result;
-    SExpr defaultVerbosity;
-    for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
-        i != d_commandVerbosity.end();
-        ++i) {
-      vector<SExpr> v;
-      v.push_back(SExpr((*i).first));
-      v.push_back(SExpr((*i).second));
-      if((*i).first == "*") {
+  if (key == "command-verbosity")
+  {
+    vector<Node> result;
+    Node defaultVerbosity;
+    for (map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
+         i != d_commandVerbosity.end();
+         ++i)
+    {
+      // treat the command name as a variable name as opposed to a string
+      // constant to avoid printing double quotes around the name
+      Node name = nm->mkBoundVar(i->first, nm->integerType());
+      Node value = nm->mkConst(Rational(i->second));
+      if ((*i).first == "*")
+      {
         // put the default at the end of the SExpr
-        defaultVerbosity = SExpr(v);
-      } else {
-        result.push_back(SExpr(v));
+        defaultVerbosity = nm->mkNode(Kind::SEXPR, name, value);
+      }
+      else
+      {
+        result.push_back(nm->mkNode(Kind::SEXPR, name, value));
       }
     }
-    // put the default at the end of the SExpr
-    if(!defaultVerbosity.isAtom()) {
-      result.push_back(defaultVerbosity);
-    } else {
-      // ensure the default is always listed
-      vector<SExpr> v;
-      v.push_back(SExpr("*"));
-      v.push_back(SExpr(Integer(2)));
-      result.push_back(SExpr(v));
+    // ensure the default is always listed
+    if (defaultVerbosity.isNull())
+    {
+      defaultVerbosity = nm->mkNode(Kind::SEXPR,
+                                    nm->mkBoundVar("*", nm->integerType()),
+                                    nm->mkConst(Rational(2)));
     }
-    return SExpr(result);
+    result.push_back(defaultVerbosity);
+    return nm->mkNode(Kind::SEXPR, result);
   }
 
-  return SExpr::parseAtom(getOptions().getOption(key));
+  // parse atom string
+  std::string atom = getOptions().getOption(key);
+
+  if (atom == "true")
+  {
+    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
+  }
+  return nm->mkConst(String(atom));
 }
 
 Options& SmtEngine::getOptions() { return d_env->d_options; }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 744320950..dd0fe3a6e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -310,7 +310,7 @@ class CVC4_EXPORT SmtEngine
    * Get an aspect of the current SMT execution environment.
    * @throw OptionException
    */
-  CVC4::SExpr getOption(const std::string& key) const;
+  Node 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 14752f726..964e73fc0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -707,6 +707,7 @@ set(regress_0_tests
   regress0/nl/very-simple-unsat.smt2
   regress0/opt-abd-no-use.smt2
   regress0/options/invalid_dump.smt2
+  regress0/options/set-and-get-options.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2
new file mode 100644
index 000000000..478e3d523
--- /dev/null
+++ b/test/regress/regress0/options/set-and-get-options.smt2
@@ -0,0 +1,19 @@
+; EXPECT: ((* 2))
+; EXPECT: ((check-sat 1) (* 1))
+; EXPECT: true
+; EXPECT: false
+; EXPECT: 15
+; EXPECT: "SimplificationMode::NONE"
+
+(get-option :command-verbosity)
+(set-option :command-verbosity (* 1))
+(set-option :command-verbosity (check-sat 1))
+(get-option :command-verbosity)
+(set-option :check-models true)
+(get-option :check-models)
+(set-option :check-models false)
+(get-option :check-models)
+(set-option :dag-thresh 15)
+(get-option :dag-thresh)
+(set-option :simplification none)
+(get-option :simplification)