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.
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
#include "options/smt_options.h"
#include "options/uf_options.h"
+#include "smt/dump_manager.h"
#include "theory/rewriter.h"
#include "theory/sort_inference.h"
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<const Node, Node>& 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
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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<Command*, CommandCleanup> CommandList;
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* CVC4__SMT__COMMAND_LIST_H */
--- /dev/null
+/********************* */
+/*! \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<Command>(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<Command>(cc));
+ }
+ }
+ if (Dump.isOn(dumpTag))
+ {
+ if (d_fullyInited)
+ {
+ Dump(dumpTag) << c;
+ }
+ else
+ {
+ d_dumpCommands.push_back(std::unique_ptr<Command>(c.clone()));
+ }
+ }
+}
+
+void DumpManager::setPrintFuncInModel(Node f, bool p)
+{
+ Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
+ for (std::unique_ptr<Command>& c : d_modelGlobalCommands)
+ {
+ DeclareFunctionCommand* dfc =
+ dynamic_cast<DeclareFunctionCommand*>(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<DeclareFunctionCommand*>(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
--- /dev/null
+/********************* */
+/*! \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 <memory>
+#include <vector>
+
+#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<Command*> 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<std::unique_ptr<Command>> 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<std::unique_ptr<Command>> 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<std::unique_ptr<Command>> d_dumpCommands;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
#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"
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);
}
}
tn.toType());
if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
{
- d_smt.addToModelCommandAndDump(c);
+ d_dm.addToModelCommandAndDump(c);
}
}
types.push_back(dt.toType());
}
DatatypeDeclarationCommand c(types);
- d_smt.addToModelCommandAndDump(c);
+ d_dm.addToModelCommandAndDump(c);
}
}
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);
}
}
}
if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
{
- d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
+ d_dm.addToModelCommandAndDump(c, flags, false, "skolems");
}
}
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 */
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
#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"
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 */
#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"
namespace smt {
-struct DeleteCommandFunction : public std::unary_function<const Command*, void>
-{
- void operator()(const Command* command) { delete command; }
-};
-
-void DeleteAndClearCommandVector(std::vector<Command*>& 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
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),
d_abductSolver(nullptr),
d_assertionList(nullptr),
d_assignments(nullptr),
- d_modelGlobalCommands(),
- d_modelCommands(nullptr),
- d_dumpCommands(),
d_defineCommands(),
d_logic(),
d_originalOptions(),
#endif
d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
- d_modelCommands = new (true) smt::CommandList(getUserContext());
}
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())
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
#endif
d_absValues.reset(nullptr);
+ d_dumpm.reset(nullptr);
d_theoryEngine.reset(nullptr);
d_propEngine.reset(nullptr);
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()) {
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;
// (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;
}
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();
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<d_modelGlobalCommands.size(); i++ ){
- Command * c = d_modelGlobalCommands[i];
- DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
- if(dfc != NULL) {
- if( dfc->getFunction()==f ){
- dfc->setPrintInModel( p );
- }
- }
- }
- for( unsigned i=0; i<d_modelCommands->size(); i++ ){
- Command * c = (*d_modelCommands)[i];
- DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(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
return d_resourceManager.get();
}
+DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
+
void SmtEngine::setSygusConjectureStale()
{
if (d_private->d_sygusConjectureStale)
namespace smt {
/** Utilities */
class AbstractValues;
+class DumpManager;
class ResourceOutListener;
class SmtNodeManagerListener;
class OptionsManager;
class ProcessAssertions;
ProofManager* currentProofManager();
-
-struct CommandCleanup;
-typedef context::CDList<Command*, CommandCleanup> CommandList;
}/* CVC4::smt namespace */
/* -------------------------------------------------------------------------- */
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;
const std::vector<Expr>& expr_values,
const std::string& str_value);
- /** Set print function in model. */
- void setPrintFuncInModel(Expr f, bool p);
-
/**
* Get expression name.
*
/** Get the resource manager of this SMT engine */
ResourceManager* getResourceManager();
+ /** Permit access to the underlying dump manager. */
+ smt::DumpManager* getDumpManager();
+
/**
* Get expanded assertions.
*
NodeManager* d_nodeManager;
/** Abstract values */
std::unique_ptr<smt::AbstractValues> d_absValues;
+ /** The dump manager */
+ std::unique_ptr<smt::DumpManager> d_dumpm;
/** Resource out listener */
std::unique_ptr<smt::ResourceOutListener> d_routListener;
/** Node manager listener */
*/
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<Command*> 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<Command*> d_dumpCommands;
-
/**
* A vector of command definitions to be imported in the new
* SmtEngine when checking unsat-cores.
projects / cvc5.git / commitdiff