From: Andrew Reynolds Date: Wed, 11 Nov 2020 18:56:03 +0000 (-0600) Subject: Move symbol manager to src/expr/ (#5420) X-Git-Tag: cvc5-1.0.0~2613 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80930ce4f6d21b417028a5ec207ddfbd7d85e66d;p=cvc5.git Move symbol manager to src/expr/ (#5420) This is required since symbol manager will use context dependent data structures (in its cpp). This is required since classes in src/parser/ are not allowed to include private headers. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1a06e9366..c1e39f47e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1128,6 +1128,7 @@ install(FILES expr/expr_iomanip.h expr/record.h expr/sequence.h + expr/symbol_manager.h expr/symbol_table.h expr/type.h expr/uninterpreted_constant.h @@ -1151,7 +1152,6 @@ install(FILES parser/parser_builder.h parser/parser_exception.h parser/parse_op.h - parser/symbol_manager.h DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/parser) install(FILES diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index d7af52fec..fb3df5327 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -76,6 +76,8 @@ libcvc4_add_sources( proof_step_buffer.h skolem_manager.cpp skolem_manager.h + symbol_manager.cpp + symbol_manager.h symbol_table.cpp symbol_table.h tconv_seq_proof_generator.cpp diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp new file mode 100644 index 000000000..ac3b5d211 --- /dev/null +++ b/src/expr/symbol_manager.cpp @@ -0,0 +1,75 @@ +/********************* */ +/*! \file symbol_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The symbol manager + **/ + +#include "expr/symbol_manager.h" + +namespace CVC4 { + +SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {} + +SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; } + +bool SymbolManager::setExpressionName(api::Term t, + const std::string& name, + bool isAssertion) +{ + if (d_names.find(t) != d_names.end()) + { + // already named assertion + return false; + } + if (isAssertion) + { + d_namedAsserts.insert(t); + } + d_names[t] = name; + return true; +} + +bool SymbolManager::getExpressionName(api::Term t, + std::string& name, + bool isAssertion) const +{ + std::map::const_iterator it = d_names.find(t); + if (it == d_names.end()) + { + return false; + } + if (isAssertion) + { + // must be an assertion name + if (d_namedAsserts.find(t) == d_namedAsserts.end()) + { + return false; + } + } + name = it->second; + return true; +} + +void SymbolManager::getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions) const +{ + for (const api::Term& t : ts) + { + std::string name; + if (getExpressionName(t, name, areAssertions)) + { + names.push_back(name); + } + } +} + +} // namespace CVC4 diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h new file mode 100644 index 000000000..4890ed994 --- /dev/null +++ b/src/expr/symbol_manager.h @@ -0,0 +1,103 @@ +/********************* */ +/*! \file symbol_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The symbol manager + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__EXPR__SYMBOL_MANAGER_H +#define CVC4__EXPR__SYMBOL_MANAGER_H + +#include +#include +#include + +#include "api/cvc4cpp.h" +#include "expr/symbol_table.h" + +namespace CVC4 { + +/** + * Symbol manager, which manages: + * (1) The symbol table used by the parser, + * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2. + * + * Like SymbolTable, this class currently lives in src/expr/ since it uses + * context-dependent data structures. + */ +class CVC4_PUBLIC SymbolManager +{ + public: + SymbolManager(api::Solver* s); + ~SymbolManager() {} + /** Get the underlying symbol table */ + SymbolTable* getSymbolTable(); + //---------------------------- named expressions + /** Set name of term t to name + * + * @param t The term to name + * @param name The given name + * @param isAssertion Whether t is being given a name in an assertion + * context. In particular, this is true if and only if there was an assertion + * command of the form (assert (! t :named name)). + * @return true if the name was set. This method may return false if t + * already has a name. + */ + bool setExpressionName(api::Term t, + const std::string& name, + bool isAssertion = false); + /** Get name for term t + * + * @param t The term + * @param name The argument to update with the name of t + * @param isAssertion Whether we only wish to get the assertion name of t + * @return true if t has a name. If so, name is updated to that name. + * Otherwise, name is unchanged. + */ + bool getExpressionName(api::Term t, + std::string& name, + bool isAssertion = false) const; + /** + * Convert list of terms to list of names. This adds to names the names of + * all terms in ts that has names. Terms that do not have names are not + * included. + * + * Notice that we do not distinguish what terms among those in ts have names. + * If the caller of this method wants more fine-grained information about what + * specific terms had names, then use the more fine grained interface above, + * per term. + * + * @param ts The terms + * @param names The name list + * @param areAssertions Whether we only wish to include assertion names + */ + void getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions = false) const; + //---------------------------- end named expressions + + private: + /** The API Solver object. */ + api::Solver* d_solver; + /** + * The declaration scope that is "owned" by this symbol manager. + */ + SymbolTable d_symtabAllocated; + /** Map terms to names */ + std::map d_names; + /** The set of terms with assertion names */ + std::set d_namedAsserts; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__SYMBOL_MANAGER_H */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 7b20f3a1a..be90be3f0 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -50,7 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString CommandExecutor::CommandExecutor(Options& options) : d_solver(new api::Solver(&options)), - d_symman(new parser::SymbolManager(d_solver.get())), + d_symman(new SymbolManager(d_solver.get())), d_smtEngine(d_solver->getSmtEngine()), d_options(options), d_stats("driver"), @@ -200,7 +200,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) } bool solverInvoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, Command* cmd, std::ostream* out) { diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 87748b1e5..acf9e45bb 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -20,8 +20,8 @@ #include "api/cvc4cpp.h" #include "expr/expr_manager.h" +#include "expr/symbol_manager.h" #include "options/options.h" -#include "parser/symbol_manager.h" #include "smt/smt_engine.h" #include "util/statistics_registry.h" @@ -52,7 +52,7 @@ class CommandExecutor * Certain commands (e.g. reset-assertions) have a specific impact on the * symbol manager. */ - std::unique_ptr d_symman; + std::unique_ptr d_symman; SmtEngine* d_smtEngine; Options& d_options; StatisticsRegistry d_stats; @@ -80,7 +80,7 @@ class CommandExecutor api::Solver* getSolver() { return d_solver.get(); } /** Get a pointer to the symbol manager owned by this CommandExecutor */ - parser::SymbolManager* getSymbolManager() { return d_symman.get(); } + SymbolManager* getSymbolManager() { return d_symman.get(); } api::Result getResult() const { return d_result; } void reset(); @@ -117,7 +117,7 @@ private: }; /* class CommandExecutor */ bool solverInvoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, Command* cmd, std::ostream* out); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 8d482b08e..3586fce87 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -38,12 +38,12 @@ #include "api/cvc4cpp.h" #include "base/output.h" +#include "expr/symbol_manager.h" #include "options/language.h" #include "options/options.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "parser/symbol_manager.h" #include "smt/command.h" #include "theory/logic_info.h" @@ -84,8 +84,7 @@ static set s_declarations; #endif /* HAVE_LIBEDITLINE */ -InteractiveShell::InteractiveShell(api::Solver* solver, - parser::SymbolManager* sm) +InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) : d_options(solver->getOptions()), d_in(*d_options.getIn()), d_out(*d_options.getOutConst()), diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index b00f8a8f4..4d60d3445 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -33,9 +33,10 @@ class Solver; namespace parser { class Parser; - class SymbolManager; }/* CVC4::parser namespace */ +class SymbolManager; + class CVC4_PUBLIC InteractiveShell { const Options& d_options; @@ -51,7 +52,7 @@ class CVC4_PUBLIC InteractiveShell static const unsigned s_historyLimit = 500; public: - InteractiveShell(api::Solver* solver, parser::SymbolManager* sm); + InteractiveShell(api::Solver* solver, SymbolManager* sm); /** * Close out the interactive session. diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 7b55c0915..8e69da34b 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -55,8 +55,6 @@ set(libcvc4parser_src_files smt2/smt2_input.h smt2/sygus_input.cpp smt2/sygus_input.h - symbol_manager.cpp - symbol_manager.h tptp/TptpLexer.c tptp/TptpParser.c tptp/tptp.cpp diff --git a/src/parser/parser.h b/src/parser/parser.h index 405935165..c762fc117 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -26,11 +26,11 @@ #include "api/cvc4cpp.h" #include "expr/kind.h" +#include "expr/symbol_manager.h" #include "expr/symbol_table.h" #include "parser/input.h" #include "parser/parse_op.h" #include "parser/parser_exception.h" -#include "parser/symbol_manager.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 9d62c12a3..bf205b13a 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -26,16 +26,16 @@ namespace CVC4 { -class Options; - namespace api { class Solver; } +class Options; +class SymbolManager; + namespace parser { class Parser; -class SymbolManager; /** * A builder for input language parsers. build() can be diff --git a/src/parser/symbol_manager.cpp b/src/parser/symbol_manager.cpp deleted file mode 100644 index 32e17aea8..000000000 --- a/src/parser/symbol_manager.cpp +++ /dev/null @@ -1,77 +0,0 @@ -/********************* */ -/*! \file symbol_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The symbol manager - **/ - -#include "parser/symbol_manager.h" - -namespace CVC4 { -namespace parser { - -SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {} - -SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; } - -bool SymbolManager::setExpressionName(api::Term t, - const std::string& name, - bool isAssertion) -{ - if (d_names.find(t) != d_names.end()) - { - // already named assertion - return false; - } - if (isAssertion) - { - d_namedAsserts.insert(t); - } - d_names[t] = name; - return true; -} - -bool SymbolManager::getExpressionName(api::Term t, - std::string& name, - bool isAssertion) const -{ - std::map::const_iterator it = d_names.find(t); - if (it == d_names.end()) - { - return false; - } - if (isAssertion) - { - // must be an assertion name - if (d_namedAsserts.find(t) == d_namedAsserts.end()) - { - return false; - } - } - name = it->second; - return true; -} - -void SymbolManager::getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions) const -{ - for (const api::Term& t : ts) - { - std::string name; - if (getExpressionName(t, name, areAssertions)) - { - names.push_back(name); - } - } -} - -} // namespace parser -} // namespace CVC4 diff --git a/src/parser/symbol_manager.h b/src/parser/symbol_manager.h deleted file mode 100644 index 20b0c80e4..000000000 --- a/src/parser/symbol_manager.h +++ /dev/null @@ -1,102 +0,0 @@ -/********************* */ -/*! \file symbol_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief The symbol manager - **/ - -#include "cvc4parser_public.h" - -#ifndef CVC4__PARSER__SYMBOL_MANAGER_H -#define CVC4__PARSER__SYMBOL_MANAGER_H - -#include -#include -#include - -#include "api/cvc4cpp.h" -#include "expr/symbol_table.h" - -namespace CVC4 { -namespace parser { - -/** - * Symbol manager, which manages: - * (1) The symbol table used by the parser, - * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2. - */ -class CVC4_PUBLIC SymbolManager -{ - public: - SymbolManager(api::Solver* s); - ~SymbolManager() {} - /** Get the underlying symbol table */ - SymbolTable* getSymbolTable(); - //---------------------------- named expressions - /** Set name of term t to name - * - * @param t The term to name - * @param name The given name - * @param isAssertion Whether t is being given a name in an assertion - * context. In particular, this is true if and only if there was an assertion - * command of the form (assert (! t :named name)). - * @return true if the name was set. This method may return false if t - * already has a name. - */ - bool setExpressionName(api::Term t, - const std::string& name, - bool isAssertion = false); - /** Get name for term t - * - * @param t The term - * @param name The argument to update with the name of t - * @param isAssertion Whether we only wish to get the assertion name of t - * @return true if t has a name. If so, name is updated to that name. - * Otherwise, name is unchanged. - */ - bool getExpressionName(api::Term t, - std::string& name, - bool isAssertion = false) const; - /** - * Convert list of terms to list of names. This adds to names the names of - * all terms in ts that has names. Terms that do not have names are not - * included. - * - * Notice that we do not distinguish what terms among those in ts have names. - * If the caller of this method wants more fine-grained information about what - * specific terms had names, then use the more fine grained interface above, - * per term. - * - * @param ts The terms - * @param names The name list - * @param areAssertions Whether we only wish to include assertion names - */ - void getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions = false) const; - //---------------------------- end named expressions - - private: - /** The API Solver object. */ - api::Solver* d_solver; - /** - * The declaration scope that is "owned" by this symbol manager. - */ - SymbolTable d_symtabAllocated; - /** Map terms to names */ - std::map d_names; - /** The set of terms with assertion names */ - std::set d_namedAsserts; -}; - -} // namespace parser -} // namespace CVC4 - -#endif /* CVC4__PARSER__SYMBOL_MANAGER_H */ 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(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& 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& 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& 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& 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& 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& 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& 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(); } diff --git a/src/smt/command.h b/src/smt/command.h index 310850b78..7d794cf3f 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -41,10 +41,7 @@ class Solver; class Term; } // namespace api -namespace parser { class SymbolManager; -} - class UnsatCore; class SmtEngine; class Command; @@ -209,12 +206,12 @@ class CVC4_PUBLIC Command /** * Invoke the command on the solver and symbol manager sm. */ - virtual void invoke(api::Solver* solver, parser::SymbolManager* sm) = 0; + virtual void invoke(api::Solver* solver, SymbolManager* sm) = 0; /** * Same as above, and prints the result to output stream out. */ virtual void invoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, std::ostream& out); virtual void toStream( @@ -288,7 +285,7 @@ class CVC4_PUBLIC EmptyCommand : public Command public: EmptyCommand(std::string name = ""); std::string getName() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -308,9 +305,9 @@ class CVC4_PUBLIC EchoCommand : public Command std::string getOutput() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void invoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, std::ostream& out) override; Command* clone() const override; @@ -336,7 +333,7 @@ class CVC4_PUBLIC AssertCommand : public Command api::Term getTerm() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; @@ -350,7 +347,7 @@ class CVC4_PUBLIC AssertCommand : public Command class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -363,7 +360,7 @@ class CVC4_PUBLIC PushCommand : public Command class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -381,7 +378,7 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command public: DeclarationDefinitionCommand(const std::string& id); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override = 0; + void invoke(api::Solver* solver, SymbolManager* sm) override = 0; std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ @@ -401,7 +398,7 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand bool getPrintInModelSetByUser() const; void setPrintInModel(bool p); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -423,7 +420,7 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand size_t getArity() const; api::Sort getSort() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -448,7 +445,7 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand const std::vector& getParameters() const; api::Sort getSort() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -475,7 +472,7 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand const std::vector& getFormals() const; api::Term getFormula() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -511,7 +508,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand const std::vector& formals, api::Term formula, bool global); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; void toStream( std::ostream& out, @@ -541,7 +538,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command const std::vector >& getFormals() const; const std::vector& getFormulas() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -576,7 +573,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, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -607,7 +604,7 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command api::Term term, const std::string& value); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -640,7 +637,7 @@ class CVC4_PUBLIC CheckSatCommand : public Command api::Term getTerm() const; api::Result getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -668,7 +665,7 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command const std::vector& getTerms() const; api::Result getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -695,7 +692,7 @@ class CVC4_PUBLIC QueryCommand : public Command api::Term getTerm() const; api::Result getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -722,7 +719,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, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -771,7 +768,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, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -808,7 +805,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, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -851,7 +848,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, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -887,7 +884,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, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; /** creates a copy of this command */ Command* clone() const override; /** returns this command's name */ @@ -920,7 +917,7 @@ class CVC4_PUBLIC SimplifyCommand : public Command api::Term getTerm() const; api::Term getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -943,7 +940,7 @@ class CVC4_PUBLIC GetValueCommand : public Command const std::vector& getTerms() const; api::Term getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -963,7 +960,7 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command GetAssignmentCommand(); SExpr getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -981,7 +978,7 @@ class CVC4_PUBLIC GetModelCommand : public Command // Model is private to the library -- for now // Model* getResult() const ; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1001,7 +998,7 @@ class CVC4_PUBLIC BlockModelCommand : public Command public: BlockModelCommand(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1018,7 +1015,7 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command BlockModelValuesCommand(const std::vector& terms); const std::vector& getTerms() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1037,7 +1034,7 @@ class CVC4_PUBLIC GetProofCommand : public Command public: GetProofCommand(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1052,7 +1049,7 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command public: GetInstantiationsCommand(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1071,7 +1068,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command public: GetSynthSolutionCommand(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1109,7 +1106,7 @@ class CVC4_PUBLIC GetInterpolCommand : public Command * query. */ api::Term getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1160,7 +1157,7 @@ class CVC4_PUBLIC GetAbductCommand : public Command */ api::Term getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1196,7 +1193,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command api::Term getTerm() const; bool getDoFull() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; api::Term getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; @@ -1213,7 +1210,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; std::vector getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1234,7 +1231,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command GetUnsatCoreCommand(); const std::vector& getUnsatCore() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1260,7 +1257,7 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command public: GetAssertionsCommand(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; std::string getResult() const; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; @@ -1282,7 +1279,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command BenchmarkStatus getStatus() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1301,7 +1298,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command SetBenchmarkLogicCommand(std::string logic); std::string getLogic() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1323,7 +1320,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1345,7 +1342,7 @@ class CVC4_PUBLIC GetInfoCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1368,7 +1365,7 @@ class CVC4_PUBLIC SetOptionCommand : public Command std::string getFlag() const; SExpr getSExpr() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1390,7 +1387,7 @@ class CVC4_PUBLIC GetOptionCommand : public Command std::string getFlag() const; std::string getResult() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; @@ -1417,7 +1414,7 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command public: SetExpressionNameCommand(api::Term term, std::string name); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1437,7 +1434,7 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command DatatypeDeclarationCommand(const std::vector& datatypes); const std::vector& getDatatypes() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1451,7 +1448,7 @@ class CVC4_PUBLIC ResetCommand : public Command { public: ResetCommand() {} - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1465,7 +1462,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1479,7 +1476,7 @@ class CVC4_PUBLIC QuitCommand : public Command { public: QuitCommand() {} - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1498,7 +1495,7 @@ class CVC4_PUBLIC CommentCommand : public Command std::string getComment() const; - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; void toStream( @@ -1523,9 +1520,9 @@ class CVC4_PUBLIC CommandSequence : public Command void addCommand(Command* cmd); void clear(); - void invoke(api::Solver* solver, parser::SymbolManager* sm) override; + void invoke(api::Solver* solver, SymbolManager* sm) override; void invoke(api::Solver* solver, - parser::SymbolManager* sm, + SymbolManager* sm, std::ostream& out) override; typedef std::vector::iterator iterator; diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 5ed240233..efca53ab3 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -111,8 +111,7 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL int runTest() { std::unique_ptr solver = std::unique_ptr(new api::Solver()); - std::unique_ptr symman( - new parser::SymbolManager(solver.get())); + std::unique_ptr symman(new SymbolManager(solver.get())); psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer") .withStringInput(declarations) .withInputLanguage(input::LANG_SMTLIB_V2) diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 8adab327e..3738bd1b6 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -60,8 +60,7 @@ int main() void testGetInfo(api::Solver* solver, const char* s) { - std::unique_ptr symman( - new parser::SymbolManager(solver)); + std::unique_ptr symman(new SymbolManager(solver)); ParserBuilder pb(solver, symman.get(), "", solver->getOptions()); Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index af6960ff7..993f24690 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -22,12 +22,12 @@ #include "api/cvc4cpp.h" #include "expr/expr_manager.h" +#include "expr/symbol_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" #include "options/language.h" #include "options/options.h" #include "parser/parser_builder.h" -#include "parser/symbol_manager.h" #include "smt/command.h" using namespace CVC4; @@ -45,7 +45,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite d_options.set(options::inputLanguage, language::input::LANG_CVC4); d_symman.reset(nullptr); d_solver.reset(new api::Solver(&d_options)); - d_symman.reset(new parser::SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager(d_solver.get())); } void tearDown() override @@ -99,7 +99,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite private: std::unique_ptr d_solver; - std::unique_ptr d_symman; + std::unique_ptr d_symman; Options d_options; stringstream* d_sin; stringstream* d_sout; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 2bdd5c950..3b0bbb139 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -23,13 +23,13 @@ #include "base/output.h" #include "expr/expr.h" #include "expr/expr_manager.h" +#include "expr/symbol_manager.h" #include "options/base_options.h" #include "options/language.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" -#include "parser/symbol_manager.h" #include "smt/command.h" using namespace CVC4; @@ -70,7 +70,7 @@ class ParserBlack // Debug.on("parser-extra"); // cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - d_symman.reset(new parser::SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager(d_solver.get())); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(goodInput) .withOptions(d_options) @@ -102,7 +102,7 @@ class ParserBlack // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - d_symman.reset(new parser::SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager(d_solver.get())); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(badInput) .withOptions(d_options) @@ -134,7 +134,7 @@ class ParserBlack // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - d_symman.reset(new parser::SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager(d_solver.get())); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(goodExpr) .withOptions(d_options) @@ -182,7 +182,7 @@ class ParserBlack // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; - d_symman.reset(new parser::SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager(d_solver.get())); Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") .withStringInput(badExpr) .withOptions(d_options) @@ -224,7 +224,7 @@ class ParserBlack private: InputLanguage d_lang; std::unique_ptr d_solver; - std::unique_ptr d_symman; + std::unique_ptr d_symman; }; /* class ParserBlack */ diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index b8ec96836..c101542d0 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -25,10 +25,10 @@ #include #include "api/cvc4cpp.h" +#include "expr/symbol_manager.h" #include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "parser/symbol_manager.h" using namespace CVC4; using namespace CVC4::parser; @@ -43,7 +43,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite // ensure the old symbol manager is deleted d_symman.reset(nullptr); d_solver.reset(new api::Solver()); - d_symman.reset(new parser::SymbolManager(d_solver.get())); + d_symman.reset(new SymbolManager(d_solver.get())); } void tearDown() override {} @@ -134,6 +134,6 @@ class ParserBuilderBlack : public CxxTest::TestSuite } std::unique_ptr d_solver; - std::unique_ptr d_symman; + std::unique_ptr d_symman; }; // class ParserBuilderBlack