1 files changed, 44 insertions, 60 deletions

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);
 }