From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Thu, 18 Mar 2021 18:33:47 +0000 (-0500) Subject: Eliminate more uses of SExpr. (#6149) X-Git-Tag: cvc5-1.0.0~2058 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2638e65d242fa9da99d038db07c4a2b75e8dfde3;p=cvc5.git Eliminate more uses of SExpr. (#6149) This PR eliminates all remaining uses of SExpr outside of statistics. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 4ccff9930..e87e6176b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -6229,7 +6229,7 @@ std::string Solver::getOption(const std::string& option) const { CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - SExpr res = d_smtEngine->getOption(option); + Node res = d_smtEngine->getOption(option); return res.toString(); //////// CVC4_API_TRY_CATCH_END; diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 001da12db..846bef5be 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -252,7 +252,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // "--tear-down-incremental incompatible with --incremental"); // } - // cmd.reset(new SetOptionCommand("incremental", SExpr(false))); + // cmd.reset(new SetOptionCommand("incremental", "false")); // cmd->setMuted(true); // pExecutor->doCommand(cmd); } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b7997cafa..c12c1efc6 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -538,7 +538,6 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { #include "parser/antlr_input.h" #include "parser/antlr_tracing.h" #include "parser/parser.h" -#include "util/integer.h" }/* @lexer::includes */ @@ -551,6 +550,7 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { #include "parser/antlr_tracing.h" #include "parser/parser.h" #include "smt/command.h" +#include "util/rational.h" namespace CVC4 { class Expr; diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 0449f13ce..a7fe65f67 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -34,7 +34,6 @@ namespace CVC4 { class Command; -class SExpr; namespace api { class Solver; diff --git a/src/printer/printer.h b/src/printer/printer.h index 06b263e51..17fd66848 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -25,7 +25,6 @@ #include "options/language.h" #include "smt/model.h" #include "util/result.h" -#include "util/sexpr.h" namespace CVC4 { diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 664bc2bf9..26ccf5821 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -245,7 +245,6 @@ class Smt2Printer : public CVC4::Printer TNode n, int toDepth, TypeNode tn) const; - void toStream(std::ostream& out, const SExpr& sexpr) const; void toStream(std::ostream& out, const DType& dt) const; /** * To stream model sort. This prints the appropriate output for type 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 values = solver->getValue(terms); Assert(values.size() == names.size()); - std::vector sexprs; + std::vector sexprs; for (size_t i = 0, nterms = terms.size(); i < nterms; i++) { - std::vector 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::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::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 result; - SExpr defaultVerbosity; - for(map::const_iterator i = d_commandVerbosity.begin(); - i != d_commandVerbosity.end(); - ++i) { - vector v; - v.push_back(SExpr((*i).first)); - v.push_back(SExpr((*i).second)); - if((*i).first == "*") { + if (key == "command-verbosity") + { + vector result; + Node defaultVerbosity; + for (map::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 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(true); + } + else if (atom == "false") + { + return nm->mkConst(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: diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 14752f726..964e73fc0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -707,6 +707,7 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/invalid_dump.smt2 + regress0/options/set-and-get-options.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2 new file mode 100644 index 000000000..478e3d523 --- /dev/null +++ b/test/regress/regress0/options/set-and-get-options.smt2 @@ -0,0 +1,19 @@ +; EXPECT: ((* 2)) +; EXPECT: ((check-sat 1) (* 1)) +; EXPECT: true +; EXPECT: false +; EXPECT: 15 +; EXPECT: "SimplificationMode::NONE" + +(get-option :command-verbosity) +(set-option :command-verbosity (* 1)) +(set-option :command-verbosity (check-sat 1)) +(get-option :command-verbosity) +(set-option :check-models true) +(get-option :check-models) +(set-option :check-models false) +(get-option :check-models) +(set-option :dag-thresh 15) +(get-option :dag-thresh) +(set-option :simplification none) +(get-option :simplification)