summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-06-05 10:19:10 -0500
committerGitHub <noreply@github.com>2020-06-05 10:19:10 -0500
commite9c29bb348bd8fab5cedc48ab96ce2a0e6f98078 (patch)
treebd23e59f1cefd4cd7bf062130e978327d33a8c55 /src/expr/node_manager.h
parent7aa98fa461932db12c05820e685772d2aa983993 (diff)
(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.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h20
1 files changed, 13 insertions, 7 deletions
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<SkolemManager> 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.
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback