From 5a3569cbeba6c53c157f4fb8e88016c5a501cafb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 3 Aug 2020 09:40:52 -0500 Subject: [PATCH] Split dump manager from SmtEngine (#4824) Towards splitting SmtEngine. This moves utilities related to managing information for dumping to its own utility, DumpManager. Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work. --- src/CMakeLists.txt | 4 +- src/preprocessing/passes/sort_infer.cpp | 7 +- src/smt/command_list.cpp | 30 ----- src/smt/command_list.h | 39 ------- src/smt/dump_manager.cpp | 140 ++++++++++++++++++++++++ src/smt/dump_manager.h | 106 ++++++++++++++++++ src/smt/listeners.cpp | 13 ++- src/smt/listeners.h | 8 +- src/smt/model.cpp | 18 ++- src/smt/smt_engine.cpp | 100 ++--------------- src/smt/smt_engine.h | 37 +------ 11 files changed, 288 insertions(+), 214 deletions(-) delete mode 100644 src/smt/command_list.cpp delete mode 100644 src/smt/command_list.h create mode 100644 src/smt/dump_manager.cpp create mode 100644 src/smt/dump_manager.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 53d049411..61261afe4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -225,11 +225,11 @@ libcvc4_add_sources( smt/abstract_values.h smt/command.cpp smt/command.h - smt/command_list.cpp - smt/command_list.h smt/defined_function.h smt/dump.cpp smt/dump.h + smt/dump_manager.cpp + smt/dump_manager.h smt/listeners.cpp smt/listeners.h smt/logic_exception.h diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 92c2e55b1..03f0469bf 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -16,6 +16,7 @@ #include "options/smt_options.h" #include "options/uf_options.h" +#include "smt/dump_manager.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" @@ -65,12 +66,12 @@ PreprocessingPassResult SortInferencePass::applyInternal( assertionsToPreprocess->push_back(nar); } // indicate correspondence between the functions - // TODO (#2308): move this to a better place SmtEngine* smt = smt::currentSmtEngine(); + smt::DumpManager* dm = smt->getDumpManager(); for (const std::pair& mrf : model_replace_f) { - smt->setPrintFuncInModel(mrf.first.toExpr(), false); - smt->setPrintFuncInModel(mrf.second.toExpr(), true); + dm->setPrintFuncInModel(mrf.first, false); + dm->setPrintFuncInModel(mrf.second, true); } } // only need to compute monotonicity on the resulting formula if we are diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp deleted file mode 100644 index a88efbbec..000000000 --- a/src/smt/command_list.cpp +++ /dev/null @@ -1,30 +0,0 @@ -/********************* */ -/*! \file command_list.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** 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 A context-sensitive list of Commands, and their cleanup - ** - ** A context-sensitive list of Commands, and their cleanup. - **/ - -// we include both of these to make sure they agree on the typedef -#include "smt/command.h" -#include "smt/command_list.h" -#include "smt/smt_engine.h" - -namespace CVC4 { -namespace smt { - -void CommandCleanup::operator()(Command** c) { - delete *c; -} - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ diff --git a/src/smt/command_list.h b/src/smt/command_list.h deleted file mode 100644 index cdc8e4c22..000000000 --- a/src/smt/command_list.h +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file command_list.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner - ** 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 A context-sensitive list of Commands, and their cleanup - ** - ** A context-sensitive list of Commands, and their cleanup. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__SMT__COMMAND_LIST_H -#define CVC4__SMT__COMMAND_LIST_H - -#include "context/cdlist.h" - -namespace CVC4 { - -class Command; - -namespace smt { - -struct CommandCleanup { - void operator()(Command** c); -};/* struct CommandCleanup */ - -typedef context::CDList CommandList; - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__SMT__COMMAND_LIST_H */ diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp new file mode 100644 index 000000000..b8525f24e --- /dev/null +++ b/src/smt/dump_manager.cpp @@ -0,0 +1,140 @@ +/********************* */ +/*! \file dump_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 Implementation of the dump manager. + **/ + +#include "smt/dump_manager.h" + +#include "expr/expr_manager.h" +#include "options/smt_options.h" +#include "smt/dump.h" + +namespace CVC4 { +namespace smt { + +DumpManager::DumpManager(context::UserContext* u) + : d_modelGlobalCommands(), d_modelCommands(u), d_dumpCommands() +{ +} + +DumpManager::~DumpManager() +{ + d_dumpCommands.clear(); + d_modelCommandsAlloc.clear(); + d_modelGlobalCommands.clear(); +} + +void DumpManager::finishInit() +{ + Trace("smt-debug") << "Dump declaration commands..." << std::endl; + // dump out any pending declaration commands + for (size_t i = 0, ncoms = d_dumpCommands.size(); i < ncoms; ++i) + { + Dump("declarations") << *d_dumpCommands[i]; + } + d_dumpCommands.clear(); + + d_fullyInited = true; +} + +void DumpManager::resetAssertions() { d_modelGlobalCommands.clear(); } + +void DumpManager::addToModelCommandAndDump(const Command& c, + uint32_t flags, + bool userVisible, + 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 + { + Command* 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) + { + Dump(dumpTag) << c; + } + else + { + d_dumpCommands.push_back(std::unique_ptr(c.clone())); + } + } +} + +void DumpManager::setPrintFuncInModel(Node f, bool p) +{ + Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; + for (std::unique_ptr& c : d_modelGlobalCommands) + { + DeclareFunctionCommand* dfc = + dynamic_cast(c.get()); + if (dfc != NULL) + { + Node df = Node::fromExpr(dfc->getFunction()); + if (df == f) + { + dfc->setPrintInModel(p); + } + } + } + for (Command* c : d_modelCommands) + { + DeclareFunctionCommand* dfc = dynamic_cast(c); + if (dfc != NULL) + { + Node df = Node::fromExpr(dfc->getFunction()); + if (df == f) + { + dfc->setPrintInModel(p); + } + } + } +} + +size_t DumpManager::getNumModelCommands() const +{ + return d_modelCommands.size() + d_modelGlobalCommands.size(); +} + +const Command* 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()]; +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h new file mode 100644 index 000000000..6f2ee37a1 --- /dev/null +++ b/src/smt/dump_manager.h @@ -0,0 +1,106 @@ +/********************* */ +/*! \file dump_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 dump manager of the SmtEngine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__DUMP_MANAGER_H +#define CVC4__SMT__DUMP_MANAGER_H + +#include +#include + +#include "context/cdlist.h" +#include "expr/node.h" +#include "smt/command.h" + +namespace CVC4 { +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. + */ +class DumpManager +{ + typedef context::CDList CommandList; + + public: + DumpManager(context::UserContext* u); + ~DumpManager(); + /** + * Finish init, called during SmtEngine::finishInit, which is triggered + * when initialization of options is finished. + */ + void finishInit(); + /** + * Reset assertions, called on SmtEngine::resetAssertions. + */ + void resetAssertions(); + /** + * Add to Model command. This is used for recording a command + * that should be reported during a get-model call. + */ + void addToModelCommandAndDump(const Command& c, + uint32_t flags = 0, + bool userVisible = true, + const char* dumpTag = "declarations"); + + /** + * 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 Command* 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. + * This ensures the declarations come after the set-logic and + * any necessary set-option commands are dumped. + */ + std::vector> d_dumpCommands; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 452894f62..41602dab2 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -20,6 +20,7 @@ #include "options/smt_options.h" #include "smt/command.h" #include "smt/dump.h" +#include "smt/dump_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -35,14 +36,14 @@ void ResourceOutListener::notify() d_smt.interrupt(); } -SmtNodeManagerListener::SmtNodeManagerListener(SmtEngine& smt) : d_smt(smt) {} +SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm) : d_dm(dm) {} void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags) { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { - d_smt.addToModelCommandAndDump(c, flags); + d_dm.addToModelCommandAndDump(c, flags); } } @@ -54,7 +55,7 @@ void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn, tn.toType()); if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { - d_smt.addToModelCommandAndDump(c); + d_dm.addToModelCommandAndDump(c); } } @@ -70,7 +71,7 @@ void SmtNodeManagerListener::nmNotifyNewDatatypes( types.push_back(dt.toType()); } DatatypeDeclarationCommand c(types); - d_smt.addToModelCommandAndDump(c); + d_dm.addToModelCommandAndDump(c); } } @@ -80,7 +81,7 @@ void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags) n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - d_smt.addToModelCommandAndDump(c, flags); + d_dm.addToModelCommandAndDump(c, flags); } } @@ -96,7 +97,7 @@ void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n, } if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - d_smt.addToModelCommandAndDump(c, flags, false, "skolems"); + d_dm.addToModelCommandAndDump(c, flags, false, "skolems"); } } diff --git a/src/smt/listeners.h b/src/smt/listeners.h index 6054d13af..77d6d257f 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -41,13 +41,15 @@ class ResourceOutListener : public Listener SmtEngine& d_smt; }; +class DumpManager; + /** * A listener for node manager calls, which impacts certain dumping traces. */ class SmtNodeManagerListener : public NodeManagerListener { public: - SmtNodeManagerListener(SmtEngine& smt); + SmtNodeManagerListener(DumpManager& dm); /** Notify when new sort is created */ void nmNotifyNewSort(TypeNode tn, uint32_t flags) override; /** Notify when new sort constructor is created */ @@ -65,8 +67,8 @@ class SmtNodeManagerListener : public NodeManagerListener void nmNotifyDeleteNode(TNode n) override {} private: - /** Reference to the smt engine */ - SmtEngine& d_smt; + /** Reference to the dump manager of smt engine */ + DumpManager& d_dm; }; } // namespace smt diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 6f6a09f38..7924698ff 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -20,7 +20,7 @@ #include "options/base_options.h" #include "printer/printer.h" #include "smt/command.h" -#include "smt/command_list.h" +#include "smt/dump_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -37,18 +37,14 @@ std::ostream& operator<<(std::ostream& out, const Model& m) { Model::Model() : d_smt(*smt::currentSmtEngine()), d_isKnownSat(false) {} -size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); +size_t Model::getNumCommands() const +{ + return d_smt.getDumpManager()->getNumModelCommands(); } -const Command* Model::getCommand(size_t i) const { - Assert(i < getNumCommands()); - // index the global commands first, then the locals - if(i < d_smt.d_modelGlobalCommands.size()) { - return d_smt.d_modelGlobalCommands[i]; - } else { - return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; - } +const Command* Model::getCommand(size_t i) const +{ + return d_smt.getDumpManager()->getModelCommand(i); } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5d34e6fa2..f114dba7c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -83,8 +83,8 @@ #include "smt/abduction_solver.h" #include "smt/abstract_values.h" #include "smt/command.h" -#include "smt/command_list.h" #include "smt/defined_function.h" +#include "smt/dump_manager.h" #include "smt/listeners.h" #include "smt/logic_request.h" #include "smt/model_blocker.h" @@ -137,16 +137,6 @@ extern const char* const plf_signatures; namespace smt { -struct DeleteCommandFunction : public std::unary_function -{ - void operator()(const Command* command) { delete command; } -}; - -void DeleteAndClearCommandVector(std::vector& commands) { - std::for_each(commands.begin(), commands.end(), DeleteCommandFunction()); - commands.clear(); -} - /** * This is an inelegant solution, but for the present, it will work. * The point of this is to separate the public and private portions of @@ -338,8 +328,9 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), d_absValues(new AbstractValues(d_nodeManager)), + d_dumpm(new DumpManager(d_userContext.get())), d_routListener(new ResourceOutListener(*this)), - d_snmListener(new SmtNodeManagerListener(*this)), + d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())), d_theoryEngine(nullptr), d_propEngine(nullptr), d_proofManager(nullptr), @@ -348,9 +339,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_abductSolver(nullptr), d_assertionList(nullptr), d_assignments(nullptr), - d_modelGlobalCommands(), - d_modelCommands(nullptr), - d_dumpCommands(), d_defineCommands(), d_logic(), d_originalOptions(), @@ -413,7 +401,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) #endif d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); - d_modelCommands = new (true) smt::CommandList(getUserContext()); } void SmtEngine::finishInit() @@ -495,13 +482,8 @@ void SmtEngine::finishInit() everything.getLogicString()); } - Trace("smt-debug") << "Dump declaration commands..." << std::endl; - // dump out any pending declaration commands - for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { - Dump("declarations") << *d_dumpCommands[i]; - delete d_dumpCommands[i]; - } - d_dumpCommands.clear(); + // initialize the dump manager + d_dumpm->finishInit(); // subsolvers if (options::produceAbducts()) @@ -579,18 +561,6 @@ SmtEngine::~SmtEngine() d_assertionList->deleteSelf(); } - for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { - delete d_dumpCommands[i]; - d_dumpCommands[i] = NULL; - } - d_dumpCommands.clear(); - - DeleteAndClearCommandVector(d_modelGlobalCommands); - - if(d_modelCommands != NULL) { - d_modelCommands->deleteSelf(); - } - d_definedFunctions->deleteSelf(); //destroy all passes before destroying things that they refer to @@ -608,6 +578,7 @@ SmtEngine::~SmtEngine() #endif d_absValues.reset(nullptr); + d_dumpm.reset(nullptr); d_theoryEngine.reset(nullptr); d_propEngine.reset(nullptr); @@ -950,7 +921,7 @@ void SmtEngine::defineFunction(Expr func, language::SetLanguage::getLanguage(Dump.getStream())) << func; DefineFunctionCommand c(ss.str(), func, formals, formula, global); - addToModelCommandAndDump( + d_dumpm->addToModelCommandAndDump( c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); PROOF(if (options::checkUnsatCores()) { @@ -2050,35 +2021,6 @@ vector> SmtEngine::getAssignment() return res; } -void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) { - Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl; - SmtScope smts(this); - // 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(/* userVisible && */ - (!d_fullyInited || options::produceModels()) && - (flags & ExprManager::VAR_FLAG_DEFINED) == 0) { - if(flags & ExprManager::VAR_FLAG_GLOBAL) { - d_modelGlobalCommands.push_back(c.clone()); - } else { - d_modelCommands->push_back(c.clone()); - } - } - if(Dump.isOn(dumpTag)) { - if(d_fullyInited) { - Dump(dumpTag) << c; - } else { - d_dumpCommands.push_back(c.clone()); - } - } -} - // TODO(#1108): Simplify the error reporting of this method. Model* SmtEngine::getModel() { Trace("smt") << "SMT getModel()" << endl; @@ -3078,7 +3020,7 @@ void SmtEngine::resetAssertions() // (see solver execution modes in the SMT-LIB standard) Assert(d_context->getLevel() == 0); Assert(d_userContext->getLevel() == 0); - DeleteAndClearCommandVector(d_modelGlobalCommands); + d_dumpm->resetAssertions(); return; } @@ -3100,7 +3042,7 @@ void SmtEngine::resetAssertions() Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1); d_context->popto(0); d_userContext->popto(0); - DeleteAndClearCommandVector(d_modelGlobalCommands); + d_dumpm->resetAssertions(); d_userContext->push(); d_context->push(); @@ -3177,28 +3119,6 @@ void SmtEngine::setUserAttribute(const std::string& attr, d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value); } -void SmtEngine::setPrintFuncInModel(Expr f, bool p) { - Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; - for( unsigned i=0; i(c); - if(dfc != NULL) { - if( dfc->getFunction()==f ){ - dfc->setPrintInModel( p ); - } - } - } - for( unsigned i=0; isize(); i++ ){ - Command * c = (*d_modelCommands)[i]; - DeclareFunctionCommand* dfc = dynamic_cast(c); - if(dfc != NULL) { - if( dfc->getFunction()==f ){ - dfc->setPrintInModel( p ); - } - } - } -} - void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) { // Always check whether the SmtEngine has been initialized (which is done @@ -3317,6 +3237,8 @@ ResourceManager* SmtEngine::getResourceManager() return d_resourceManager.get(); } +DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); } + void SmtEngine::setSygusConjectureStale() { if (d_private->d_sygusConjectureStale) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f260a307b..99b993e7b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -93,6 +93,7 @@ namespace prop { namespace smt { /** Utilities */ class AbstractValues; +class DumpManager; class ResourceOutListener; class SmtNodeManagerListener; class OptionsManager; @@ -112,9 +113,6 @@ class SmtScope; class ProcessAssertions; ProofManager* currentProofManager(); - -struct CommandCleanup; -typedef context::CDList CommandList; }/* CVC4::smt namespace */ /* -------------------------------------------------------------------------- */ @@ -147,9 +145,6 @@ class CVC4_PUBLIC SmtEngine friend class ::CVC4::smt::ProcessAssertions; friend ProofManager* ::CVC4::smt::currentProofManager(); friend class ::CVC4::LogicRequest; - friend class ::CVC4::Model; // to access d_modelCommands - friend class ::CVC4::smt::SmtNodeManagerListener; // to access - // addToModelCommandAndDump friend class ::CVC4::theory::TheoryModel; friend class ::CVC4::theory::Rewriter; @@ -857,9 +852,6 @@ class CVC4_PUBLIC SmtEngine const std::vector& expr_values, const std::string& str_value); - /** Set print function in model. */ - void setPrintFuncInModel(Expr f, bool p); - /** * Get expression name. * @@ -883,6 +875,9 @@ class CVC4_PUBLIC SmtEngine /** Get the resource manager of this SMT engine */ ResourceManager* getResourceManager(); + /** Permit access to the underlying dump manager. */ + smt::DumpManager* getDumpManager(); + /** * Get expanded assertions. * @@ -1126,6 +1121,8 @@ class CVC4_PUBLIC SmtEngine NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; + /** The dump manager */ + std::unique_ptr d_dumpm; /** Resource out listener */ std::unique_ptr d_routListener; /** Node manager listener */ @@ -1178,28 +1175,6 @@ class CVC4_PUBLIC SmtEngine */ AssignmentSet* d_assignments; - /** - * 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. - */ - smt::CommandList* d_modelCommands; - - /** - * A vector of declaration commands waiting to be dumped out. - * Once the SmtEngine is fully initialized, we'll dump them. - * This ensures the declarations come after the set-logic and - * any necessary set-option commands are dumped. - */ - std::vector d_dumpCommands; - /** * A vector of command definitions to be imported in the new * SmtEngine when checking unsat-cores. -- 2.30.2