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

4 files changed, 26 insertions, 24 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3ff3966cc..443aaa9b7 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -34,7 +34,7 @@
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"  // for incrementalSolving()
 #include "preprocessing/util/ite_utilities.h"
@@ -1178,6 +1178,7 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n)
 Node TheoryArithPrivate::eliminateOperators(Node node)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
 
   Kind k = node.getKind();
   switch (k)
@@ -1206,9 +1207,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
         Node zero = mkRationalNode(0);
         Node diff = nm->mkNode(kind::MINUS, node[0], v);
         Node lem = mkInRange(diff, zero, one);
-        toIntSkolem = ProofSkolemCache::mkSkolem(
+        toIntSkolem = sm->mkSkolem(
             v, lem, "toInt", "a conversion of a Real term to its Integer part");
-        toIntSkolem = ProofSkolemCache::getWitnessForm(toIntSkolem);
+        toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem);
         d_to_int_skolem[node[0]] = toIntSkolem;
       }
       else
@@ -1303,9 +1304,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
                               nm->mkNode(
                                   PLUS, v, nm->mkConst(Rational(-1))))))));
         }
-        intVar = ProofSkolemCache::mkSkolem(
+        intVar = sm->mkSkolem(
             v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
-        intVar = ProofSkolemCache::getWitnessForm(intVar);
+        intVar = SkolemManager::getWitnessForm(intVar);
         d_int_div_skolem[rw] = intVar;
       }
       else
@@ -1345,9 +1346,9 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
         Node lem = nm->mkNode(IMPLIES,
                               den.eqNode(nm->mkConst(Rational(0))).negate(),
                               nm->mkNode(MULT, den, v).eqNode(num));
-        var = ProofSkolemCache::mkSkolem(
+        var = sm->mkSkolem(
             v, lem, "nonlinearDiv", "the result of a non-linear div term");
-        var = ProofSkolemCache::getWitnessForm(var);
+        var = SkolemManager::getWitnessForm(var);
         d_div_skolem[rw] = var;
       }
       else
@@ -1490,12 +1491,12 @@ Node TheoryArithPrivate::eliminateOperators(Node node)
           lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
         }
         Assert(!lem.isNull());
-        Node ret = ProofSkolemCache::mkSkolem(
+        Node ret = sm->mkSkolem(
             var,
             lem,
             "tfk",
             "Skolem to eliminate a non-standard transcendental function");
-        ret = ProofSkolemCache::getWitnessForm(ret);
+        ret = SkolemManager::getWitnessForm(ret);
         d_nlin_inverse_skolem[node] = ret;
         return ret;
       }
@@ -4269,8 +4270,8 @@ bool TheoryArithPrivate::needsCheckLastEffort() {
   }
 }
 
-Node TheoryArithPrivate::explain(TNode n) {
-
+Node TheoryArithPrivate::explain(TNode n)
+{
   Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
 
   ConstraintP c = d_constraintDatabase.lookup(n);
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)
   {
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 4af75f1cc..85a948567 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -82,12 +82,13 @@ Node SkolemCache::mkTypedSkolemCached(
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   Node sk;
   switch (id)
   {
     // exists k. k = a
     case SK_PURIFY:
-      sk = ProofSkolemCache::mkPurifySkolem(a, c, "string purify skolem");
+      sk = sm->mkPurifySkolem(a, c, "string purify skolem");
       break;
     // these are eliminated by normalizeStringSkolem
     case SK_ID_V_SPT:
@@ -113,7 +114,7 @@ Node SkolemCache::mkTypedSkolemCached(
       Notice() << "Don't know how to handle Skolem ID " << id << std::endl;
       Node v = nm->mkBoundVar(tn);
       Node cond = nm->mkConst(true);
-      sk = ProofSkolemCache::mkSkolem(v, cond, c, "string skolem");
+      sk = sm->mkSkolem(v, cond, c, "string skolem");
     }
     break;
   }
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 0ebbb3277..7ce507f29 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -22,7 +22,7 @@
 #include <unordered_set>
 
 #include "expr/node.h"
-#include "expr/proof_skolem_cache.h"
+#include "expr/skolem_manager.h"
 
 namespace CVC4 {
 namespace theory {