From c28f040e3b8c4aba150a61f0e42b1da7376b350e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Nov 2020 07:44:25 -0600 Subject: [PATCH] Pass symbol manager to commands (#5410) This PR passes the symbol manager to Command::invoke. There are no behavior changes in this PR. This is in preparation for reimplementing several features in the parser related to symbols. --- src/main/command_executor.cpp | 14 ++- src/main/command_executor.h | 5 +- src/smt/command.cpp | 189 +++++++++++++++------------------- src/smt/command.h | 167 +++++++++++++----------------- test/api/smt2_compliance.cpp | 2 +- 5 files changed, 168 insertions(+), 209 deletions(-) diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index a56210fb1..7b20f3a1a 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -119,9 +119,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; if(d_options.getVerbosity() >= -1) { - status = solverInvoke(d_solver.get(), cmd, d_options.getOut()); + status = + solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut()); } else { - status = solverInvoke(d_solver.get(), cmd, nullptr); + status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr); } api::Result res; @@ -198,15 +199,18 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) return status; } -bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out) +bool solverInvoke(api::Solver* solver, + parser::SymbolManager* sm, + Command* cmd, + std::ostream* out) { if (out == NULL) { - cmd->invoke(solver); + cmd->invoke(solver, sm); } else { - cmd->invoke(solver, *out); + cmd->invoke(solver, sm, *out); } // ignore the error if the command-verbosity is 0 for this command std::string commandName = diff --git a/src/main/command_executor.h b/src/main/command_executor.h index c3c310380..87748b1e5 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -116,7 +116,10 @@ private: }; /* class CommandExecutor */ -bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out); +bool solverInvoke(api::Solver* solver, + parser::SymbolManager* sm, + Command* cmd, + std::ostream* out); }/* CVC4::main namespace */ }/* CVC4 namespace */ 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(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& 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& 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& 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& 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& 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& 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& 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 { diff --git a/src/smt/command.h b/src/smt/command.h index 438f9febb..310850b78 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -41,6 +41,10 @@ class Solver; class Term; } // namespace api +namespace parser { +class SymbolManager; +} + class UnsatCore; class SmtEngine; class Command; @@ -202,8 +206,16 @@ class CVC4_PUBLIC Command virtual ~Command(); - virtual void invoke(api::Solver* solver) = 0; - virtual void invoke(api::Solver* solver, std::ostream& out); + /** + * Invoke the command on the solver and symbol manager sm. + */ + virtual void invoke(api::Solver* solver, parser::SymbolManager* sm) = 0; + /** + * Same as above, and prints the result to output stream out. + */ + virtual void invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out); virtual void toStream( std::ostream& out, @@ -276,13 +288,12 @@ class CVC4_PUBLIC EmptyCommand : public Command public: EmptyCommand(std::string name = ""); std::string getName() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -297,15 +308,16 @@ class CVC4_PUBLIC EchoCommand : public Command std::string getOutput() const; - void invoke(api::Solver* solver) override; - void invoke(api::Solver* solver, std::ostream& out) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -324,14 +336,13 @@ class CVC4_PUBLIC AssertCommand : public Command api::Term getTerm() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class AssertCommand */ @@ -339,13 +350,12 @@ class CVC4_PUBLIC AssertCommand : public Command class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PushCommand */ @@ -353,13 +363,12 @@ class CVC4_PUBLIC PushCommand : public Command class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PopCommand */ @@ -372,7 +381,7 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command public: DeclarationDefinitionCommand(const std::string& id); - void invoke(api::Solver* solver) override = 0; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override = 0; std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ @@ -392,13 +401,12 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand bool getPrintInModelSetByUser() const; void setPrintInModel(bool p); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ @@ -415,13 +423,12 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand size_t getArity() const; api::Sort getSort() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareSortCommand */ @@ -441,13 +448,12 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand const std::vector& getParameters() const; api::Sort getSort() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineSortCommand */ @@ -469,13 +475,12 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand const std::vector& getFormals() const; api::Term getFormula() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -506,7 +511,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand const std::vector& formals, api::Term formula, bool global); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; void toStream( std::ostream& out, @@ -536,13 +541,12 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command const std::vector >& getFormals() const; const std::vector& getFormulas() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -572,7 +576,7 @@ class CVC4_PUBLIC DeclareHeapCommand : public Command DeclareHeapCommand(api::Sort locSort, api::Sort dataSort); api::Sort getLocationSort() const; api::Sort getDataSort() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -603,13 +607,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command api::Term term, const std::string& value); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -637,14 +640,13 @@ class CVC4_PUBLIC CheckSatCommand : public Command api::Term getTerm() const; api::Result getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -666,14 +668,13 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command const std::vector& getTerms() const; api::Result getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -694,14 +695,13 @@ class CVC4_PUBLIC QueryCommand : public Command api::Term getTerm() const; api::Result getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QueryCommand */ @@ -722,7 +722,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand * The declared sygus variable is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -731,7 +731,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -772,7 +771,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand * The declared function-to-synthesize is communicated to the SMT engine in * case a synthesis conjecture is built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -781,7 +780,6 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -810,7 +808,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command * The declared constraint is communicated to the SMT engine in case a * synthesis conjecture is built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -819,7 +817,6 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -854,7 +851,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command * invariant constraint is built, in case an actual synthesis conjecture is * built later on. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -863,7 +860,6 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -891,7 +887,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command * and then perform a satisfiability check, whose result is stored in * d_result. */ - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -900,7 +896,6 @@ class CVC4_PUBLIC CheckSynthCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -925,14 +920,13 @@ class CVC4_PUBLIC SimplifyCommand : public Command api::Term getTerm() const; api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SimplifyCommand */ @@ -949,14 +943,13 @@ class CVC4_PUBLIC GetValueCommand : public Command const std::vector& getTerms() const; api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetValueCommand */ @@ -970,14 +963,13 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command GetAssignmentCommand(); SExpr getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssignmentCommand */ @@ -989,14 +981,13 @@ class CVC4_PUBLIC GetModelCommand : public Command // Model is private to the library -- for now // Model* getResult() const ; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1010,13 +1001,12 @@ class CVC4_PUBLIC BlockModelCommand : public Command public: BlockModelCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class BlockModelCommand */ @@ -1028,13 +1018,12 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command BlockModelValuesCommand(const std::vector& terms); const std::vector& getTerms() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1048,13 +1037,12 @@ class CVC4_PUBLIC GetProofCommand : public Command public: GetProofCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetProofCommand */ @@ -1064,14 +1052,13 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command public: GetInstantiationsCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1084,14 +1071,13 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command public: GetSynthSolutionCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1123,14 +1109,13 @@ class CVC4_PUBLIC GetInterpolCommand : public Command * query. */ api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1175,14 +1160,13 @@ class CVC4_PUBLIC GetAbductCommand : public Command */ api::Term getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1212,7 +1196,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command api::Term getTerm() const; bool getDoFull() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; api::Term getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; @@ -1221,7 +1205,6 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetQuantifierEliminationCommand */ @@ -1230,7 +1213,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; std::vector getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1238,7 +1221,6 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1252,7 +1234,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command GetUnsatCoreCommand(); const std::vector& getUnsatCore() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1260,7 +1242,6 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; @@ -1279,7 +1260,7 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command public: GetAssertionsCommand(); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; std::string getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1301,7 +1282,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command BenchmarkStatus getStatus() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1320,7 +1301,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command SetBenchmarkLogicCommand(std::string logic); std::string getLogic() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1342,7 +1323,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1364,7 +1345,7 @@ class CVC4_PUBLIC GetInfoCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1387,13 +1368,12 @@ class CVC4_PUBLIC SetOptionCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetOptionCommand */ @@ -1410,14 +1390,13 @@ class CVC4_PUBLIC GetOptionCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetOptionCommand */ @@ -1438,13 +1417,12 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command public: SetExpressionNameCommand(api::Term term, std::string name); - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetExpressionNameCommand */ @@ -1459,13 +1437,12 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command DatatypeDeclarationCommand(const std::vector& datatypes); const std::vector& getDatatypes() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DatatypeDeclarationCommand */ @@ -1474,13 +1451,12 @@ class CVC4_PUBLIC ResetCommand : public Command { public: ResetCommand() {} - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetCommand */ @@ -1489,13 +1465,12 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetAssertionsCommand */ @@ -1504,13 +1479,12 @@ class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand() {} - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QuitCommand */ @@ -1524,13 +1498,12 @@ class CVC4_PUBLIC CommentCommand : public Command std::string getComment() const; - void invoke(api::Solver* solver) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommentCommand */ @@ -1550,8 +1523,10 @@ class CVC4_PUBLIC CommandSequence : public Command void addCommand(Command* cmd); void clear(); - void invoke(api::Solver* solver) override; - void invoke(api::Solver* solver, std::ostream& out) override; + void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, + parser::SymbolManager* sm, + std::ostream& out) override; typedef std::vector::iterator iterator; typedef std::vector::const_iterator const_iterator; @@ -1567,7 +1542,6 @@ class CVC4_PUBLIC CommandSequence : public Command void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommandSequence */ @@ -1577,7 +1551,6 @@ class CVC4_PUBLIC DeclarationSequence : public CommandSequence void toStream( std::ostream& out, int toDepth = -1, - size_t dag = 1, OutputLanguage language = language::output::LANG_AUTO) const override; }; diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 7f9035636..8adab327e 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -70,7 +70,7 @@ void testGetInfo(api::Solver* solver, const char* s) assert(c != NULL); cout << c << endl; stringstream ss; - c->invoke(solver, ss); + c->invoke(solver, symman.get(), ss); assert(p->nextCommand() == NULL); delete p; delete c; -- 2.30.2