(proof-new) Use bound variable manager (#5679)

This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.

This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 1dd495ba2..1e70dd766 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -43,6 +43,7 @@ namespace CVC4 {
 class StatisticsRegistry;
 class ResourceManager;
 class SkolemManager;
+class BoundVarManager;
 
 class DType;
 
@@ -108,7 +109,9 @@ class NodeManager {
   StatisticsRegistry* d_statisticsRegistry;
 
   /** The skolem manager */
-  std::shared_ptr<SkolemManager> d_skManager;
+  std::unique_ptr<SkolemManager> d_skManager;
+  /** The bound variable manager */
+  std::unique_ptr<BoundVarManager> d_bvManager;
 
   NodeValuePool d_nodeValuePool;
 
@@ -386,6 +389,8 @@ class NodeManager {
   static NodeManager* currentNM() { return s_current; }
   /** Get this node manager's skolem manager */
   SkolemManager* getSkolemManager() { return d_skManager.get(); }
+  /** Get this node manager's bound variable manager */
+  BoundVarManager* getBoundVarManager() { return d_bvManager.get(); }
 
   /** Get this node manager's statistics registry */
   StatisticsRegistry* getStatisticsRegistry() const