diff options
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 128 |
1 files changed, 53 insertions, 75 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 68c776536..f1490e2f9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -28,10 +28,10 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/node.h" +#include "expr/symbol_manager.h" #include "expr/type.h" #include "options/options.h" #include "options/smt_options.h" -#include "parser/symbol_manager.h" #include "printer/printer.h" #include "proof/unsat_core.h" #include "smt/dump.h" @@ -176,9 +176,7 @@ bool Command::interrupted() const && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL; } -void Command::invoke(api::Solver* solver, - parser::SymbolManager* sm, - std::ostream& out) +void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out) { invoke(solver, sm); if (!(isMuted() && ok())) @@ -218,7 +216,7 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const EmptyCommand::EmptyCommand(std::string name) : d_name(name) {} std::string EmptyCommand::getName() const { return d_name; } -void EmptyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void EmptyCommand::invoke(api::Solver* solver, SymbolManager* sm) { /* empty commands have no implementation */ d_commandStatus = CommandSuccess::instance(); @@ -241,14 +239,14 @@ void EmptyCommand::toStream(std::ostream& out, EchoCommand::EchoCommand(std::string output) : d_output(output) {} std::string EchoCommand::getOutput() const { return d_output; } -void EchoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm) { /* we don't have an output stream here, nothing to do */ d_commandStatus = CommandSuccess::instance(); } void EchoCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, std::ostream& out) { out << d_output << std::endl; @@ -281,7 +279,7 @@ AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore) } api::Term AssertCommand::getTerm() const { return d_term; } -void AssertCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -317,7 +315,7 @@ void AssertCommand::toStream(std::ostream& out, /* class PushCommand */ /* -------------------------------------------------------------------------- */ -void PushCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void PushCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -349,7 +347,7 @@ void PushCommand::toStream(std::ostream& out, /* class PopCommand */ /* -------------------------------------------------------------------------- */ -void PopCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void PopCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -386,7 +384,7 @@ CheckSatCommand::CheckSatCommand() : d_term() {} CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {} api::Term CheckSatCommand::getTerm() const { return d_term; } -void CheckSatCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm) { Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~" << std::endl; @@ -454,8 +452,7 @@ const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const return d_terms; } -void CheckSatAssumingCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void CheckSatAssumingCommand::invoke(api::Solver* solver, SymbolManager* sm) { Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms << " )~" << std::endl; @@ -520,7 +517,7 @@ QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore) } api::Term QueryCommand::getTerm() const { return d_term; } -void QueryCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -577,8 +574,7 @@ DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id, api::Term DeclareSygusVarCommand::getVar() const { return d_var; } api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; } -void DeclareSygusVarCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void DeclareSygusVarCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -633,7 +629,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; } const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } -void SynthFunCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -672,8 +668,7 @@ SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t) { } -void SygusConstraintCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -724,8 +719,7 @@ SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv, { } -void SygusInvConstraintCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void SygusInvConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -771,7 +765,7 @@ void SygusInvConstraintCommand::toStream(std::ostream& out, /* class CheckSynthCommand */ /* -------------------------------------------------------------------------- */ -void CheckSynthCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -839,7 +833,7 @@ void CheckSynthCommand::toStream(std::ostream& out, /* class ResetCommand */ /* -------------------------------------------------------------------------- */ -void ResetCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -867,8 +861,7 @@ void ResetCommand::toStream(std::ostream& out, /* class ResetAssertionsCommand */ /* -------------------------------------------------------------------------- */ -void ResetAssertionsCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void ResetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -903,7 +896,7 @@ void ResetAssertionsCommand::toStream(std::ostream& out, /* class QuitCommand */ /* -------------------------------------------------------------------------- */ -void QuitCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm) { Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); @@ -926,7 +919,7 @@ void QuitCommand::toStream(std::ostream& out, CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {} std::string CommentCommand::getComment() const { return d_comment; } -void CommentCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void CommentCommand::invoke(api::Solver* solver, SymbolManager* sm) { Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); @@ -962,7 +955,7 @@ void CommandSequence::addCommand(Command* cmd) } void CommandSequence::clear() { d_commandSequence.clear(); } -void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm) +void CommandSequence::invoke(api::Solver* solver, SymbolManager* sm) { for (; d_index < d_commandSequence.size(); ++d_index) { @@ -981,7 +974,7 @@ void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm) } void CommandSequence::invoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, std::ostream& out) { for (; d_index < d_commandSequence.size(); ++d_index) @@ -1096,8 +1089,7 @@ void DeclareFunctionCommand::setPrintInModel(bool p) d_printInModelSetByUser = true; } -void DeclareFunctionCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -1138,7 +1130,7 @@ DeclareSortCommand::DeclareSortCommand(const std::string& id, size_t DeclareSortCommand::getArity() const { return d_arity; } api::Sort DeclareSortCommand::getSort() const { return d_sort; } -void DeclareSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -1184,7 +1176,7 @@ const std::vector<api::Sort>& DefineSortCommand::getParameters() const } api::Sort DefineSortCommand::getSort() const { return d_sort; } -void DefineSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void DefineSortCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -1245,8 +1237,7 @@ const std::vector<api::Term>& DefineFunctionCommand::getFormals() const } api::Term DefineFunctionCommand::getFormula() const { return d_formula; } -void DefineFunctionCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1301,8 +1292,7 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand( { } -void DefineNamedFunctionCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void DefineNamedFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { this->DefineFunctionCommand::invoke(solver, sm); if (!d_func.isNull() && d_func.getSort().isBoolean()) @@ -1374,8 +1364,7 @@ const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const return d_formulas; } -void DefineFunctionRecCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1427,7 +1416,7 @@ DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort) api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; } api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; } -void DeclareHeapCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void DeclareHeapCommand::invoke(api::Solver* solver, SymbolManager* sm) { solver->declareSeparationHeap(d_locSort, d_dataSort); } @@ -1485,8 +1474,7 @@ SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr, { } -void SetUserAttributeCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1531,7 +1519,7 @@ void SetUserAttributeCommand::toStream(std::ostream& out, SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {} api::Term SimplifyCommand::getTerm() const { return d_term; } -void SimplifyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1598,7 +1586,7 @@ const std::vector<api::Term>& GetValueCommand::getTerms() const { return d_terms; } -void GetValueCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1664,8 +1652,7 @@ void GetValueCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAssignmentCommand::GetAssignmentCommand() {} -void GetAssignmentCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1735,7 +1722,7 @@ void GetAssignmentCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetModelCommand::GetModelCommand() : d_result(nullptr) {} -void GetModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1796,7 +1783,7 @@ void GetModelCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ BlockModelCommand::BlockModelCommand() {} -void BlockModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1850,8 +1837,7 @@ const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const { return d_terms; } -void BlockModelValuesCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1897,7 +1883,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetProofCommand::GetProofCommand() {} -void GetProofCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm) { Unimplemented() << "Unimplemented get-proof\n"; } @@ -1923,8 +1909,7 @@ void GetProofCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {} -void GetInstantiationsCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -1976,8 +1961,7 @@ void GetInstantiationsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {} -void GetSynthSolutionCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void GetSynthSolutionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2047,7 +2031,7 @@ const api::Grammar* GetInterpolCommand::getGrammar() const api::Term GetInterpolCommand::getResult() const { return d_result; } -void GetInterpolCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2138,7 +2122,7 @@ const api::Grammar* GetAbductCommand::getGrammar() const std::string GetAbductCommand::getAbductName() const { return d_name; } api::Term GetAbductCommand::getResult() const { return d_result; } -void GetAbductCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2215,7 +2199,7 @@ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand( api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; } bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; } void GetQuantifierEliminationCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) + SymbolManager* sm) { try { @@ -2280,8 +2264,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out, GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {} -void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2341,7 +2324,7 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetUnsatCoreCommand::GetUnsatCoreCommand() {} -void GetUnsatCoreCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2406,8 +2389,7 @@ void GetUnsatCoreCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAssertionsCommand::GetAssertionsCommand() {} -void GetAssertionsCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2473,8 +2455,7 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const return d_status; } -void SetBenchmarkStatusCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void SetBenchmarkStatusCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2525,8 +2506,7 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) } std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; } -void SetBenchmarkLogicCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void SetBenchmarkLogicCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2568,7 +2548,7 @@ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) std::string SetInfoCommand::getFlag() const { return d_flag; } SExpr SetInfoCommand::getSExpr() const { return d_sexpr; } -void SetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2607,7 +2587,7 @@ void SetInfoCommand::toStream(std::ostream& out, GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {} std::string GetInfoCommand::getFlag() const { return d_flag; } -void GetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2678,7 +2658,7 @@ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) std::string SetOptionCommand::getFlag() const { return d_flag; } SExpr SetOptionCommand::getSExpr() const { return d_sexpr; } -void SetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2716,7 +2696,7 @@ void SetOptionCommand::toStream(std::ostream& out, GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {} std::string GetOptionCommand::getFlag() const { return d_flag; } -void GetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) +void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { @@ -2773,8 +2753,7 @@ SetExpressionNameCommand::SetExpressionNameCommand(api::Term term, { } -void SetExpressionNameCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm) { solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name); d_commandStatus = CommandSuccess::instance(); @@ -2822,8 +2801,7 @@ const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const return d_datatypes; } -void DatatypeDeclarationCommand::invoke(api::Solver* solver, - parser::SymbolManager* sm) +void DatatypeDeclarationCommand::invoke(api::Solver* solver, SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } |