diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-18 13:33:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-18 13:33:47 -0500 |
commit | 2638e65d242fa9da99d038db07c4a2b75e8dfde3 (patch) | |
tree | a3be9ecd4d807957e8b0755368707158ca2b79f0 /src/smt | |
parent | d52bc44199583e3c06816c1d30f61e8075820c1b (diff) |
Eliminate more uses of SExpr. (#6149)
This PR eliminates all remaining uses of SExpr outside of statistics.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 15 | ||||
-rw-r--r-- | src/smt/command.h | 6 | ||||
-rw-r--r-- | src/smt/env.h | 1 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 106 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
5 files changed, 80 insertions, 50 deletions
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: |