diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-26 09:15:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-26 09:15:30 -0600 |
commit | d3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88 (patch) | |
tree | bd51ec106bd30add6a8a9e5f3300a6ae022f0e97 /src/smt/command.cpp | |
parent | 70f0cddbce01fa17622b7b70b638794181aefec5 (diff) |
Removing infrastructure related to SMT model (#5527)
Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine.
The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index fa3eb66c0..e6361be9e 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1069,25 +1069,12 @@ DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, api::Sort sort) : DeclarationDefinitionCommand(id), d_func(func), - d_sort(sort), - d_printInModel(true), - d_printInModelSetByUser(false) + d_sort(sort) { } api::Term DeclareFunctionCommand::getFunction() const { return d_func; } api::Sort DeclareFunctionCommand::getSort() const { return d_sort; } -bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel; } -bool DeclareFunctionCommand::getPrintInModelSetByUser() const -{ - return d_printInModelSetByUser; -} - -void DeclareFunctionCommand::setPrintInModel(bool p) -{ - d_printInModel = p; - d_printInModelSetByUser = true; -} void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm) { @@ -1100,8 +1087,6 @@ Command* DeclareFunctionCommand::clone() const { DeclareFunctionCommand* dfc = new DeclareFunctionCommand(d_symbol, d_func, d_sort); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; return dfc; } |