diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 84 |
1 files changed, 53 insertions, 31 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e6361be9e..14b9ed0aa 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -29,7 +29,7 @@ #include "expr/expr_iomanip.h" #include "expr/node.h" #include "expr/symbol_manager.h" -#include "expr/type.h" +#include "expr/type_node.h" #include "options/options.h" #include "options/smt_options.h" #include "printer/printer.h" @@ -45,6 +45,43 @@ using namespace std; namespace CVC4 { +std::string sexprToString(api::Term sexpr) +{ + // if sexpr is a spec constant and not a string, return the result of calling + // Term::toString + if (sexpr.getKind() == api::CONST_BOOLEAN + || sexpr.getKind() == api::CONST_FLOATINGPOINT + || sexpr.getKind() == api::CONST_RATIONAL) + { + return sexpr.toString(); + } + + // if sexpr is a constant string, return the result of calling Term::toString. + // However, strip the surrounding quotes + if (sexpr.getKind() == api::CONST_STRING) + { + return sexpr.toString().substr(1, sexpr.toString().length() - 2); + } + + // if sexpr is not a spec constant, make sure it is an array of sub-sexprs + Assert(sexpr.getKind() == api::SEXPR); + + std::stringstream ss; + auto it = sexpr.begin(); + + // recursively print the sub-sexprs + ss << '(' << sexprToString(*it); + ++it; + while (it != sexpr.end()) + { + ss << ' ' << sexprToString(*it); + ++it; + } + ss << ')'; + + return ss.str(); +} + const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); const CommandInterrupted* CommandInterrupted::s_instance = @@ -137,11 +174,6 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) Command::Command() : d_commandStatus(nullptr), d_muted(false) {} -Command::Command(const api::Solver* solver) - : d_commandStatus(nullptr), d_muted(false) -{ -} - Command::Command(const Command& cmd) { d_commandStatus = @@ -1811,7 +1843,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2520,21 +2552,21 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out, /* class SetInfoCommand */ /* -------------------------------------------------------------------------- */ -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) +SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetInfoCommand::getFlag() const { return d_flag; } -SExpr SetInfoCommand::getSExpr() const { return d_sexpr; } +const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; } void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setInfo(d_flag, d_sexpr); + solver->setInfo(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { // As per SMT-LIB spec, silently accept unknown set-info keys d_commandStatus = CommandSuccess::instance(); @@ -2570,23 +2602,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - vector<SExpr> v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.emplace_back(solver->getSmtEngine()->getInfo(d_flag)); - stringstream ss; - if (d_flag == "all-options" || d_flag == "all-statistics") - { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); + std::vector<api::Term> v; + v.push_back(solver->mkString(":" + d_flag)); + v.push_back(solver->mkString(solver->getInfo(d_flag))); + d_result = sexprToString(solver->mkTerm(api::SEXPR, v)); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) - { - d_commandStatus = new CommandUnsupported(); - } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -2630,21 +2652,21 @@ void GetInfoCommand::toStream(std::ostream& out, /* class SetOptionCommand */ /* -------------------------------------------------------------------------- */ -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) +SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr) : d_flag(flag), d_sexpr(sexpr) { } std::string SetOptionCommand::getFlag() const { return d_flag; } -SExpr SetOptionCommand::getSExpr() const { return d_sexpr; } +const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; } void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->setOption(d_flag, d_sexpr); + solver->setOption(d_flag, d_sexpr); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } @@ -2682,7 +2704,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) d_result = solver->getOption(d_flag); d_commandStatus = CommandSuccess::instance(); } - catch (UnrecognizedOptionException&) + catch (api::CVC4ApiRecoverableException&) { d_commandStatus = new CommandUnsupported(); } |