Refactor skolem construction (#7561)

This makes all methods for constructing skolems local to SkolemManager.

It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things:
(1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon.
(2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions.

This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.

20 files changed, 175 insertions, 221 deletions

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index d8ec0cb61..4a0ed994f 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -867,10 +867,7 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
   SkolemManager* sm = nm->getSkolemManager();
   TypeNode stype = nm->mkSelectorType(dtt, t);
   Node nindex = nm->mkConst(Rational(index));
-  s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR,
-                           stype,
-                           nindex,
-                           NodeManager::SKOLEM_NO_NOTIFY);
+  s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, stype, nindex);
   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 ddb88499b..f23cfa4f9 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -49,11 +49,10 @@ void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
   Assert(!isResolved());
   Assert(!selectorType.isNull());
   SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
-  Node sel = sm->mkDummySkolem(
-      "unresolved_" + selectorName,
-      selectorType,
-      "is an unresolved selector type placeholder",
-      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+  Node sel = sm->mkDummySkolem("unresolved_" + selectorName,
+                               selectorType,
+                               "is an unresolved selector type placeholder",
+                               SkolemManager::SKOLEM_EXACT_NAME);
   // can use null updater for now
   Node nullNode;
   Trace("datatypes") << "DTypeConstructor::addArg: " << sel << std::endl;
@@ -562,17 +561,15 @@ bool DTypeConstructor::resolve(
     }
     // Internally, selectors (and updaters) are fresh internal skolems which
     // we constructor via mkDummySkolem.
-    arg->d_selector = sm->mkDummySkolem(
-        argName,
-        nm->mkSelectorType(self, range),
-        "is a selector",
-        NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+    arg->d_selector = sm->mkDummySkolem(argName,
+                                        nm->mkSelectorType(self, range),
+                                        "is a selector",
+                                        SkolemManager::SKOLEM_EXACT_NAME);
     std::string updateName("update_" + argName);
-    arg->d_updater = sm->mkDummySkolem(
-        updateName,
-        nm->mkDatatypeUpdateType(self, range),
-        "is a selector",
-        NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+    arg->d_updater = sm->mkDummySkolem(updateName,
+                                       nm->mkDatatypeUpdateType(self, range),
+                                       "is a selector",
+                                       SkolemManager::SKOLEM_EXACT_NAME);
     // must set indices to ensure datatypes::utils::indexOf works
     arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex);
     arg->d_selector.setAttribute(DTypeIndexAttr(), index);
@@ -600,16 +597,14 @@ 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 = sm->mkDummySkolem(
-      testerName,
-      nm->mkTesterType(self),
-      "is a tester",
-      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
-  d_constructor = sm->mkDummySkolem(
-      getName(),
-      nm->mkConstructorType(argTypes, self),
-      "is a constructor",
-      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
+  d_tester = sm->mkDummySkolem(testerName,
+                               nm->mkTesterType(self),
+                               "is a tester",
+                               SkolemManager::SKOLEM_EXACT_NAME);
+  d_constructor = sm->mkDummySkolem(getName(),
+                                    nm->mkConstructorType(argTypes, self),
+                                    "is a constructor",
+                                    SkolemManager::SKOLEM_EXACT_NAME);
   Assert(d_constructor.getType().isConstructor());
   // associate constructor with all selectors
   for (std::shared_ptr<DTypeSelector> sel : d_args)
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a9e5854b0..3734e5860 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -100,8 +100,7 @@ NodeManager::NodeManager()
       d_attrManager(new expr::attr::AttributeManager()),
       d_nodeUnderDeletion(nullptr),
       d_inReclaimZombies(false),
-      d_abstractValueCount(0),
-      d_skolemCounter(0)
+      d_abstractValueCount(0)
 {
 }
 
@@ -503,25 +502,6 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
-Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) {
-  Node n = NodeBuilder(this, kind::SKOLEM);
-  setAttribute(n, TypeAttr(), type);
-  setAttribute(n, TypeCheckedAttr(), true);
-  if((flags & SKOLEM_EXACT_NAME) == 0) {
-    stringstream name;
-    name << prefix << '_' << ++d_skolemCounter;
-    setAttribute(n, expr::VarNameAttr(), name.str());
-  } else {
-    setAttribute(n, expr::VarNameAttr(), prefix);
-  }
-  if((flags & SKOLEM_NO_NOTIFY) == 0) {
-    for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-      (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL);
-    }
-  }
-  return n;
-}
-
 TypeNode NodeManager::mkBagType(TypeNode elementType)
 {
   CheckArgument(
@@ -1061,13 +1041,6 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
   return n;
 }
 
-Node NodeManager::mkBooleanTermVariable() {
-  Node n = NodeBuilder(this, kind::BOOLEAN_TERM_VARIABLE);
-  n.setAttribute(TypeAttr(), booleanType());
-  n.setAttribute(TypeCheckedAttr(), true);
-  return n;
-}
-
 Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b526efc80..5b5f07e6f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -72,8 +72,6 @@ class NodeManagerListener {
   {
   }
   virtual void nmNotifyNewVar(TNode n) {}
-  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
-                                 uint32_t flags) {}
   /**
    * Notify a listener of a Node that's being GCed.  If this function stores a
    * reference
@@ -212,15 +210,6 @@ class NodeManager
   unsigned d_abstractValueCount;
 
   /**
-   * A counter used to produce unique skolem names.
-   *
-   * Note that it is NOT incremented when skolems are created using
-   * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
-   * by this node manager.
-   */
-  unsigned d_skolemCounter;
-
-  /**
    * Look up a NodeValue in the pool associated to this NodeManager.
    * The NodeValue argument need not be a "completely-constructed"
    * NodeValue.  In particular, "non-inlined" constants are permitted
@@ -365,19 +354,6 @@ class NodeManager
   /** Create a variable with the given type. */
   Node mkVar(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:
   /**
    * Initialize the node manager by adding a null node to the pool and filling
@@ -555,27 +531,9 @@ class NodeManager
    */
   Node mkChain(Kind kind, const std::vector<Node>& children);
 
-  /**
-   * Optional flags used to control behavior of NodeManager::mkSkolem().
-   * They should be composed with a bitwise OR (e.g.,
-   * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
-   * cannot be composed in such a manner.
-   */
-  enum SkolemFlags
-  {
-    SKOLEM_DEFAULT = 0,    /**< default behavior */
-    SKOLEM_NO_NOTIFY = 1,  /**< do not notify subscribers */
-    SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
-    SKOLEM_IS_GLOBAL = 4,  /**< global vars appear in models even after a pop */
-    SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
-  };                         /* enum SkolemFlags */
-
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
 
-  /** Create a boolean term variable. */
-  Node mkBooleanTermVariable();
-
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);
 
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index e8651ea75..c1741beac 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -20,6 +20,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/node_algorithm.h"
+#include "expr/node_manager_attributes.h"
 
 using namespace cvc5::kind;
 
@@ -79,6 +80,8 @@ std::ostream& operator<<(std::ostream& out, SkolemFunId id)
   return out;
 }
 
+SkolemManager::SkolemManager() : d_skolemCounter(0) {}
+
 Node SkolemManager::mkSkolem(Node v,
                              Node pred,
                              const std::string& prefix,
@@ -217,10 +220,9 @@ Node SkolemManager::mkSkolemFunction(SkolemFunId id,
       d_skolemFuns.find(key);
   if (it == d_skolemFuns.end())
   {
-    NodeManager* nm = NodeManager::currentNM();
     std::stringstream ss;
     ss << "SKOLEM_FUN_" << id;
-    Node k = nm->mkSkolem(ss.str(), tn, "an internal skolem function", flags);
+    Node k = mkSkolemNode(ss.str(), tn, "an internal skolem function", flags);
     d_skolemFuns[key] = k;
     d_skolemFunMap[k] = key;
     return k;
@@ -264,7 +266,7 @@ Node SkolemManager::mkDummySkolem(const std::string& prefix,
                                   const std::string& comment,
                                   int flags)
 {
-  return NodeManager::currentNM()->mkSkolem(prefix, type, comment, flags);
+  return mkSkolemNode(prefix, type, comment, flags);
 }
 
 ProofGenerator* SkolemManager::getProofGenerator(Node t) const
@@ -367,25 +369,15 @@ Node SkolemManager::mkSkolemInternal(Node w,
                                      int flags)
 {
   // note that witness, original forms are independent, but share skolems
-  NodeManager* nm = NodeManager::currentNM();
   // w is not necessarily a witness term
   SkolemFormAttribute sfa;
-  Node k;
   // could already have a skolem if we used w already
   if (w.hasAttribute(sfa))
   {
     return w.getAttribute(sfa);
   }
   // make the new skolem
-  if (flags & NodeManager::SKOLEM_BOOL_TERM_VAR)
-  {
-    Assert (w.getType().isBoolean());
-    k = nm->mkBooleanTermVariable();
-  }
-  else
-  {
-    k = nm->mkSkolem(prefix, w.getType(), comment, flags);
-  }
+  Node k = mkSkolemNode(prefix, w.getType(), comment, flags);
   // set skolem form attribute for w
   w.setAttribute(sfa, k);
   Trace("sk-manager") << "SkolemManager::mkSkolem: " << k << " : " << w
@@ -393,4 +385,35 @@ Node SkolemManager::mkSkolemInternal(Node w,
   return k;
 }
 
+Node SkolemManager::mkSkolemNode(const std::string& prefix,
+                                 const TypeNode& type,
+                                 const std::string& comment,
+                                 int flags)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node n;
+  if (flags & SKOLEM_BOOL_TERM_VAR)
+  {
+    Assert(type.isBoolean());
+    n = NodeBuilder(nm, BOOLEAN_TERM_VARIABLE);
+  }
+  else
+  {
+    n = NodeBuilder(nm, SKOLEM);
+    if ((flags & SKOLEM_EXACT_NAME) == 0)
+    {
+      std::stringstream name;
+      name << prefix << '_' << ++d_skolemCounter;
+      n.setAttribute(expr::VarNameAttr(), name.str());
+    }
+    else
+    {
+      n.setAttribute(expr::VarNameAttr(), prefix);
+    }
+  }
+  n.setAttribute(expr::TypeAttr(), type);
+  n.setAttribute(expr::TypeCheckedAttr(), true);
+  return n;
+}
+
 }  // namespace cvc5
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 16cab62ca..0556185df 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -174,8 +174,21 @@ std::ostream& operator<<(std::ostream& out, SkolemFunId id);
 class SkolemManager
 {
  public:
-  SkolemManager() {}
+  SkolemManager();
   ~SkolemManager() {}
+
+  /**
+   * Optional flags used to control behavior of skolem creation.
+   * They should be composed with a bitwise OR (e.g.,
+   * "SKOLEM_BOOL_TERM_VAR | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
+   * cannot be composed in such a manner.
+   */
+  enum SkolemFlags
+  {
+    SKOLEM_DEFAULT = 0,    /**< default behavior */
+    SKOLEM_EXACT_NAME = 1, /**< do not make the name unique by adding the id */
+    SKOLEM_BOOL_TERM_VAR = 2 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
+  };
   /**
    * This makes a skolem of same type as bound variable v, (say its type is T),
    * whose definition is (witness ((v T)) pred). This definition is maintained
@@ -217,7 +230,7 @@ class SkolemManager
    * variable v.
    * @param prefix The prefix of the name of the Skolem
    * @param comment Debug information about the Skolem
-   * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+   * @param flags The flags for the Skolem (see SkolemFlags)
    * @param pg The proof generator for this skolem. If non-null, this proof
    * generator must respond to a call to getProofFor(exists v. pred) during
    * the lifetime of the current node manager.
@@ -227,7 +240,7 @@ class SkolemManager
                 Node pred,
                 const std::string& prefix,
                 const std::string& comment = "",
-                int flags = NodeManager::SKOLEM_DEFAULT,
+                int flags = SKOLEM_DEFAULT,
                 ProofGenerator* pg = nullptr);
   /**
    * Make skolemized form of existentially quantified formula q, and store its
@@ -255,7 +268,7 @@ class SkolemManager
    * @param skolems Vector to add Skolems of q to,
    * @param prefix The prefix of the name of each of the Skolems
    * @param comment Debug information about each of the Skolems
-   * @param flags The flags for the Skolem (see NodeManager::mkSkolem)
+   * @param flags The flags for the Skolem (see SkolemFlags)
    * @param pg The proof generator for this skolem. If non-null, this proof
    * generator must respond to a call to getProofFor(q) during
    * the lifetime of the current node manager.
@@ -265,7 +278,7 @@ class SkolemManager
                    std::vector<Node>& skolems,
                    const std::string& prefix,
                    const std::string& comment = "",
-                   int flags = NodeManager::SKOLEM_DEFAULT,
+                   int flags = SKOLEM_DEFAULT,
                    ProofGenerator* pg = nullptr);
   /**
    * Same as above, but for special case of (witness ((x T)) (= x t))
@@ -288,7 +301,7 @@ class SkolemManager
   Node mkPurifySkolem(Node t,
                       const std::string& prefix,
                       const std::string& comment = "",
-                      int flags = NodeManager::SKOLEM_DEFAULT);
+                      int flags = SKOLEM_DEFAULT);
   /**
    * Make skolem function. This method should be used for creating fixed
    * skolem functions of the forms described in SkolemFunId. The user of this
@@ -321,12 +334,12 @@ class SkolemManager
   Node mkSkolemFunction(SkolemFunId id,
                         TypeNode tn,
                         Node cacheVal = Node::null(),
-                        int flags = NodeManager::SKOLEM_DEFAULT);
+                        int flags = SKOLEM_DEFAULT);
   /** Same as above, with multiple cache values */
   Node mkSkolemFunction(SkolemFunId id,
                         TypeNode tn,
                         const std::vector<Node>& cacheVals,
-                        int flags = NodeManager::SKOLEM_DEFAULT);
+                        int flags = SKOLEM_DEFAULT);
   /**
    * Is k a skolem function? Returns true if k was generated by the above call.
    * Updates the arguments to the values used when constructing it.
@@ -348,12 +361,12 @@ class SkolemManager
    * 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
+   * skolem behavior
    */
   Node mkDummySkolem(const std::string& prefix,
                      const TypeNode& type,
                      const std::string& comment = "",
-                     int flags = NodeManager::SKOLEM_DEFAULT);
+                     int flags = SKOLEM_DEFAULT);
   /**
    * Get proof generator for existentially quantified formula q. This returns
    * the proof generator that was provided in a call to mkSkolem above.
@@ -386,11 +399,20 @@ class SkolemManager
    * Mapping from witness terms to proof generators.
    */
   std::map<Node, ProofGenerator*> d_gens;
+
+  /**
+   * A counter used to produce unique skolem names.
+   *
+   * Note that it is NOT incremented when skolems are created using
+   * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
+   * by this node manager.
+   */
+  size_t d_skolemCounter;
   /** Get or make skolem attribute for term w, which may be a witness term */
-  static Node mkSkolemInternal(Node w,
-                               const std::string& prefix,
-                               const std::string& comment,
-                               int flags);
+  Node mkSkolemInternal(Node w,
+                        const std::string& prefix,
+                        const std::string& comment,
+                        int flags);
   /**
    * Skolemize the first variable of existentially quantified formula q.
    * For example, calling this method on:
@@ -408,7 +430,18 @@ class SkolemManager
                  Node& qskolem,
                  const std::string& prefix,
                  const std::string& comment = "",
-                 int flags = NodeManager::SKOLEM_DEFAULT);
+                 int flags = SKOLEM_DEFAULT);
+  /**
+   * Create a skolem constant with the given name, type, and comment.
+   *
+   * This method is intentionally private. To create skolems, one should
+   * call a public method from SkolemManager for allocating a skolem in a
+   * proper way, or otherwise use SkolemManager::mkDummySkolem.
+   */
+  Node mkSkolemNode(const std::string& prefix,
+                    const TypeNode& type,
+                    const std::string& comment = "",
+                    int flags = SKOLEM_DEFAULT);
 };
 
 }  // namespace cvc5
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 8202acb15..d432d8ed1 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -76,18 +76,10 @@ MipLibTrick::MipLibTrick(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "miplib-trick"),
       d_statistics(statisticsRegistry())
 {
-  if (!options().base.incrementalSolving)
-  {
-    NodeManager::currentNM()->subscribeEvents(this);
-  }
 }
 
 MipLibTrick::~MipLibTrick()
 {
-  if (!options().base.incrementalSolving)
-  {
-    NodeManager::currentNM()->unsubscribeEvents(this);
-  }
 }
 
 /**
@@ -166,22 +158,34 @@ size_t MipLibTrick::removeFromConjunction(
   return 0;
 }
 
-void MipLibTrick::nmNotifyNewVar(TNode n)
+void MipLibTrick::collectBooleanVariables(
+    AssertionPipeline* assertionsToPreprocess)
 {
-  if (n.getType().isBoolean())
+  d_boolVars.clear();
+  std::unordered_set<TNode> visited;
+  std::unordered_set<TNode>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
-    d_boolVars.push_back(n);
+    visit.push_back((*assertionsToPreprocess)[i]);
   }
-}
-
-void MipLibTrick::nmNotifyNewSkolem(TNode n,
-                                    const std::string& comment,
-                                    uint32_t flags)
-{
-  if (n.getType().isBoolean())
+  do
   {
-    d_boolVars.push_back(n);
-  }
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar() && cur.getType().isBoolean())
+      {
+        d_boolVars.push_back(cur);
+      }
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
 }
 
 PreprocessingPassResult MipLibTrick::applyInternal(
@@ -191,6 +195,9 @@ PreprocessingPassResult MipLibTrick::applyInternal(
          == assertionsToPreprocess->size());
   Assert(!options().base.incrementalSolving);
 
+  // collect Boolean variables
+  collectBooleanVariables(assertionsToPreprocess);
+
   context::Context fakeContext;
   TheoryEngine* te = d_preprocContext->getTheoryEngine();
   booleans::CircuitPropagator* propagator =
@@ -529,8 +536,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
               Node newVar = sm->mkDummySkolem(
                   ss.str(),
                   nm->integerType(),
-                  "a variable introduced due to scrubbing a miplib encoding",
-                  NodeManager::SKOLEM_EXACT_NAME);
+                  "a variable introduced due to scrubbing a miplib encoding");
               Node geq = rewrite(nm->mkNode(kind::GEQ, newVar, zero));
               Node leq = rewrite(nm->mkNode(kind::LEQ, newVar, one));
               TrustNode tgeq = TrustNode::mkTrustLemma(geq, nullptr);
diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index 796063b46..65779f90d 100644
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -25,18 +25,12 @@ namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
-class MipLibTrick : public PreprocessingPass, public NodeManagerListener
+class MipLibTrick : public PreprocessingPass
 {
  public:
   MipLibTrick(PreprocessingPassContext* preprocContext);
   ~MipLibTrick();
 
-  // NodeManagerListener callbacks to collect d_boolVars.
-  void nmNotifyNewVar(TNode n) override;
-  void nmNotifyNewSkolem(TNode n,
-                         const std::string& comment,
-                         uint32_t flags) override;
-
  protected:
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
@@ -51,6 +45,10 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener
 
   size_t removeFromConjunction(
       Node& n, const std::unordered_set<unsigned long>& toRemove);
+  /**
+   * Collect Boolean variables in the given pipeline, store them in d_boolVars.
+   */
+  void collectBooleanVariables(AssertionPipeline* assertionsToPreprocess);
 
   Statistics d_statistics;
 
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index de6368951..7a1951d95 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -89,19 +89,5 @@ void SmtNodeManagerListener::nmNotifyNewVar(TNode n)
   d_dm.addToDump(c);
 }
 
-void SmtNodeManagerListener::nmNotifyNewSkolem(TNode n,
-                                               const std::string& comment,
-                                               uint32_t flags)
-{
-  std::string id = n.getAttribute(expr::VarNameAttr());
-  DeclareFunctionNodeCommand c(id, n, n.getType());
-  if (Dump.isOn("skolems") && comment != "")
-  {
-    d_outMgr.getPrinter().toStreamCmdSetInfo(
-        d_outMgr.getDumpOut(), "notes", id + " is " + comment);
-  }
-  d_dm.addToDump(c, "skolems");
-}
-
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index 60ec6b4ed..df99f8008 100644
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -61,10 +61,6 @@ class SmtNodeManagerListener : public NodeManagerListener
                             uint32_t flags) override;
   /** Notify when new variable is created */
   void nmNotifyNewVar(TNode n) override;
-  /** Notify when new skolem is created */
-  void nmNotifyNewSkolem(TNode n,
-                         const std::string& comment,
-                         uint32_t flags) override;
   /** Notify when a term is deleted */
   void nmNotifyDeleteNode(TNode n) override {}
 
diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 07100576d..c633ecb63 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -439,7 +439,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node,
           node,
           "btvK",
           "a Boolean term variable introduced during term formula removal",
-          NodeManager::SKOLEM_BOOL_TERM_VAR);
+          SkolemManager::SKOLEM_BOOL_TERM_VAR);
       d_skolem_cache.insert(node, skolem);
 
       // The new assertion
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 6b1749305..a3dd77fd1 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -38,8 +38,7 @@ CadSolver::CadSolver(Env& env, InferenceManager& im, NlModel& model)
 {
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
-  d_ranVariable = sm->mkDummySkolem(
-      "__z", nm->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
+  d_ranVariable = sm->mkDummySkolem("__z", nm->realType(), "");
 #ifdef CVC5_POLY_IMP
   if (env.isTheoryProofProducing())
   {
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 90f4a2cc7..afbb9b70f 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -462,8 +462,8 @@ Node OperatorElim::mkWitnessTerm(Node v,
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
   // we mark that we should send a lemma
-  Node k =
-      sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this);
+  Node k = sm->mkSkolem(
+      v, pred, prefix, comment, SkolemManager::SKOLEM_DEFAULT, this);
   if (d_pnm != nullptr)
   {
     Node lem = SkolemLemma::getSkolemLemmaFor(k);
diff --git a/src/theory/fp/fp_expand_defs.cpp b/src/theory/fp/fp_expand_defs.cpp
index a499b9666..de86626af 100644
--- a/src/theory/fp/fp_expand_defs.cpp
+++ b/src/theory/fp/fp_expand_defs.cpp
@@ -50,11 +50,8 @@ Node FpExpandDefs::minUF(Node node)
     args[0] = t;
     args[1] = t;
     fun = sm->mkDummySkolem("floatingpoint_min_zero_case",
-                            nm->mkFunctionType(args,
-                                               nm->mkBitVectorType(1U)
-                                                   ),
-                            "floatingpoint_min_zero_case",
-                            NodeManager::SKOLEM_EXACT_NAME);
+                            nm->mkFunctionType(args, nm->mkBitVectorType(1U)),
+                            "floatingpoint_min_zero_case");
     d_minMap.insert(t, fun);
   }
   else
@@ -84,11 +81,8 @@ Node FpExpandDefs::maxUF(Node node)
     args[0] = t;
     args[1] = t;
     fun = sm->mkDummySkolem("floatingpoint_max_zero_case",
-                            nm->mkFunctionType(args,
-                                               nm->mkBitVectorType(1U)
-                                                   ),
-                            "floatingpoint_max_zero_case",
-                            NodeManager::SKOLEM_EXACT_NAME);
+                            nm->mkFunctionType(args, nm->mkBitVectorType(1U)),
+                            "floatingpoint_max_zero_case");
     d_maxMap.insert(t, fun);
   }
   else
@@ -121,8 +115,7 @@ Node FpExpandDefs::toUBVUF(Node node)
     args[1] = source;
     fun = sm->mkDummySkolem("floatingpoint_to_ubv_out_of_range_case",
                             nm->mkFunctionType(args, target),
-                            "floatingpoint_to_ubv_out_of_range_case",
-                            NodeManager::SKOLEM_EXACT_NAME);
+                            "floatingpoint_to_ubv_out_of_range_case");
     d_toUBVMap.insert(p, fun);
   }
   else
@@ -155,8 +148,7 @@ Node FpExpandDefs::toSBVUF(Node node)
     args[1] = source;
     fun = sm->mkDummySkolem("floatingpoint_to_sbv_out_of_range_case",
                             nm->mkFunctionType(args, target),
-                            "floatingpoint_to_sbv_out_of_range_case",
-                            NodeManager::SKOLEM_EXACT_NAME);
+                            "floatingpoint_to_sbv_out_of_range_case");
     d_toSBVMap.insert(p, fun);
   }
   else
@@ -183,8 +175,7 @@ Node FpExpandDefs::toRealUF(Node node)
     args[0] = t;
     fun = sm->mkDummySkolem("floatingpoint_to_real_infinity_and_NaN_case",
                             nm->mkFunctionType(args, nm->realType()),
-                            "floatingpoint_to_real_infinity_and_NaN_case",
-                            NodeManager::SKOLEM_EXACT_NAME);
+                            "floatingpoint_to_real_infinity_and_NaN_case");
     d_toRealMap.insert(t, fun);
   }
   else
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 5af838354..b3033aedb 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -188,10 +188,8 @@ Node SygusUnifRl::purifyLemma(Node n,
       // Build purified head with fresh skolem and recreate node
       std::stringstream ss;
       ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++;
-      Node new_f = sm->mkDummySkolem(ss.str(),
-                                     nb[0].getType(),
-                                     "head of unif evaluation point",
-                                     NodeManager::SKOLEM_EXACT_NAME);
+      Node new_f = sm->mkDummySkolem(
+          ss.str(), nb[0].getType(), "head of unif evaluation point");
       // Adds new enumerator to map from candidate
       Trace("sygus-unif-rl-purify")
           << "...new enum " << new_f << " for candidate " << nb[0] << "\n";
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 324d6b7dc..a87466fab 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1407,8 +1407,7 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
   stringstream stream;
   stream << "chooseUf" << setType.getId();
   string name = stream.str();
-  Node chooseSkolem = sm->mkDummySkolem(
-      name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
+  Node chooseSkolem = sm->mkDummySkolem(name, chooseUf, "choose function");
   d_chooseFunctions[setType] = chooseSkolem;
   return chooseSkolem;
 }
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 60e6b6a01..fc68ddfc4 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -109,8 +109,8 @@ Node SkolemCache::mkTypedSkolemCached(
     {
       // for sequences of Booleans, we may purify Boolean terms, in which case
       // they must be Boolean term variables.
-      int flags = a.getType().isBoolean() ? NodeManager::SKOLEM_BOOL_TERM_VAR
-                                          : NodeManager::SKOLEM_DEFAULT;
+      int flags = a.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                          : SkolemManager::SKOLEM_DEFAULT;
       sk = sm->mkPurifySkolem(a, c, "string purify skolem", flags);
     }
     break;
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 5ad7010ed..b170ccbb6 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -532,13 +532,13 @@ TEST_F(TestNodeBlackNode, toString)
   TypeNode booleanType = d_nodeManager->booleanType();
 
   Node w = d_skolemManager->mkDummySkolem(
-      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "w", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node x = d_skolemManager->mkDummySkolem(
-      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "x", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node y = d_skolemManager->mkDummySkolem(
-      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "y", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node z = d_skolemManager->mkDummySkolem(
-      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "z", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node m = NodeBuilder() << w << x << kind::OR;
   Node n = NodeBuilder() << m << y << z << kind::AND;
 
@@ -550,13 +550,13 @@ TEST_F(TestNodeBlackNode, toStream)
   TypeNode booleanType = d_nodeManager->booleanType();
 
   Node w = d_skolemManager->mkDummySkolem(
-      "w", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "w", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node x = d_skolemManager->mkDummySkolem(
-      "x", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "x", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node y = d_skolemManager->mkDummySkolem(
-      "y", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "y", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node z = d_skolemManager->mkDummySkolem(
-      "z", booleanType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "z", booleanType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node m = NodeBuilder() << x << y << kind::OR;
   Node n = NodeBuilder() << w << m << z << kind::AND;
   Node o = NodeBuilder() << n << n << kind::XOR;
@@ -619,13 +619,13 @@ TEST_F(TestNodeBlackNode, dagifier)
   TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
 
   Node x = d_skolemManager->mkDummySkolem(
-      "x", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "x", intType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node y = d_skolemManager->mkDummySkolem(
-      "y", intType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "y", intType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node f = d_skolemManager->mkDummySkolem(
-      "f", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "f", fnType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node g = d_skolemManager->mkDummySkolem(
-      "g", fnType, "", NodeManager::SKOLEM_EXACT_NAME);
+      "g", fnType, "", SkolemManager::SKOLEM_EXACT_NAME);
   Node fx = d_nodeManager->mkNode(APPLY_UF, f, x);
   Node fy = d_nodeManager->mkNode(APPLY_UF, f, y);
   Node gx = d_nodeManager->mkNode(APPLY_UF, g, x);
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index de0c76ce1..b02790cb5 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -122,7 +122,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
 TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
 {
   Node x = d_skolemManager->mkDummySkolem(
-      "x", *d_boolTypeNode, "", NodeManager::SKOLEM_EXACT_NAME);
+      "x", *d_boolTypeNode, "", SkolemManager::SKOLEM_EXACT_NAME);
   ASSERT_EQ(x.getKind(), SKOLEM);
   ASSERT_EQ(x.getNumChildren(), 0u);
   ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp
index 0a2bcb532..4d6bade95 100644
--- a/test/unit/theory/theory_arith_cad_white.cpp
+++ b/test/unit/theory/theory_arith_cad_white.cpp
@@ -90,13 +90,15 @@ Node operator*(const Node& a, const Node& b)
 Node operator!(const Node& a) { return nodeManager->mkNode(Kind::NOT, a); }
 Node make_real_variable(const std::string& s)
 {
-  return nodeManager->mkSkolem(
-      s, nodeManager->realType(), "", NodeManager::SKOLEM_EXACT_NAME);
+  SkolemManager* sm = nodeManager->getSkolemManager();
+  return sm->mkDummySkolem(
+      s, nodeManager->realType(), "", SkolemManager::SKOLEM_EXACT_NAME);
 }
 Node make_int_variable(const std::string& s)
 {
-  return nodeManager->mkSkolem(
-      s, nodeManager->integerType(), "", NodeManager::SKOLEM_EXACT_NAME);
+  SkolemManager* sm = nodeManager->getSkolemManager();
+  return sm->mkDummySkolem(
+      s, nodeManager->integerType(), "", SkolemManager::SKOLEM_EXACT_NAME);
 }
 
 TEST_F(TestTheoryWhiteArithCAD, test_univariate_isolation)