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.

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index ab792f6fe5ad9ad6dfe849ee657ef12c37ec110b..66dcdbfb2b02391713adef21463692808d46950a 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -346,9 +346,9 @@ void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
 
 void AstPrinter::toStreamCmdSetInfo(std::ostream& out,
                                     const std::string& flag,
-                                    SExpr sexpr) const
+                                    const std::string& value) const
 {
-  out << "SetInfo(" << flag << ", " << sexpr << ')' << std::endl;
+  out << "SetInfo(" << flag << ", " << value << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
@@ -359,9 +359,9 @@ void AstPrinter::toStreamCmdGetInfo(std::ostream& out,
 
 void AstPrinter::toStreamCmdSetOption(std::ostream& out,
                                       const std::string& flag,
-                                      SExpr sexpr) const
+                                      const std::string& value) const
 {
-  out << "SetOption(" << flag << ", " << sexpr << ')' << std::endl;
+  out << "SetOption(" << flag << ", " << value << ')' << std::endl;
 }
 
 void AstPrinter::toStreamCmdGetOption(std::ostream& out,

diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 732933bb4b14836af020654ea4c6da2608794d90..be1529b04f7a0faf71e1f45b518963b0b39bbb04 100644 (file)
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -124,7 +124,7 @@ class AstPrinter : public CVC4::Printer
   /** Print set-info command */
   void toStreamCmdSetInfo(std::ostream& out,
                           const std::string& flag,
-                          SExpr sexpr) const override;
+                          const std::string& value) const override;
 
   /** Print get-info command */
   void toStreamCmdGetInfo(std::ostream& out,
@@ -133,7 +133,7 @@ class AstPrinter : public CVC4::Printer
   /** Print set-option command */
   void toStreamCmdSetOption(std::ostream& out,
                             const std::string& flag,
-                            SExpr sexpr) const override;
+                            const std::string& value) const override;
 
   /** Print get-option command */
   void toStreamCmdGetOption(std::ostream& out,

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 82798d074ce9e57f7f27967d3714891105217d2b..7ac2da40bce187f06df421ac7f91f7a6abc4b7ab 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1420,13 +1420,9 @@ void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out,
 
 void CvcPrinter::toStreamCmdSetInfo(std::ostream& out,
                                     const std::string& flag,
-                                    SExpr sexpr) const
+                                    const std::string& value) const
 {
-  out << "% (set-info " << flag << ' ';
-  OutputLanguage language =
-      d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
-  SExpr::toStream(out, sexpr, language);
-  out << ')' << std::endl;
+  out << "% (set-info " << flag << ' ' << value << ')' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
@@ -1437,11 +1433,9 @@ void CvcPrinter::toStreamCmdGetInfo(std::ostream& out,
 
 void CvcPrinter::toStreamCmdSetOption(std::ostream& out,
                                       const std::string& flag,
-                                      SExpr sexpr) const
+                                      const std::string& value) const
 {
-  out << "OPTION \"" << flag << "\" ";
-  SExpr::toStream(out, sexpr, language::output::LANG_CVC4);
-  out << ';' << std::endl;
+  out << "OPTION \"" << flag << "\" " << value << ';' << std::endl;
 }
 
 void CvcPrinter::toStreamCmdGetOption(std::ostream& out,

diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 58e47dbac9fa92bfaf9cf4472d968fd6c81d837b..ab18d62de5f9ac40586a7cd1b980b33086f9675d 100644 (file)
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -125,7 +125,7 @@ class CvcPrinter : public CVC4::Printer
   /** Print set-info command */
   void toStreamCmdSetInfo(std::ostream& out,
                           const std::string& flag,
-                          SExpr sexpr) const override;
+                          const std::string& value) const override;
 
   /** Print get-info command */
   void toStreamCmdGetInfo(std::ostream& out,
@@ -134,7 +134,7 @@ class CvcPrinter : public CVC4::Printer
   /** Print set-option command */
   void toStreamCmdSetOption(std::ostream& out,
                             const std::string& flag,
-                            SExpr sexpr) const override;
+                            const std::string& value) const override;
 
   /** Print get-option command */
   void toStreamCmdGetOption(std::ostream& out,

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 4e464f8299f4caf58da0609f3036da25b3dbbde8..2d5ae58cd9023518518ef76fde3e8309888472e4 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -388,7 +388,7 @@ void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
 
 void Printer::toStreamCmdSetInfo(std::ostream& out,
                                  const std::string& flag,
-                                 SExpr sexpr) const
+                                 const std::string& value) const
 {
   printUnknownCommand(out, "set-info");
 }
@@ -401,7 +401,7 @@ void Printer::toStreamCmdGetInfo(std::ostream& out,
 
 void Printer::toStreamCmdSetOption(std::ostream& out,
                                    const std::string& flag,
-                                   SExpr sexpr) const
+                                   const std::string& value) const
 {
   printUnknownCommand(out, "set-option");
 }

diff --git a/src/printer/printer.h b/src/printer/printer.h
index f17029618b902116f245e184893e3849e0a1ecaf..0a5ed1eac0275dc3ba8978520ba9831e89eab189 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -217,7 +217,7 @@ class Printer
   /** Print set-info command */
   virtual void toStreamCmdSetInfo(std::ostream& out,
                                   const std::string& flag,
-                                  SExpr sexpr) const;
+                                  const std::string& value) const;
 
   /** Print get-info command */
   virtual void toStreamCmdGetInfo(std::ostream& out,
@@ -226,7 +226,7 @@ class Printer
   /** Print set-option command */
   virtual void toStreamCmdSetOption(std::ostream& out,
                                     const std::string& flag,
-                                    SExpr sexpr) const;
+                                    const std::string& value) const;
 
   /** Print get-option command */
   virtual void toStreamCmdGetOption(std::ostream& out,

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8c122f26d098d94efeb5d1da5367ee6fac80a355..c3ac36b5e29d8b49c1dd1f0fb1ad2ce3b51c02ff 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -50,8 +50,6 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-static OutputLanguage variantToLanguage(Variant v);
-
 /** returns whether the variant is smt-lib 2.6 or greater */
 bool isVariant_2_6(Variant v) { return v == smt2_6_variant; }
 
@@ -1808,11 +1806,9 @@ void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out,
 
 void Smt2Printer::toStreamCmdSetInfo(std::ostream& out,
                                      const std::string& flag,
-                                     SExpr sexpr) const
+                                     const std::string& value) const
 {
-  out << "(set-info :" << flag << ' ';
-  SExpr::toStream(out, sexpr, variantToLanguage(d_variant));
-  out << ')' << std::endl;
+  out << "(set-info :" << flag << ' ' << value << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
@@ -1823,11 +1819,9 @@ void Smt2Printer::toStreamCmdGetInfo(std::ostream& out,
 
 void Smt2Printer::toStreamCmdSetOption(std::ostream& out,
                                        const std::string& flag,
-                                       SExpr sexpr) const
+                                       const std::string& value) const
 {
-  out << "(set-option :" << flag << ' ';
-  SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5);
-  out << ')' << std::endl;
+  out << "(set-option :" << flag << ' ' << value << ')' << std::endl;
 }
 
 void Smt2Printer::toStreamCmdGetOption(std::ostream& out,
@@ -2233,16 +2227,6 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v)
   return false;
 }
 
-static OutputLanguage variantToLanguage(Variant variant)
-{
-  switch(variant) {
-  case smt2_0_variant:
-    return language::output::LANG_SMTLIB_V2_0;
-  case no_variant:
-  default: return language::output::LANG_SMTLIB_V2_6;
-  }
-}
-
 }/* CVC4::printer::smt2 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 8934967b952a736316e1dc0d6b267922e746c3c3..4ba0d6cadc956426519820d9e0b00bc4b369971e 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -178,7 +178,7 @@ class Smt2Printer : public CVC4::Printer
   /** Print set-info command */
   void toStreamCmdSetInfo(std::ostream& out,
                           const std::string& flag,
-                          SExpr sexpr) const override;
+                          const std::string& value) const override;
 
   /** Print get-info command */
   void toStreamCmdGetInfo(std::ostream& out,
@@ -187,7 +187,7 @@ class Smt2Printer : public CVC4::Printer
   /** Print set-option command */
   void toStreamCmdSetOption(std::ostream& out,
                             const std::string& flag,
-                            SExpr sexpr) const override;
+                            const std::string& value) const override;
 
   /** Print get-option command */
   void toStreamCmdGetOption(std::ostream& out,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f10191c7521c981154723c899b575e80d38479d0..9227c37031a2adb3c19738b99f7064f97673470c 100644 (file)
--- 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 a88b7e022e0e32b1920a1ef5601585f01b377978..c11012944aa3166550f84040f1c5d6a452d90d82 100644 (file)
--- 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 ed5e73d5d81ba1551b6ceae3dc06e8fcbe6e3946..80d7b96fabac6e7b1cfaedf21cd1b8f9029fb050 100644 (file)
--- 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 53a5b7f2f78b25585d97286bb2d2f9012e374b76..8974e5e60e4e1623fcf49aba7d30f5eb2954f586 100644 (file)
--- 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.
    *

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 6ce561b2dc922c0587ec1afd8249549407a1e986..96a26059d56f0cc0978fbd8ea22884664704aaec 100644 (file)
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   Assert (!query.isNull());
   initializeSubsolver(checker);
   // also set the options
-  checker->setOption("sygus-rr-synth-input", false);
+  checker->setOption("sygus-rr-synth-input", "false");
   checker->setOption("input-language", "smt2");
   // Convert bound variables to skolems. This ensures the satisfiability
   // check is ground.

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 8b741b6d7ec94a59db1c7632a02327ce2f8a8cc8..9b4a034736043a6d21ca23ef39e4648c70ba4531 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -237,9 +237,9 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
                       options::sygusRepairConstTimeout.wasSetByUser(),
                       options::sygusRepairConstTimeout());
   // renable options disabled by sygus
-  repcChecker->setOption("miniscope-quant", true);
-  repcChecker->setOption("miniscope-quant-fv", true);
-  repcChecker->setOption("quant-split", true);
+  repcChecker->setOption("miniscope-quant", "true");
+  repcChecker->setOption("miniscope-quant-fv", "true");
+  repcChecker->setOption("quant-split", "true");
   repcChecker->assertFormula(fo_body);
   // check satisfiability
   Result r = repcChecker->checkSat();

diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
index 5e5b52d3e0e071595213689b5898d9c655b6634a..4c8834c8d5d295fb77f780c931857986b9b07e43 100644 (file)
--- a/test/unit/theory/theory_arith_white.cpp
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -41,7 +41,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit
   void SetUp() override
   {
     TestSmtNoFinishInit::SetUp();
-    d_smtEngine->setOption("incremental", CVC4::SExpr(false));
+    d_smtEngine->setOption("incremental", "false");
     d_smtEngine->finishInit();
     d_context = d_smtEngine->getContext();
     d_user_context = d_smtEngine->getUserContext();

diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index c07f2c40229cd1f9e78d3ccad4015420c84a7906..976724c8ef4bd29f80941047e7f9b55be5eacdd3 100644 (file)
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -43,8 +43,8 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
 {
   d_smtEngine->setLogic("QF_BV");
 
-  d_smtEngine->setOption("bitblast", SExpr("eager"));
-  d_smtEngine->setOption("incremental", SExpr("false"));
+  d_smtEngine->setOption("bitblast", "eager");
+  d_smtEngine->setOption("incremental", "false");
   // Notice that this unit test uses the theory engine of a created SMT
   // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized
   // via the following call, which constructs its underlying theory engine.
@@ -72,7 +72,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
 
 TEST_F(TestTheoryWhiteBv, mkUmulo)
 {
-  d_smtEngine->setOption("incremental", SExpr("true"));
+  d_smtEngine->setOption("incremental", "true");
   for (uint32_t w = 1; w < 16; ++w)
   {
     d_smtEngine->push();

diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index 5c222d2c1ac90d023cccecdac4b8f27aea6f63e1..b5996a68410d4f5fc8d144d3b508d834898b728c 100644 (file)
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -35,8 +35,8 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
   void SetUp() override
   {
     TestSmtNoFinishInit::SetUp();
-    d_smtEngine->setOption("cegqi-full", CVC4::SExpr(true));
-    d_smtEngine->setOption("produce-models", CVC4::SExpr(true));
+    d_smtEngine->setOption("cegqi-full", "true");
+    d_smtEngine->setOption("produce-models", "true");
     d_smtEngine->finishInit();
 
     d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4));