From e9c29bb348bd8fab5cedc48ab96ce2a0e6f98078 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Jun 2020 10:19:10 -0500 Subject: (proof-new) Rename ProofSkolemCache to SkolemManager (#4556) This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing. This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form. Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler. Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal. --- src/expr/node_manager.h | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'src/expr/node_manager.h') diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1fab328e9..7fa2d147a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -42,6 +42,7 @@ namespace CVC4 { class StatisticsRegistry; class ResourceManager; +class SkolemManager; class DType; @@ -113,6 +114,9 @@ class NodeManager { ResourceManager* d_resourceManager; + /** The skolem manager */ + std::shared_ptr d_skManager; + /** * A list of registrations on d_options to that call into d_resourceManager. * These must be garbage collected before d_options and d_resourceManager. @@ -405,6 +409,8 @@ public: /** Get this node manager's resource manager */ ResourceManager* getResourceManager() { return d_resourceManager; } + /** Get this node manager's skolem manager */ + SkolemManager* getSkolemManager() { return d_skManager.get(); } /** Get this node manager's statistics registry */ StatisticsRegistry* getStatisticsRegistry() const @@ -539,13 +545,13 @@ public: * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT * cannot be composed in such a manner. */ - enum SkolemFlags { - SKOLEM_DEFAULT = 0, /**< default behavior */ - SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ - SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */ - SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ - };/* enum SkolemFlags */ - + enum SkolemFlags + { + SKOLEM_DEFAULT = 0, /**< default behavior */ + SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ + SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */ + SKOLEM_IS_GLOBAL = 4 /**< global vars appear in models even after a pop */ + }; /** * Create a skolem constant with the given name, type, and comment. * -- cgit v1.2.3