summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/expr/CMakeLists.txt2
-rw-r--r--src/expr/symbol_manager.cpp (renamed from src/parser/symbol_manager.cpp)4
-rw-r--r--src/expr/symbol_manager.h (renamed from src/parser/symbol_manager.h)13
-rw-r--r--src/main/command_executor.cpp4
-rw-r--r--src/main/command_executor.h8
-rw-r--r--src/main/interactive_shell.cpp5
-rw-r--r--src/main/interactive_shell.h5
-rw-r--r--src/parser/CMakeLists.txt2
-rw-r--r--src/parser/parser.h2
-rw-r--r--src/parser/parser_builder.h6
-rw-r--r--src/smt/command.cpp128
-rw-r--r--src/smt/command.h111
-rw-r--r--test/api/ouroborous.cpp3
-rw-r--r--test/api/smt2_compliance.cpp3
-rw-r--r--test/unit/main/interactive_shell_black.h6
-rw-r--r--test/unit/parser/parser_black.h12
-rw-r--r--test/unit/parser/parser_builder_black.h6
18 files changed, 147 insertions, 175 deletions
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/parser/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 32e17aea8..ac3b5d211 100644
--- a/src/parser/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -12,10 +12,9 @@
** \brief The symbol manager
**/
-#include "parser/symbol_manager.h"
+#include "expr/symbol_manager.h"
namespace CVC4 {
-namespace parser {
SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {}
@@ -73,5 +72,4 @@ void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
}
}
-} // namespace parser
} // namespace CVC4
diff --git a/src/parser/symbol_manager.h b/src/expr/symbol_manager.h
index 20b0c80e4..4890ed994 100644
--- a/src/parser/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -12,10 +12,10 @@
** \brief The symbol manager
**/
-#include "cvc4parser_public.h"
+#include "cvc4_public.h"
-#ifndef CVC4__PARSER__SYMBOL_MANAGER_H
-#define CVC4__PARSER__SYMBOL_MANAGER_H
+#ifndef CVC4__EXPR__SYMBOL_MANAGER_H
+#define CVC4__EXPR__SYMBOL_MANAGER_H
#include <map>
#include <set>
@@ -25,12 +25,14 @@
#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.
+ *
+ * Like SymbolTable, this class currently lives in src/expr/ since it uses
+ * context-dependent data structures.
*/
class CVC4_PUBLIC SymbolManager
{
@@ -96,7 +98,6 @@ class CVC4_PUBLIC SymbolManager
std::set<api::Term> d_namedAsserts;
};
-} // namespace parser
} // namespace CVC4
-#endif /* CVC4__PARSER__SYMBOL_MANAGER_H */
+#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<parser::SymbolManager> d_symman;
+ std::unique_ptr<SymbolManager> 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<string> 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. <code>build()</code> can be
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 68c776536..f1490e2f9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -28,10 +28,10 @@
#include "base/output.h"
#include "expr/expr_iomanip.h"
#include "expr/node.h"
+#include "expr/symbol_manager.h"
#include "expr/type.h"
#include "options/options.h"
#include "options/smt_options.h"
-#include "parser/symbol_manager.h"
#include "printer/printer.h"
#include "proof/unsat_core.h"
#include "smt/dump.h"
@@ -176,9 +176,7 @@ bool Command::interrupted() const
&& dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
}
-void Command::invoke(api::Solver* solver,
- parser::SymbolManager* sm,
- std::ostream& out)
+void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out)
{
invoke(solver, sm);
if (!(isMuted() && ok()))
@@ -218,7 +216,7 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const
EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
std::string EmptyCommand::getName() const { return d_name; }
-void EmptyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void EmptyCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
/* empty commands have no implementation */
d_commandStatus = CommandSuccess::instance();
@@ -241,14 +239,14 @@ void EmptyCommand::toStream(std::ostream& out,
EchoCommand::EchoCommand(std::string output) : d_output(output) {}
std::string EchoCommand::getOutput() const { return d_output; }
-void EchoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
/* we don't have an output stream here, nothing to do */
d_commandStatus = CommandSuccess::instance();
}
void EchoCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm,
+ SymbolManager* sm,
std::ostream& out)
{
out << d_output << std::endl;
@@ -281,7 +279,7 @@ AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
}
api::Term AssertCommand::getTerm() const { return d_term; }
-void AssertCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -317,7 +315,7 @@ void AssertCommand::toStream(std::ostream& out,
/* class PushCommand */
/* -------------------------------------------------------------------------- */
-void PushCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void PushCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -349,7 +347,7 @@ void PushCommand::toStream(std::ostream& out,
/* class PopCommand */
/* -------------------------------------------------------------------------- */
-void PopCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void PopCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -386,7 +384,7 @@ CheckSatCommand::CheckSatCommand() : d_term() {}
CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}
api::Term CheckSatCommand::getTerm() const { return d_term; }
-void CheckSatCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
<< std::endl;
@@ -454,8 +452,7 @@ const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
return d_terms;
}
-void CheckSatAssumingCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void CheckSatAssumingCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
<< " )~" << std::endl;
@@ -520,7 +517,7 @@ QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
}
api::Term QueryCommand::getTerm() const { return d_term; }
-void QueryCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -577,8 +574,7 @@ DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
api::Term DeclareSygusVarCommand::getVar() const { return d_var; }
api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }
-void DeclareSygusVarCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void DeclareSygusVarCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
d_commandStatus = CommandSuccess::instance();
}
@@ -633,7 +629,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; }
const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
-void SynthFunCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
d_commandStatus = CommandSuccess::instance();
}
@@ -672,8 +668,7 @@ SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
{
}
-void SygusConstraintCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -724,8 +719,7 @@ SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
{
}
-void SygusInvConstraintCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void SygusInvConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -771,7 +765,7 @@ void SygusInvConstraintCommand::toStream(std::ostream& out,
/* class CheckSynthCommand */
/* -------------------------------------------------------------------------- */
-void CheckSynthCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -839,7 +833,7 @@ void CheckSynthCommand::toStream(std::ostream& out,
/* class ResetCommand */
/* -------------------------------------------------------------------------- */
-void ResetCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -867,8 +861,7 @@ void ResetCommand::toStream(std::ostream& out,
/* class ResetAssertionsCommand */
/* -------------------------------------------------------------------------- */
-void ResetAssertionsCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void ResetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -903,7 +896,7 @@ void ResetAssertionsCommand::toStream(std::ostream& out,
/* class QuitCommand */
/* -------------------------------------------------------------------------- */
-void QuitCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
@@ -926,7 +919,7 @@ void QuitCommand::toStream(std::ostream& out,
CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
std::string CommentCommand::getComment() const { return d_comment; }
-void CommentCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CommentCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
@@ -962,7 +955,7 @@ void CommandSequence::addCommand(Command* cmd)
}
void CommandSequence::clear() { d_commandSequence.clear(); }
-void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CommandSequence::invoke(api::Solver* solver, SymbolManager* sm)
{
for (; d_index < d_commandSequence.size(); ++d_index)
{
@@ -981,7 +974,7 @@ void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm)
}
void CommandSequence::invoke(api::Solver* solver,
- parser::SymbolManager* sm,
+ SymbolManager* sm,
std::ostream& out)
{
for (; d_index < d_commandSequence.size(); ++d_index)
@@ -1096,8 +1089,7 @@ void DeclareFunctionCommand::setPrintInModel(bool p)
d_printInModelSetByUser = true;
}
-void DeclareFunctionCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
d_commandStatus = CommandSuccess::instance();
}
@@ -1138,7 +1130,7 @@ DeclareSortCommand::DeclareSortCommand(const std::string& id,
size_t DeclareSortCommand::getArity() const { return d_arity; }
api::Sort DeclareSortCommand::getSort() const { return d_sort; }
-void DeclareSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
d_commandStatus = CommandSuccess::instance();
}
@@ -1184,7 +1176,7 @@ const std::vector<api::Sort>& DefineSortCommand::getParameters() const
}
api::Sort DefineSortCommand::getSort() const { return d_sort; }
-void DefineSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void DefineSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
d_commandStatus = CommandSuccess::instance();
}
@@ -1245,8 +1237,7 @@ const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
}
api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
-void DefineFunctionCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1301,8 +1292,7 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(
{
}
-void DefineNamedFunctionCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void DefineNamedFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
this->DefineFunctionCommand::invoke(solver, sm);
if (!d_func.isNull() && d_func.getSort().isBoolean())
@@ -1374,8 +1364,7 @@ const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
return d_formulas;
}
-void DefineFunctionRecCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1427,7 +1416,7 @@ DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort)
api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
-void DeclareHeapCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void DeclareHeapCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
solver->declareSeparationHeap(d_locSort, d_dataSort);
}
@@ -1485,8 +1474,7 @@ SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
{
}
-void SetUserAttributeCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1531,7 +1519,7 @@ void SetUserAttributeCommand::toStream(std::ostream& out,
SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {}
api::Term SimplifyCommand::getTerm() const { return d_term; }
-void SimplifyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1598,7 +1586,7 @@ const std::vector<api::Term>& GetValueCommand::getTerms() const
{
return d_terms;
}
-void GetValueCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1664,8 +1652,7 @@ void GetValueCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetAssignmentCommand::GetAssignmentCommand() {}
-void GetAssignmentCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1735,7 +1722,7 @@ void GetAssignmentCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetModelCommand::GetModelCommand() : d_result(nullptr) {}
-void GetModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1796,7 +1783,7 @@ void GetModelCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
BlockModelCommand::BlockModelCommand() {}
-void BlockModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1850,8 +1837,7 @@ const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
{
return d_terms;
}
-void BlockModelValuesCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1897,7 +1883,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetProofCommand::GetProofCommand() {}
-void GetProofCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
Unimplemented() << "Unimplemented get-proof\n";
}
@@ -1923,8 +1909,7 @@ void GetProofCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
-void GetInstantiationsCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -1976,8 +1961,7 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
-void GetSynthSolutionCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void GetSynthSolutionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2047,7 +2031,7 @@ const api::Grammar* GetInterpolCommand::getGrammar() const
api::Term GetInterpolCommand::getResult() const { return d_result; }
-void GetInterpolCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2138,7 +2122,7 @@ const api::Grammar* GetAbductCommand::getGrammar() const
std::string GetAbductCommand::getAbductName() const { return d_name; }
api::Term GetAbductCommand::getResult() const { return d_result; }
-void GetAbductCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2215,7 +2199,7 @@ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
void GetQuantifierEliminationCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+ SymbolManager* sm)
{
try
{
@@ -2280,8 +2264,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
-void GetUnsatAssumptionsCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2341,7 +2324,7 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetUnsatCoreCommand::GetUnsatCoreCommand() {}
-void GetUnsatCoreCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2406,8 +2389,7 @@ void GetUnsatCoreCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
GetAssertionsCommand::GetAssertionsCommand() {}
-void GetAssertionsCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2473,8 +2455,7 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
return d_status;
}
-void SetBenchmarkStatusCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void SetBenchmarkStatusCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2525,8 +2506,7 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
}
std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
-void SetBenchmarkLogicCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void SetBenchmarkLogicCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2568,7 +2548,7 @@ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
std::string SetInfoCommand::getFlag() const { return d_flag; }
SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
-void SetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2607,7 +2587,7 @@ void SetInfoCommand::toStream(std::ostream& out,
GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
std::string GetInfoCommand::getFlag() const { return d_flag; }
-void GetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2678,7 +2658,7 @@ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
std::string SetOptionCommand::getFlag() const { return d_flag; }
SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
-void SetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2716,7 +2696,7 @@ void SetOptionCommand::toStream(std::ostream& out,
GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
std::string GetOptionCommand::getFlag() const { return d_flag; }
-void GetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
@@ -2773,8 +2753,7 @@ SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
{
}
-void SetExpressionNameCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
d_commandStatus = CommandSuccess::instance();
@@ -2822,8 +2801,7 @@ const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
return d_datatypes;
}
-void DatatypeDeclarationCommand::invoke(api::Solver* solver,
- parser::SymbolManager* sm)
+void DatatypeDeclarationCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
d_commandStatus = CommandSuccess::instance();
}
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<api::Sort>& 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<api::Term>& 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<api::Term>& 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<std::vector<api::Term> >& getFormals() const;
const std::vector<api::Term>& 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<api::Term>& 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<api::Term>& 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<api::Term>& terms);
const std::vector<api::Term>& 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<api::Term> 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<api::Term>& 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<api::Sort>& datatypes);
const std::vector<api::Sort>& 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<Command*>::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<api::Solver> solver =
std::unique_ptr<api::Solver>(new api::Solver());
- std::unique_ptr<parser::SymbolManager> symman(
- new parser::SymbolManager(solver.get()));
+ std::unique_ptr<SymbolManager> 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<parser::SymbolManager> symman(
- new parser::SymbolManager(solver));
+ std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
ParserBuilder pb(solver, symman.get(), "<internal>", 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<api::Solver> d_solver;
- std::unique_ptr<parser::SymbolManager> d_symman;
+ std::unique_ptr<SymbolManager> 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<api::Solver> d_solver;
- std::unique_ptr<parser::SymbolManager> d_symman;
+ std::unique_ptr<SymbolManager> 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 <iostream>
#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<api::Solver> d_solver;
- std::unique_ptr<parser::SymbolManager> d_symman;
+ std::unique_ptr<SymbolManager> d_symman;
}; // class ParserBuilderBlack
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback