From: Andrew Reynolds Date: Thu, 26 Nov 2020 15:15:30 +0000 (-0600) Subject: Removing infrastructure related to SMT model (#5527) X-Git-Tag: cvc5-1.0.0~2546 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88;p=cvc5.git 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. --- diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 612084de2..56d54eec9 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -67,24 +67,14 @@ void CheckModels::checkModel(Model* m, /* substituteUnderQuantifiers = */ false); Trace("check-model") << "checkModel: Collect substitution..." << std::endl; - for (size_t k = 0, ncmd = m->getNumCommands(); k < ncmd; ++k) + const std::vector& decTerms = m->getDeclaredTerms(); + for (const Node& func : decTerms) { - const DeclareFunctionNodeCommand* c = - dynamic_cast(m->getCommand(k)); - Notice() << "SmtEngine::checkModel(): model command " << k << " : " - << m->getCommand(k)->toString() << std::endl; - if (c == nullptr) - { - // we don't care about DECLARE-DATATYPES, DECLARE-SORT, ... - Notice() << "SmtEngine::checkModel(): skipping..." << std::endl; - continue; - } // We have a DECLARE-FUN: // // We'll first do some checks, then add to our substitution map // the mapping: function symbol |-> value - Node func = c->getFunction(); Node val = m->getValue(func); Notice() << "SmtEngine::checkModel(): adding substitution: " << func 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; } diff --git a/src/smt/command.h b/src/smt/command.h index 96a6938d6..0b86f3539 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -387,16 +387,11 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand protected: api::Term d_func; api::Sort d_sort; - bool d_printInModel; - bool d_printInModelSetByUser; public: DeclareFunctionCommand(const std::string& id, api::Term func, api::Sort sort); api::Term getFunction() const; api::Sort getSort() const; - bool getPrintInModel() const; - bool getPrintInModelSetByUser() const; - void setPrintInModel(bool p); void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp index 9b7fba5a2..9d3031b4d 100644 --- a/src/smt/dump_manager.cpp +++ b/src/smt/dump_manager.cpp @@ -24,8 +24,6 @@ namespace smt { DumpManager::DumpManager(context::UserContext* u) : d_fullyInited(false), - d_modelGlobalCommands(), - d_modelCommands(u), d_dumpCommands() { } @@ -33,8 +31,6 @@ DumpManager::DumpManager(context::UserContext* u) DumpManager::~DumpManager() { d_dumpCommands.clear(); - d_modelCommandsAlloc.clear(); - d_modelGlobalCommands.clear(); } void DumpManager::finishInit() @@ -49,8 +45,10 @@ void DumpManager::finishInit() d_fullyInited = true; } - -void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); } +void DumpManager::resetAssertions() +{ + // currently, do nothing +} void DumpManager::addToModelCommandAndDump(const NodeCommand& c, uint32_t flags, @@ -58,29 +56,6 @@ void DumpManager::addToModelCommandAndDump(const NodeCommand& c, const char* dumpTag) { Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << std::endl; - // If we aren't yet fully inited, the user might still turn on - // produce-models. So let's keep any commands around just in - // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares - // sort "U" in QF_UF before setLogic() is run and we still want to - // support finding card(U) with --finite-model-find, and (2) to - // decouple SmtEngine and ExprManager if the user does a few - // ExprManager::mkSort() before SmtEngine::setOption("produce-models") - // and expects to find their cardinalities in the model. - if ((!d_fullyInited || options::produceModels()) - && (flags & ExprManager::VAR_FLAG_DEFINED) == 0) - { - if (flags & ExprManager::VAR_FLAG_GLOBAL) - { - d_modelGlobalCommands.push_back(std::unique_ptr(c.clone())); - } - else - { - NodeCommand* cc = c.clone(); - d_modelCommands.push_back(cc); - // also remember for memory management purposes - d_modelCommandsAlloc.push_back(std::unique_ptr(cc)); - } - } if (Dump.isOn(dumpTag)) { if (d_fullyInited) @@ -97,48 +72,7 @@ void DumpManager::addToModelCommandAndDump(const NodeCommand& c, void DumpManager::setPrintFuncInModel(Node f, bool p) { Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; - for (std::unique_ptr& c : d_modelGlobalCommands) - { - DeclareFunctionNodeCommand* dfc = - dynamic_cast(c.get()); - if (dfc != NULL) - { - Node df = dfc->getFunction(); - if (df == f) - { - dfc->setPrintInModel(p); - } - } - } - for (NodeCommand* c : d_modelCommands) - { - DeclareFunctionNodeCommand* dfc = - dynamic_cast(c); - if (dfc != NULL) - { - Node df = dfc->getFunction(); - if (df == f) - { - dfc->setPrintInModel(p); - } - } - } -} - -size_t DumpManager::getNumModelCommands() const -{ - return d_modelCommands.size() + d_modelGlobalCommands.size(); -} - -const NodeCommand* DumpManager::getModelCommand(size_t i) const -{ - Assert(i < getNumModelCommands()); - // index the global commands first, then the locals - if (i < d_modelGlobalCommands.size()) - { - return d_modelGlobalCommands[i].get(); - } - return d_modelCommands[i - d_modelGlobalCommands.size()]; + // TODO (cvc4-wishues/issues/75): implement } } // namespace smt diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 0ba8e0b8b..eaedf39a1 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -31,14 +31,10 @@ namespace smt { /** * This utility is responsible for: - * (1) storing information required for SMT-LIB queries such as get-model, - * which requires knowing what symbols are declared and should be printed in - * the model. - * (2) implementing some dumping traces e.g. --dump=declarations. + * implementing some dumping traces e.g. --dump=declarations. */ class DumpManager { - typedef context::CDList CommandList; public: DumpManager(context::UserContext* u); @@ -65,34 +61,10 @@ class DumpManager * Set that function f should print in the model if and only if p is true. */ void setPrintFuncInModel(Node f, bool p); - /** get number of commands to report in a model */ - size_t getNumModelCommands() const; - /** get model command at index i */ - const NodeCommand* getModelCommand(size_t i) const; private: /** Fully inited */ bool d_fullyInited; - - /** - * A list of commands that should be in the Model globally (i.e., - * regardless of push/pop). Only maintained if produce-models option - * is on. - */ - std::vector> d_modelGlobalCommands; - - /** - * A list of commands that should be in the Model locally (i.e., - * it is context-dependent on push/pop). Only maintained if - * produce-models option is on. - */ - CommandList d_modelCommands; - /** - * A list of model commands allocated to d_modelCommands at any time. This - * is maintained for memory management purposes. - */ - std::vector> d_modelCommandsAlloc; - /** * A vector of declaration commands waiting to be dumped out. * Once the SmtEngine is fully initialized, we'll dump them. diff --git a/src/smt/model.cpp b/src/smt/model.cpp index b734ad9e9..8a9f944d2 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -26,29 +26,17 @@ namespace CVC4 { namespace smt { -Model::Model(SmtEngine& smt, theory::TheoryModel* tm) - : d_smt(smt), d_isKnownSat(false), d_tmodel(tm) +Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm) { Assert(d_tmodel != nullptr); } std::ostream& operator<<(std::ostream& out, const Model& m) { - smt::SmtScope smts(&m.d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, m); return out; } -size_t Model::getNumCommands() const -{ - return d_smt.getDumpManager()->getNumModelCommands(); -} - -const NodeCommand* Model::getCommand(size_t i) const -{ - return d_smt.getDumpManager()->getModelCommand(i); -} - theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; } const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; } diff --git a/src/smt/model.h b/src/smt/model.h index 0913922d1..18675040a 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -27,7 +27,6 @@ namespace CVC4 { class SmtEngine; -class NodeCommand; namespace smt { @@ -49,13 +48,9 @@ class Model { public: /** construct */ - Model(SmtEngine& smt, theory::TheoryModel* tm); + Model(theory::TheoryModel* tm); /** virtual destructor */ ~Model() {} - /** get the smt engine that this model is hooked up to */ - SmtEngine* getSmtEngine() { return &d_smt; } - /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ - const SmtEngine* getSmtEngine() const { return &d_smt; } /** get the input name (file name, etc.) this model is associated to */ std::string getInputName() const { return d_inputName; } /** @@ -77,10 +72,6 @@ class Model { /** Does this model have approximations? */ bool hasApproximations() const; //----------------------- end helper methods - /** get number of commands to report */ - size_t getNumCommands() const; - /** get command */ - const NodeCommand* getCommand(size_t i) const; //----------------------- model declarations /** Clear the current model declarations. */ void clearModelDeclarations(); @@ -100,8 +91,6 @@ class Model { const std::vector& getDeclaredTerms() const; //----------------------- end model declarations protected: - /** The SmtEngine we're associated with */ - SmtEngine& d_smt; /** the input name (file name, etc.) this model is associated to */ std::string d_inputName; /** diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 91184d27d..815f99132 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -51,9 +51,7 @@ DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id, TypeNode type) : d_id(id), d_fun(expr), - d_type(type), - d_printInModel(true), - d_printInModelSetByUser(false) + d_type(type) { } @@ -72,22 +70,6 @@ NodeCommand* DeclareFunctionNodeCommand::clone() const const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; } -bool DeclareFunctionNodeCommand::getPrintInModel() const -{ - return d_printInModel; -} - -bool DeclareFunctionNodeCommand::getPrintInModelSetByUser() const -{ - return d_printInModelSetByUser; -} - -void DeclareFunctionNodeCommand::setPrintInModel(bool p) -{ - d_printInModel = p; - d_printInModelSetByUser = true; -} - /* -------------------------------------------------------------------------- */ /* class DeclareTypeNodeCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/node_command.h b/src/smt/node_command.h index 8cf9a5e10..e1a15e62c 100644 --- a/src/smt/node_command.h +++ b/src/smt/node_command.h @@ -68,16 +68,11 @@ class DeclareFunctionNodeCommand : public NodeCommand OutputLanguage language = language::output::LANG_AUTO) const override; NodeCommand* clone() const override; const Node& getFunction() const; - bool getPrintInModel() const; - bool getPrintInModelSetByUser() const; - void setPrintInModel(bool p); private: std::string d_id; Node d_fun; TypeNode d_type; - bool d_printInModel; - bool d_printInModelSetByUser; }; /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 161c2eba6..0f40db530 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -243,7 +243,7 @@ void SmtEngine::finishInit() TheoryModel* tm = te->getModel(); if (tm != nullptr) { - d_model.reset(new Model(*this, tm)); + d_model.reset(new Model(tm)); // make the check models utility d_checkModels.reset(new CheckModels(*d_smtSolver.get())); }