(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.

1 files changed, 10 insertions, 10 deletions

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 8d2a1540c..1884d3890 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/builtin/proof_checker.h"
 
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -63,9 +63,9 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
 
 Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr)
 {
-  Node nk = ProofSkolemCache::getSkolemForm(n);
+  Node nk = SkolemManager::getSkolemForm(n);
   Node nkr = applyRewriteExternal(nk, idr);
-  return ProofSkolemCache::getWitnessForm(nkr);
+  return SkolemManager::getWitnessForm(nkr);
 }
 
 Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
@@ -74,27 +74,27 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids)
   {
     return Node::null();
   }
-  Node nk = ProofSkolemCache::getSkolemForm(n);
+  Node nk = SkolemManager::getSkolemForm(n);
   Node nks = applySubstitutionExternal(nk, exp, ids);
-  return ProofSkolemCache::getWitnessForm(nks);
+  return SkolemManager::getWitnessForm(nks);
 }
 
 Node BuiltinProofRuleChecker::applySubstitution(Node n,
                                                 const std::vector<Node>& exp,
                                                 MethodId ids)
 {
-  Node nk = ProofSkolemCache::getSkolemForm(n);
+  Node nk = SkolemManager::getSkolemForm(n);
   Node nks = applySubstitutionExternal(nk, exp, ids);
-  return ProofSkolemCache::getWitnessForm(nks);
+  return SkolemManager::getWitnessForm(nks);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
     Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
 {
-  Node nk = ProofSkolemCache::getSkolemForm(n);
+  Node nk = SkolemManager::getSkolemForm(n);
   Node nks = applySubstitutionExternal(nk, exp, ids);
   Node nksr = applyRewriteExternal(nks, idr);
-  return ProofSkolemCache::getWitnessForm(nksr);
+  return SkolemManager::getWitnessForm(nksr);
 }
 
 Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr)
@@ -122,7 +122,7 @@ Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n,
                                                         MethodId ids)
 {
   Assert(!exp.isNull());
-  Node expk = ProofSkolemCache::getSkolemForm(exp);
+  Node expk = SkolemManager::getSkolemForm(exp);
   TNode var, subs;
   if (ids == MethodId::SB_DEFAULT)
   {