This moves listener classes owned by SmtEngine to their own file.
The SmtEnginePrivate class previously what itself a NodeManagerListener. This class will be deleted. Instead a new NodeManagerListener is introduced here whose sole responsibility is to do the work required for node manager listening.
Note I had to add a (temporary) friend relationship to SmtEngine, which will be removed in an upcoming PR to split the management of dumping to its own utility.
smt/defined_function.h
smt/dump.cpp
smt/dump.h
+ smt/listeners.cpp
+ smt/listeners.h
smt/logic_exception.h
smt/logic_request.cpp
smt/logic_request.h
--- /dev/null
+/********************* */
+/*! \file listeners.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 Implements listener classes for SMT engine.
+ **/
+
+#include "smt/listeners.h"
+
+#include "expr/attribute.h"
+#include "expr/expr.h"
+#include "expr/node_manager_attributes.h"
+#include "options/smt_options.h"
+#include "smt/command.h"
+#include "smt/dump.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace smt {
+
+ResourceOutListener::ResourceOutListener(SmtEngine& smt) : d_smt(smt) {}
+
+void ResourceOutListener::notify()
+{
+ SmtScope scope(&d_smt);
+ Assert(smt::smtEngineInScope());
+ d_smt.interrupt();
+}
+
+SmtNodeManagerListener::SmtNodeManagerListener(SmtEngine& smt) : d_smt(smt) {}
+
+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);
+ }
+}
+
+void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn,
+ uint32_t flags)
+{
+ DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
+ tn.getAttribute(expr::SortArityAttr()),
+ tn.toType());
+ if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
+ {
+ d_smt.addToModelCommandAndDump(c);
+ }
+}
+
+void SmtNodeManagerListener::nmNotifyNewDatatypes(
+ const std::vector<DatatypeType>& dtts, uint32_t flags)
+{
+ if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
+ {
+ std::vector<Type> types(dtts.begin(), dtts.end());
+ DatatypeDeclarationCommand c(types);
+ d_smt.addToModelCommandAndDump(c);
+ }
+}
+
+void SmtNodeManagerListener::nmNotifyNewVar(TNode n, uint32_t flags)
+{
+ DeclareFunctionCommand c(
+ n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType());
+ if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
+ {
+ d_smt.addToModelCommandAndDump(c, flags);
+ }
+}
+
+void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
+ const std::string& comment,
+ uint32_t flags)
+{
+ std::string id = n.getAttribute(expr::VarNameAttr());
+ DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
+ if (Dump.isOn("skolems") && comment != "")
+ {
+ Dump("skolems") << CommentCommand(id + " is " + comment);
+ }
+ if ((flags & ExprManager::VAR_FLAG_DEFINED) == 0)
+ {
+ d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
+ }
+}
+
+} // namespace smt
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file listeners.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 Listener classes for SMT engine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__LISTENERS_H
+#define CVC4__SMT__LISTENERS_H
+
+#include <vector>
+
+#include "base/listener.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/** A listener for resource outs */
+class ResourceOutListener : public Listener
+{
+ public:
+ ResourceOutListener(SmtEngine& smt);
+ /** notify method, interupts SmtEngine */
+ void notify() override;
+
+ private:
+ /** Reference to the SmtEngine */
+ SmtEngine& d_smt;
+};
+
+/**
+ * A listener for node manager calls, which impacts certain dumping traces.
+ */
+class SmtNodeManagerListener : public NodeManagerListener
+{
+ public:
+ SmtNodeManagerListener(SmtEngine& smt);
+ /** Notify when new sort is created */
+ void nmNotifyNewSort(TypeNode tn, uint32_t flags) override;
+ /** Notify when new sort constructor is created */
+ void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override;
+ /** Notify when list of datatypes is created */
+ void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
+ uint32_t flags) override;
+ /** Notify when new variable is created */
+ void nmNotifyNewVar(TNode n, uint32_t flags) override;
+ /** Notify when new skolem is created */
+ void nmNotifyNewSkolem(TNode n,
+ const std::string& comment,
+ uint32_t flags) override;
+ /** Notify when a term is deleted */
+ void nmNotifyDeleteNode(TNode n) override {}
+
+ private:
+ /** Reference to the smt engine */
+ SmtEngine& d_smt;
+};
+
+} // namespace smt
+} // namespace CVC4
+
+#endif
#include "base/configuration.h"
#include "base/configuration_private.h"
#include "base/exception.h"
-#include "base/listener.h"
#include "base/modal_exception.h"
#include "base/output.h"
#include "context/cdhashmap.h"
#include "smt/command.h"
#include "smt/command_list.h"
#include "smt/defined_function.h"
+#include "smt/listeners.h"
#include "smt/logic_request.h"
#include "smt/model_blocker.h"
#include "smt/model_core_builder.h"
commands.clear();
}
-class ResourceOutListener : public Listener {
- public:
- ResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
- void notify() override
- {
- SmtScope scope(d_smt);
- Assert(smt::smtEngineInScope());
- d_smt->interrupt();
- }
- private:
- SmtEngine* d_smt;
-}; /* class ResourceOutListener */
-
/**
* 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
* one) becomes an "interface shell" which simply acts as a forwarder
* of method calls.
*/
-class SmtEnginePrivate : public NodeManagerListener {
+class SmtEnginePrivate
+{
SmtEngine& d_smt;
typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
- /**
- * Manager for limiting time and abstract resource usage.
- */
- ResourceManager* d_resourceManager;
-
- /** Resource out listener */
- std::unique_ptr<ResourceOutListener> d_routListener;
-
/** A circuit propagator for non-clausal propositional deduction */
booleans::CircuitPropagator d_propagator;
public:
SmtEnginePrivate(SmtEngine& smt)
: d_smt(smt),
- d_routListener(new ResourceOutListener(d_smt)),
d_propagator(true, true),
d_assertions(),
d_assertionsProcessed(smt.getUserContext(), false),
d_iteRemover(smt.getUserContext()),
d_sygusConjectureStale(smt.getUserContext(), true)
{
- d_smt.d_nodeManager->subscribeEvents(this);
d_true = NodeManager::currentNM()->mkConst(true);
- ResourceManager* rm = d_smt.getResourceManager();
- rm->registerListener(d_routListener.get());
}
~SmtEnginePrivate()
d_propagator.finish();
d_propagator.setNeedsFinish(false);
}
- d_smt.d_nodeManager->unsubscribeEvents(this);
}
void spendResource(ResourceManager::Resource r)
ProcessAssertions* getProcessAssertions() { return &d_processor; }
- void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
- {
- DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
- 0,
- tn.toType());
- if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) {
- d_smt.addToModelCommandAndDump(c, flags);
- }
- }
-
- void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override
- {
- DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
- tn.getAttribute(expr::SortArityAttr()),
- tn.toType());
- if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0)
- {
- d_smt.addToModelCommandAndDump(c);
- }
- }
-
- void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts,
- uint32_t flags) override
- {
- if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0)
- {
- std::vector<Type> types(dtts.begin(), dtts.end());
- DatatypeDeclarationCommand c(types);
- d_smt.addToModelCommandAndDump(c);
- }
- }
-
- void nmNotifyNewVar(TNode n, uint32_t flags) override
- {
- DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
- n.toExpr(),
- n.getType().toType());
- if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
- d_smt.addToModelCommandAndDump(c, flags);
- }
- }
-
- void nmNotifyNewSkolem(TNode n,
- const std::string& comment,
- uint32_t flags) override
- {
- string id = n.getAttribute(expr::VarNameAttr());
- DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
- if(Dump.isOn("skolems") && comment != "") {
- Dump("skolems") << CommentCommand(id + " is " + comment);
- }
- if((flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
- d_smt.addToModelCommandAndDump(c, flags, false, "skolems");
- }
- }
-
- void nmNotifyDeleteNode(TNode n) override {}
-
Node applySubstitutions(TNode node)
{
return Rewriter::rewrite(
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
d_absValues(new AbstractValues(d_nodeManager)),
+ d_routListener(new ResourceOutListener(*this)),
+ d_snmListener(new SmtNodeManagerListener(*this)),
d_theoryEngine(nullptr),
d_propEngine(nullptr),
d_proofManager(nullptr),
new ResourceManager(*d_statisticsRegistry.get(), d_options));
d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
d_private.reset(new smt::SmtEnginePrivate(*this));
+ // listen to node manager events
+ d_nodeManager->subscribeEvents(d_snmListener.get());
+ // listen to resource out
+ d_resourceManager->registerListener(d_routListener.get());
+ // make statistics
d_stats.reset(new SmtEngineStatistics());
// The ProofManager is constructed before any other proof objects such as
d_stats.reset(nullptr);
d_private.reset(nullptr);
+ d_nodeManager->unsubscribeEvents(d_snmListener.get());
+ d_snmListener.reset(nullptr);
+ d_routListener.reset(nullptr);
d_optm.reset(nullptr);
// d_resourceManager must be destroyed before d_statisticsRegistry
d_resourceManager.reset(nullptr);
namespace smt {
/** Utilities */
class AbstractValues;
+class ResourceOutListener;
+class SmtNodeManagerListener;
class OptionsManager;
/** Subsolvers */
class AbductionSolver;
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;
NodeManager* d_nodeManager;
/** Abstract values */
std::unique_ptr<smt::AbstractValues> d_absValues;
+ /** Resource out listener */
+ std::unique_ptr<smt::ResourceOutListener> d_routListener;
+ /** Node manager listener */
+ std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
/** The theory engine */
std::unique_ptr<TheoryEngine> d_theoryEngine;
projects / cvc5.git / commitdiff