Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)

This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.

This PR also eliminates some unused code in TheoryArithPrivate.

Followup PRs will start formalizing/eliminating calls to mkDummySkolem.

5 files changed, 36 insertions, 19 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index b67df285d..bbe100e98 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/emptyset.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/sets_options.h"
 #include "smt/logic_exception.h"
 #include "theory/rewriter.h"
@@ -1015,6 +1016,7 @@ void CardinalityExtension::mkModelValueElementsFor(
       std::uint32_t vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
       Assert(els.size() <= vu);
       NodeManager* nm = NodeManager::currentNM();
+      SkolemManager* sm = nm->getSkolemManager();
       if (elementType.isInterpretedFinite())
       {
         // get all members of this finite type
@@ -1034,7 +1036,7 @@ void CardinalityExtension::mkModelValueElementsFor(
           // slack elements for the leaves without worrying about conflicts with
           // the current members of this finite type.
 
-          Node slack = nm->mkSkolem("slack", elementType);
+          Node slack = sm->mkDummySkolem("slack", elementType);
           Node singleton = nm->mkSingleton(elementType, slack);
           els.push_back(singleton);
           d_finite_type_slack_elements[elementType].push_back(slack);
@@ -1043,8 +1045,8 @@ void CardinalityExtension::mkModelValueElementsFor(
         }
         else
         {
-          els.push_back(
-              nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
+          els.push_back(nm->mkSingleton(
+              elementType, sm->mkDummySkolem("msde", elementType)));
         }
       }
     }
diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index c18e9406d..8c0d125d5 100644
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/sets/skolem_cache.h"
 
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 
 using namespace cvc5::kind;
@@ -49,7 +50,8 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
 
 Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c)
 {
-  Node n = NodeManager::currentNM()->mkSkolem(c, tn, "sets skolem");
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node n = sm->mkDummySkolem(c, tn, "sets skolem");
   d_allSkolems.insert(n);
   return n;
 }
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index a093840f7..43eed46a6 100644
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -15,6 +15,7 @@
 #include "theory/sets/term_registry.h"
 
 #include "expr/emptyset.h"
+#include "expr/skolem_manager.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -116,7 +117,8 @@ Node TermRegistry::getTypeConstraintSkolem(Node n, TypeNode tn)
   std::map<TypeNode, Node>::iterator it = d_tc_skolem[n].find(tn);
   if (it == d_tc_skolem[n].end())
   {
-    Node k = NodeManager::currentNM()->mkSkolem("tc_k", tn);
+    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+    Node k = sm->mkDummySkolem("tc_k", tn);
     d_tc_skolem[n][tn] = k;
     return k;
   }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index b97d3125d..3aa97672d 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1373,11 +1373,12 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
   }
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType());
   stringstream stream;
   stream << "chooseUf" << setType.getId();
   string name = stream.str();
-  Node chooseSkolem = nm->mkSkolem(
+  Node chooseSkolem = sm->mkDummySkolem(
       name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
   d_chooseFunctions[setType] = chooseSkolem;
   return chooseSkolem;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 6609e4923..aa79f903b 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -15,8 +15,10 @@
  **/
 
 #include "theory/sets/theory_sets_rels.h"
-#include "theory/sets/theory_sets_private.h"
+
+#include "expr/skolem_manager.h"
 #include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
 
 using namespace std;
 using namespace cvc5::kind;
@@ -361,11 +363,11 @@ void TheorySetsRels::check(Theory::Effort level)
   }
 
   /* JOIN-IMAGE DOWN  : (x) IS_IN (R JOIN_IMAGE n)
-  *                     -------------------------------------------------------
-  *                     (x, x1) IS_IN R .... (x, xn) IS_IN R  DISTINCT(x1, ... , xn)
-  *
-  */
-
+   *                     -------------------------------------------------------
+   *                     (x, x1) IS_IN R .... (x, xn) IS_IN R  DISTINCT(x1, ...
+   * , xn)
+   *
+   */
   void TheorySetsRels::applyJoinImageRule( Node mem_rep, Node join_image_term, Node exp ) {
     Trace("rels-debug") << "\n[Theory::Rels] *********** applyJoinImageRule on " << join_image_term
                         << " with mem_rep = " << mem_rep  << " and exp = " << exp << std::endl;
@@ -387,29 +389,37 @@ void TheorySetsRels::check(Theory::Effort level)
         }
       }
     }
-
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Node reason = exp;
     Node conclusion = d_trueNode;
     std::vector< Node > distinct_skolems;
     Node fst_mem_element = RelsUtils::nthElementOfTuple( exp[0], 0 );
 
     if( exp[1] != join_image_term ) {
-      reason = NodeManager::currentNM()->mkNode( kind::AND, reason, NodeManager::currentNM()->mkNode( kind::EQUAL, exp[1], join_image_term ) );
+      reason =
+          nm->mkNode(AND, reason, nm->mkNode(EQUAL, exp[1], join_image_term));
     }
     for( unsigned int i = 0; i < min_card; i++ ) {
-      Node skolem = NodeManager::currentNM()->mkSkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0] );
+      Node skolem = sm->mkDummySkolem(
+          "jig", join_image_rel.getType()[0].getTupleTypes()[0]);
       distinct_skolems.push_back( skolem );
-      conclusion = NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::MEMBER, RelsUtils::constructPair( join_image_rel, fst_mem_element, skolem ), join_image_rel ) );
+      conclusion = nm->mkNode(
+          AND,
+          conclusion,
+          nm->mkNode(
+              MEMBER,
+              RelsUtils::constructPair(join_image_rel, fst_mem_element, skolem),
+              join_image_rel));
     }
     if( distinct_skolems.size() >= 2 ) {
-      conclusion =  NodeManager::currentNM()->mkNode( kind::AND, conclusion, NodeManager::currentNM()->mkNode( kind::DISTINCT, distinct_skolems ) );
+      conclusion =
+          nm->mkNode(AND, conclusion, nm->mkNode(DISTINCT, distinct_skolems));
     }
     sendInfer(conclusion, InferenceId::SETS_RELS_JOIN_IMAGE_DOWN, reason);
     Trace("rels-debug") << "\n[Theory::Rels] *********** Done with applyJoinImageRule ***********" << std::endl;
-
   }
 
-
   /* IDENTITY-DOWN  : (x, y) IS_IN IDEN(R)
   *               -------------------------------------------------------
   *                   x = y,  (x IS_IN R)