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/command.cpp | |
| 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/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 15 |
1 files changed, 7 insertions, 8 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 { |