diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 189 |
1 files changed, 84 insertions, 105 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index b33fe5ad9..68c776536 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -31,6 +31,7 @@ #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" @@ -175,9 +176,11 @@ bool Command::interrupted() const && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL; } -void Command::invoke(api::Solver* solver, std::ostream& out) +void Command::invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) { - invoke(solver); + invoke(solver, sm); if (!(isMuted() && ok())) { printResult( @@ -215,7 +218,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) +void EmptyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { /* empty commands have no implementation */ d_commandStatus = CommandSuccess::instance(); @@ -226,7 +229,6 @@ std::string EmptyCommand::getCommandName() const { return "empty"; } void EmptyCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -239,13 +241,15 @@ 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) +void EchoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { /* we don't have an output stream here, nothing to do */ d_commandStatus = CommandSuccess::instance(); } -void EchoCommand::invoke(api::Solver* solver, std::ostream& out) +void EchoCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) { out << d_output << std::endl; Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~" @@ -261,7 +265,6 @@ std::string EchoCommand::getCommandName() const { return "echo"; } void EchoCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -278,7 +281,7 @@ AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore) } api::Term AssertCommand::getTerm() const { return d_term; } -void AssertCommand::invoke(api::Solver* solver) +void AssertCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -304,7 +307,6 @@ std::string AssertCommand::getCommandName() const { return "assert"; } void AssertCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -315,7 +317,7 @@ void AssertCommand::toStream(std::ostream& out, /* class PushCommand */ /* -------------------------------------------------------------------------- */ -void PushCommand::invoke(api::Solver* solver) +void PushCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -337,7 +339,6 @@ std::string PushCommand::getCommandName() const { return "push"; } void PushCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -348,7 +349,7 @@ void PushCommand::toStream(std::ostream& out, /* class PopCommand */ /* -------------------------------------------------------------------------- */ -void PopCommand::invoke(api::Solver* solver) +void PopCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -370,7 +371,6 @@ std::string PopCommand::getCommandName() const { return "pop"; } void PopCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -386,7 +386,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) +void CheckSatCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~" << std::endl; @@ -428,7 +428,6 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; } void CheckSatCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -455,7 +454,8 @@ const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const return d_terms; } -void CheckSatAssumingCommand::invoke(api::Solver* solver) +void CheckSatAssumingCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms << " )~" << std::endl; @@ -503,7 +503,6 @@ std::string CheckSatAssumingCommand::getCommandName() const void CheckSatAssumingCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -521,7 +520,7 @@ QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore) } api::Term QueryCommand::getTerm() const { return d_term; } -void QueryCommand::invoke(api::Solver* solver) +void QueryCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -558,7 +557,6 @@ std::string QueryCommand::getCommandName() const { return "query"; } void QueryCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -579,7 +577,8 @@ 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) +void DeclareSygusVarCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -596,7 +595,6 @@ std::string DeclareSygusVarCommand::getCommandName() const void DeclareSygusVarCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -635,7 +633,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; } const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } -void SynthFunCommand::invoke(api::Solver* solver) +void SynthFunCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -653,7 +651,6 @@ std::string SynthFunCommand::getCommandName() const void SynthFunCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -675,7 +672,8 @@ SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t) { } -void SygusConstraintCommand::invoke(api::Solver* solver) +void SygusConstraintCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -702,7 +700,6 @@ std::string SygusConstraintCommand::getCommandName() const void SygusConstraintCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -727,7 +724,8 @@ SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv, { } -void SygusInvConstraintCommand::invoke(api::Solver* solver) +void SygusInvConstraintCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -758,7 +756,6 @@ std::string SygusInvConstraintCommand::getCommandName() const void SygusInvConstraintCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -774,7 +771,7 @@ void SygusInvConstraintCommand::toStream(std::ostream& out, /* class CheckSynthCommand */ /* -------------------------------------------------------------------------- */ -void CheckSynthCommand::invoke(api::Solver* solver) +void CheckSynthCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -832,7 +829,6 @@ std::string CheckSynthCommand::getCommandName() const { return "check-synth"; } void CheckSynthCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -843,7 +839,7 @@ void CheckSynthCommand::toStream(std::ostream& out, /* class ResetCommand */ /* -------------------------------------------------------------------------- */ -void ResetCommand::invoke(api::Solver* solver) +void ResetCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -861,7 +857,6 @@ std::string ResetCommand::getCommandName() const { return "reset"; } void ResetCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -872,7 +867,8 @@ void ResetCommand::toStream(std::ostream& out, /* class ResetAssertionsCommand */ /* -------------------------------------------------------------------------- */ -void ResetAssertionsCommand::invoke(api::Solver* solver) +void ResetAssertionsCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -897,7 +893,6 @@ std::string ResetAssertionsCommand::getCommandName() const void ResetAssertionsCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -908,7 +903,7 @@ void ResetAssertionsCommand::toStream(std::ostream& out, /* class QuitCommand */ /* -------------------------------------------------------------------------- */ -void QuitCommand::invoke(api::Solver* solver) +void QuitCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); @@ -919,7 +914,6 @@ std::string QuitCommand::getCommandName() const { return "exit"; } void QuitCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -932,7 +926,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) +void CommentCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); @@ -943,7 +937,6 @@ std::string CommentCommand::getCommandName() const { return "comment"; } void CommentCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -969,11 +962,11 @@ void CommandSequence::addCommand(Command* cmd) } void CommandSequence::clear() { d_commandSequence.clear(); } -void CommandSequence::invoke(api::Solver* solver) +void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm) { for (; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(solver); + d_commandSequence[d_index]->invoke(solver, sm); if (!d_commandSequence[d_index]->ok()) { // abort execution @@ -987,11 +980,13 @@ void CommandSequence::invoke(api::Solver* solver) d_commandStatus = CommandSuccess::instance(); } -void CommandSequence::invoke(api::Solver* solver, std::ostream& out) +void CommandSequence::invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) { for (; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(solver, out); + d_commandSequence[d_index]->invoke(solver, sm, out); if (!d_commandSequence[d_index]->ok()) { // abort execution @@ -1040,7 +1035,6 @@ std::string CommandSequence::getCommandName() const { return "sequence"; } void CommandSequence::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1054,7 +1048,6 @@ void CommandSequence::toStream(std::ostream& out, void DeclarationSequence::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1103,7 +1096,8 @@ void DeclareFunctionCommand::setPrintInModel(bool p) d_printInModelSetByUser = true; } -void DeclareFunctionCommand::invoke(api::Solver* solver) +void DeclareFunctionCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -1124,7 +1118,6 @@ std::string DeclareFunctionCommand::getCommandName() const void DeclareFunctionCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1145,7 +1138,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) +void DeclareSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -1162,7 +1155,6 @@ std::string DeclareSortCommand::getCommandName() const void DeclareSortCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1192,7 +1184,7 @@ const std::vector<api::Sort>& DefineSortCommand::getParameters() const } api::Sort DefineSortCommand::getSort() const { return d_sort; } -void DefineSortCommand::invoke(api::Solver* solver) +void DefineSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -1206,7 +1198,6 @@ std::string DefineSortCommand::getCommandName() const { return "define-sort"; } void DefineSortCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1254,7 +1245,8 @@ const std::vector<api::Term>& DefineFunctionCommand::getFormals() const } api::Term DefineFunctionCommand::getFormula() const { return d_formula; } -void DefineFunctionCommand::invoke(api::Solver* solver) +void DefineFunctionCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -1283,7 +1275,6 @@ std::string DefineFunctionCommand::getCommandName() const void DefineFunctionCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1310,9 +1301,10 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand( { } -void DefineNamedFunctionCommand::invoke(api::Solver* solver) +void DefineNamedFunctionCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { - this->DefineFunctionCommand::invoke(solver); + this->DefineFunctionCommand::invoke(solver, sm); if (!d_func.isNull() && d_func.getSort().isBoolean()) { solver->getSmtEngine()->addToAssignment(d_func.getExpr()); @@ -1328,7 +1320,6 @@ Command* DefineNamedFunctionCommand::clone() const void DefineNamedFunctionCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1383,7 +1374,8 @@ const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const return d_formulas; } -void DefineFunctionRecCommand::invoke(api::Solver* solver) +void DefineFunctionRecCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -1408,7 +1400,6 @@ std::string DefineFunctionRecCommand::getCommandName() const void DefineFunctionRecCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1436,7 +1427,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) +void DeclareHeapCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { solver->declareSeparationHeap(d_locSort, d_dataSort); } @@ -1494,7 +1485,8 @@ SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr, { } -void SetUserAttributeCommand::invoke(api::Solver* solver) +void SetUserAttributeCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -1526,7 +1518,6 @@ std::string SetUserAttributeCommand::getCommandName() const void SetUserAttributeCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1540,7 +1531,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) +void SimplifyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -1581,7 +1572,6 @@ std::string SimplifyCommand::getCommandName() const { return "simplify"; } void SimplifyCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1608,7 +1598,7 @@ const std::vector<api::Term>& GetValueCommand::getTerms() const { return d_terms; } -void GetValueCommand::invoke(api::Solver* solver) +void GetValueCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -1662,7 +1652,6 @@ std::string GetValueCommand::getCommandName() const { return "get-value"; } void GetValueCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1675,7 +1664,8 @@ void GetValueCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAssignmentCommand::GetAssignmentCommand() {} -void GetAssignmentCommand::invoke(api::Solver* solver) +void GetAssignmentCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -1734,7 +1724,6 @@ std::string GetAssignmentCommand::getCommandName() const void GetAssignmentCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1746,7 +1735,7 @@ void GetAssignmentCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetModelCommand::GetModelCommand() : d_result(nullptr) {} -void GetModelCommand::invoke(api::Solver* solver) +void GetModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -1796,7 +1785,6 @@ std::string GetModelCommand::getCommandName() const { return "get-model"; } void GetModelCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1808,7 +1796,7 @@ void GetModelCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ BlockModelCommand::BlockModelCommand() {} -void BlockModelCommand::invoke(api::Solver* solver) +void BlockModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -1839,7 +1827,6 @@ std::string BlockModelCommand::getCommandName() const { return "block-model"; } void BlockModelCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1863,7 +1850,8 @@ const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const { return d_terms; } -void BlockModelValuesCommand::invoke(api::Solver* solver) +void BlockModelValuesCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -1897,7 +1885,6 @@ std::string BlockModelValuesCommand::getCommandName() const void BlockModelValuesCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1910,7 +1897,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetProofCommand::GetProofCommand() {} -void GetProofCommand::invoke(api::Solver* solver) +void GetProofCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { Unimplemented() << "Unimplemented get-proof\n"; } @@ -1925,7 +1912,6 @@ std::string GetProofCommand::getCommandName() const { return "get-proof"; } void GetProofCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1937,7 +1923,8 @@ void GetProofCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {} -void GetInstantiationsCommand::invoke(api::Solver* solver) +void GetInstantiationsCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -1978,7 +1965,6 @@ std::string GetInstantiationsCommand::getCommandName() const void GetInstantiationsCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -1990,7 +1976,8 @@ void GetInstantiationsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {} -void GetSynthSolutionCommand::invoke(api::Solver* solver) +void GetSynthSolutionCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -2030,7 +2017,6 @@ std::string GetSynthSolutionCommand::getCommandName() const void GetSynthSolutionCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2061,7 +2047,7 @@ const api::Grammar* GetInterpolCommand::getGrammar() const api::Term GetInterpolCommand::getResult() const { return d_result; } -void GetInterpolCommand::invoke(api::Solver* solver) +void GetInterpolCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2120,7 +2106,6 @@ std::string GetInterpolCommand::getCommandName() const void GetInterpolCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2153,7 +2138,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) +void GetAbductCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2206,7 +2191,6 @@ std::string GetAbductCommand::getCommandName() const { return "get-abduct"; } void GetAbductCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2230,7 +2214,8 @@ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand( api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; } bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; } -void GetQuantifierEliminationCommand::invoke(api::Solver* solver) +void GetQuantifierEliminationCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -2282,7 +2267,6 @@ std::string GetQuantifierEliminationCommand::getCommandName() const void GetQuantifierEliminationCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2296,7 +2280,8 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out, GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {} -void GetUnsatAssumptionsCommand::invoke(api::Solver* solver) +void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -2345,7 +2330,6 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const void GetUnsatAssumptionsCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2357,7 +2341,7 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetUnsatCoreCommand::GetUnsatCoreCommand() {} -void GetUnsatCoreCommand::invoke(api::Solver* solver) +void GetUnsatCoreCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2411,7 +2395,6 @@ std::string GetUnsatCoreCommand::getCommandName() const void GetUnsatCoreCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2423,7 +2406,8 @@ void GetUnsatCoreCommand::toStream(std::ostream& out, /* -------------------------------------------------------------------------- */ GetAssertionsCommand::GetAssertionsCommand() {} -void GetAssertionsCommand::invoke(api::Solver* solver) +void GetAssertionsCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -2469,7 +2453,6 @@ std::string GetAssertionsCommand::getCommandName() const void GetAssertionsCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2490,7 +2473,8 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const return d_status; } -void SetBenchmarkStatusCommand::invoke(api::Solver* solver) +void SetBenchmarkStatusCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -2517,7 +2501,6 @@ std::string SetBenchmarkStatusCommand::getCommandName() const void SetBenchmarkStatusCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2542,7 +2525,8 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) } std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; } -void SetBenchmarkLogicCommand::invoke(api::Solver* solver) +void SetBenchmarkLogicCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { try { @@ -2567,7 +2551,6 @@ std::string SetBenchmarkLogicCommand::getCommandName() const void SetBenchmarkLogicCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2585,7 +2568,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) +void SetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2612,7 +2595,6 @@ std::string SetInfoCommand::getCommandName() const { return "set-info"; } void SetInfoCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2625,7 +2607,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) +void GetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2679,7 +2661,6 @@ std::string GetInfoCommand::getCommandName() const { return "get-info"; } void GetInfoCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2697,7 +2678,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) +void SetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2723,7 +2704,6 @@ std::string SetOptionCommand::getCommandName() const { return "set-option"; } void SetOptionCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2736,7 +2716,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) +void GetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm) { try { @@ -2777,7 +2757,6 @@ std::string GetOptionCommand::getCommandName() const { return "get-option"; } void GetOptionCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2794,7 +2773,8 @@ SetExpressionNameCommand::SetExpressionNameCommand(api::Term term, { } -void SetExpressionNameCommand::invoke(api::Solver* solver) +void SetExpressionNameCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name); d_commandStatus = CommandSuccess::instance(); @@ -2813,7 +2793,6 @@ std::string SetExpressionNameCommand::getCommandName() const void SetExpressionNameCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { @@ -2843,7 +2822,8 @@ const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const return d_datatypes; } -void DatatypeDeclarationCommand::invoke(api::Solver* solver) +void DatatypeDeclarationCommand::invoke(api::Solver* solver, + parser::SymbolManager* sm) { d_commandStatus = CommandSuccess::instance(); } @@ -2860,7 +2840,6 @@ std::string DatatypeDeclarationCommand::getCommandName() const void DatatypeDeclarationCommand::toStream(std::ostream& out, int toDepth, - size_t dag, OutputLanguage language) const { |