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.

7 files changed, 66 insertions, 35 deletions

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 3302be018..48c0e9f00 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "expr/type_matcher.h"
 
 using namespace cvc5::kind;
@@ -882,10 +883,11 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
   NodeManager* nm = NodeManager::currentNM();
   std::stringstream ss;
   ss << "sel_" << index;
-  s = nm->mkSkolem(ss.str(),
-                   nm->mkSelectorType(dtt, t),
-                   "is a shared selector",
-                   NodeManager::SKOLEM_NO_NOTIFY);
+  SkolemManager* sm = nm->getSkolemManager();
+  s = sm->mkDummySkolem(ss.str(),
+                        nm->mkSelectorType(dtt, t),
+                        "is a shared selector",
+                        NodeManager::SKOLEM_NO_NOTIFY);
   d_sharedSel[dtt][t][index] = s;
   Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t
                          << std::endl;
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index ce15c7ede..927c48dda 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -15,6 +15,7 @@
 
 #include "expr/dtype.h"
 #include "expr/node_manager.h"
+#include "expr/skolem_manager.h"
 #include "expr/type_matcher.h"
 #include "options/datatypes_options.h"
 
@@ -45,8 +46,8 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
   // create the proper selector type)
   Assert(!isResolved());
   Assert(!selectorType.isNull());
-
-  Node type = NodeManager::currentNM()->mkSkolem(
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
+  Node type = sm->mkDummySkolem(
       "unresolved_" + selectorName,
       selectorType,
       "is an unresolved selector type placeholder",
@@ -505,6 +506,7 @@ bool DTypeConstructor::resolve(
                      << std::endl;
 
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   size_t index = 0;
   std::vector<TypeNode> argTypes;
   Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
@@ -523,7 +525,7 @@ bool DTypeConstructor::resolve(
       {
         Trace("datatypes-init") << "  ...self selector" << std::endl;
         range = self;
-        arg->d_selector = nm->mkSkolem(
+        arg->d_selector = sm->mkDummySkolem(
             argName,
             nm->mkSelectorType(self, self),
             "is a selector",
@@ -544,7 +546,7 @@ bool DTypeConstructor::resolve(
         {
           Trace("datatypes-init") << "  ...resolved selector" << std::endl;
           range = (*j).second;
-          arg->d_selector = nm->mkSkolem(
+          arg->d_selector = sm->mkDummySkolem(
               argName,
               nm->mkSelectorType(self, range),
               "is a selector",
@@ -574,7 +576,7 @@ bool DTypeConstructor::resolve(
       }
       Trace("datatypes-init")
           << "  ...range after parametric substitution " << range << std::endl;
-      arg->d_selector = nm->mkSkolem(
+      arg->d_selector = sm->mkDummySkolem(
           argName,
           nm->mkSelectorType(self, range),
           "is a selector",
@@ -603,12 +605,12 @@ bool DTypeConstructor::resolve(
   // The name of the tester variable does not matter, it is only used
   // internally.
   std::string testerName("is_" + d_name);
-  d_tester = nm->mkSkolem(
+  d_tester = sm->mkDummySkolem(
       testerName,
       nm->mkTesterType(self),
       "is a tester",
       NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
-  d_constructor = nm->mkSkolem(
+  d_constructor = sm->mkDummySkolem(
       getName(),
       nm->mkConstructorType(argTypes, self),
       "is a constructor",
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a72eada23..465ddf588 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -87,6 +87,7 @@ class NodeManager
   friend class api::Solver;
   friend class expr::NodeValue;
   friend class expr::TypeChecker;
+  friend class SkolemManager;
 
   friend class NodeBuilder;
   friend class NodeManagerScope;
@@ -366,7 +367,7 @@ class NodeManager
    * lookup is done on the name.  If you mkVar("a", type) and then
    * mkVar("a", type) again, you have two variables.  The NodeManager
    * version of this is private to avoid internal uses of mkVar() from
-   * within CVC4.  Such uses should employ mkSkolem() instead.
+   * within CVC4.  Such uses should employ SkolemManager::mkSkolem() instead.
    */
   Node mkVar(const std::string& name, const TypeNode& type);
   Node* mkVarPtr(const std::string& name, const TypeNode& type);
@@ -375,6 +376,19 @@ class NodeManager
   Node mkVar(const TypeNode& type);
   Node* mkVarPtr(const TypeNode& type);
 
+  /**
+   * Create a skolem constant with the given name, type, and comment. For
+   * details, see SkolemManager::mkDummySkolem, which calls this method.
+   *
+   * This method is intentionally private. To create skolems, one should
+   * call a method from SkolemManager for allocating a skolem in a standard
+   * way, or otherwise use SkolemManager::mkDummySkolem.
+   */
+  Node mkSkolem(const std::string& prefix,
+                const TypeNode& type,
+                const std::string& comment = "",
+                int flags = SKOLEM_DEFAULT);
+
  public:
   explicit NodeManager();
   ~NodeManager();
@@ -578,27 +592,6 @@ class NodeManager
     SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
   };                         /* enum SkolemFlags */
 
-  /**
-   * Create a skolem constant with the given name, type, and comment.
-   *
-   * @param prefix the name of the new skolem variable is the prefix
-   * appended with a unique ID.  This way a family of skolem variables
-   * can be made with unique identifiers, used in dump, tracing, and
-   * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
-   * a unique ID appended and use prefix as the name.
-   *
-   * @param type the type of the skolem variable to create
-   *
-   * @param comment a comment for dumping output; if declarations are
-   * being dumped, this is included in a comment before the declaration
-   * and can be quite useful for debugging
-   *
-   * @param flags an optional mask of bits from SkolemFlags to control
-   * mkSkolem() behavior
-   */
-  Node mkSkolem(const std::string& prefix, const TypeNode& type,
-                const std::string& comment = "", int flags = SKOLEM_DEFAULT);
-
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
 
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index a823d5b60..8ca8810b1 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -204,6 +204,14 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id, TypeNode tn, Node cacheVal)
   return it->second;
 }
 
+Node SkolemManager::mkDummySkolem(const std::string& prefix,
+                                  const TypeNode& type,
+                                  const std::string& comment,
+                                  int flags)
+{
+  return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
+}
+
 Node SkolemManager::mkBooleanTermVariable(Node t)
 {
   return mkPurifySkolem(t, "", "", NodeManager::SKOLEM_BOOL_TERM_VAR);
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 1295b2249..6cebee5d9 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -228,6 +228,28 @@ class SkolemManager
                         TypeNode tn,
                         Node cacheVal = Node::null());
   /**
+   * Create a skolem constant with the given name, type, and comment. This
+   * should only be used if the definition of the skolem does not matter.
+   * The definition of a skolem matters e.g. when the skolem is used in a
+   * proof.
+   *
+   * @param prefix the name of the new skolem variable is the prefix
+   * appended with a unique ID.  This way a family of skolem variables
+   * can be made with unique identifiers, used in dump, tracing, and
+   * debugging output.  Use SKOLEM_EXACT_NAME flag if you don't want
+   * a unique ID appended and use prefix as the name.
+   * @param type the type of the skolem variable to create
+   * @param comment a comment for dumping output; if declarations are
+   * being dumped, this is included in a comment before the declaration
+   * and can be quite useful for debugging
+   * @param flags an optional mask of bits from SkolemFlags to control
+   * mkSkolem() behavior
+   */
+  Node mkDummySkolem(const std::string& prefix,
+                     const TypeNode& type,
+                     const std::string& comment = "",
+                     int flags = NodeManager::SKOLEM_DEFAULT);
+  /**
    * Make Boolean term variable for term t. This is a special case of
    * mkPurifySkolem above, where the returned term has kind
    * BOOLEAN_TERM_VARIABLE.
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index c2138499b..8c1d67c47 100644
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -16,6 +16,7 @@
 
 #include <sstream>
 
+#include "expr/skolem_manager.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
@@ -44,8 +45,9 @@ Node Subs::getSubs(Node v) const
 
 void Subs::add(Node v)
 {
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
   // default, use a fresh skolem of the same type
-  Node s = NodeManager::currentNM()->mkSkolem("sk", v.getType());
+  Node s = sm->mkDummySkolem("sk", v.getType());
   add(v, s);
 }
 
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index 929c8a97c..82585eabe 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -15,6 +15,7 @@
 #include "expr/sygus_datatype.h"
 
 #include <sstream>
+#include "expr/skolem_manager.h"
 
 using namespace cvc5::kind;
 
@@ -38,8 +39,9 @@ void SygusDatatype::addConstructor(Node op,
 
 void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
 {
+  SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
   // add an "any constant" proxy variable
-  Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
+  Node av = sm->mkDummySkolem("_any_constant", tn);
   // mark that it represents any constant
   SygusAnyConstAttribute saca;
   av.setAttribute(saca, true);