From 0f040cbc2b068d3f22f6d46ec35aff3ab720ec28 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 31 Jul 2020 07:19:35 -0500 Subject: [PATCH] Split listener classes from SmtEngine (#4816) 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. --- src/CMakeLists.txt | 2 + src/smt/listeners.cpp | 99 ++++++++++++++++++++++++++++++++++++++++++ src/smt/listeners.h | 75 ++++++++++++++++++++++++++++++++ src/smt/smt_engine.cpp | 99 ++++++------------------------------------ src/smt/smt_engine.h | 8 ++++ 5 files changed, 197 insertions(+), 86 deletions(-) create mode 100644 src/smt/listeners.cpp create mode 100644 src/smt/listeners.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 59b559cb2..53d049411 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -230,6 +230,8 @@ libcvc4_add_sources( 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 diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp new file mode 100644 index 000000000..5cfbfd1c5 --- /dev/null +++ b/src/smt/listeners.cpp @@ -0,0 +1,99 @@ +/********************* */ +/*! \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& dtts, uint32_t flags) +{ + if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0) + { + std::vector 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 diff --git a/src/smt/listeners.h b/src/smt/listeners.h new file mode 100644 index 000000000..1eba41228 --- /dev/null +++ b/src/smt/listeners.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \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 + +#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& 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d8657c7dd..5d34e6fa2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -34,7 +34,6 @@ #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" @@ -86,6 +85,7 @@ #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" @@ -147,19 +147,6 @@ void DeleteAndClearCommandVector(std::vector& commands) { 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 @@ -174,20 +161,13 @@ class ResourceOutListener : public Listener { * 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 NodeToNodeHashMap; typedef unordered_map NodeToBoolHashMap; - /** - * Manager for limiting time and abstract resource usage. - */ - ResourceManager* d_resourceManager; - - /** Resource out listener */ - std::unique_ptr d_routListener; - /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; @@ -240,7 +220,6 @@ class SmtEnginePrivate : public NodeManagerListener { public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), - d_routListener(new ResourceOutListener(d_smt)), d_propagator(true, true), d_assertions(), d_assertionsProcessed(smt.getUserContext(), false), @@ -249,10 +228,7 @@ class SmtEnginePrivate : public NodeManagerListener { 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() @@ -261,7 +237,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_propagator.finish(); d_propagator.setNeedsFinish(false); } - d_smt.d_nodeManager->unsubscribeEvents(this); } void spendResource(ResourceManager::Resource r) @@ -271,64 +246,6 @@ class SmtEnginePrivate : public NodeManagerListener { 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& dtts, - uint32_t flags) override - { - if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0) - { - std::vector 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( @@ -421,6 +338,8 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) 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), @@ -474,6 +393,11 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) 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 @@ -690,6 +614,9 @@ SmtEngine::~SmtEngine() 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); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a651b8d1e..f260a307b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -93,6 +93,8 @@ namespace prop { namespace smt { /** Utilities */ class AbstractValues; +class ResourceOutListener; +class SmtNodeManagerListener; class OptionsManager; /** Subsolvers */ class AbductionSolver; @@ -146,6 +148,8 @@ class CVC4_PUBLIC SmtEngine 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; @@ -1122,6 +1126,10 @@ class CVC4_PUBLIC SmtEngine NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; + /** Resource out listener */ + std::unique_ptr d_routListener; + /** Node manager listener */ + std::unique_ptr d_snmListener; /** The theory engine */ std::unique_ptr d_theoryEngine; -- 2.30.2