diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-03 04:28:45 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-03 10:28:45 +0000 |
commit | 6db84f6e373f9651af48df7b654e3992f68472ac (patch) | |
tree | 3c146a185ce575431ea7a63cf97a8e0bb1031c0b /src/smt | |
parent | c4709cb01356dd73fdd767d19af85b36ffd566c4 (diff) |
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.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 30 | ||||
-rw-r--r-- | src/smt/command.h | 16 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 104 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
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. * |