diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 104 |
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); } |