From 04a494e251a8cc2c90bb429e2858f1c4eb8f88ff Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 7 Apr 2021 13:36:15 -0500
Subject: 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.
---
 src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp |  8 +++++---
 src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp |  4 +++-
 src/theory/quantifiers/cegqi/vts_term_cache.cpp      | 17 ++++++++++-------
 3 files changed, 18 insertions(+), 11 deletions(-)

(limited to 'src/theory/quantifiers/cegqi')

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index bdd6d26ab..45433bdb6 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
 
 #include <stack>
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h"
@@ -642,6 +643,7 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
   if (options::cegqiBvRmExtract())
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
     // map from terms to bitvector extracts applied to that term
     std::map<Node, std::vector<Node> > extract_map;
@@ -691,9 +693,9 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
         Node ex = bv::utils::mkExtract(
             es.first, boundaries[i - 1] - 1, boundaries[i]);
         Node var =
-            nm->mkSkolem("ek",
-                         ex.getType(),
-                         "variable to represent disjoint extract region");
+            sm->mkDummySkolem("ek",
+                              ex.getType(),
+                              "variable to represent disjoint extract region");
         children.push_back(var);
         vars.push_back(var);
       }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 5e3a64325..74469e7de 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
@@ -463,7 +464,8 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
     return it->second;
   }
   NodeManager * nm = NodeManager::currentNM();
-  Node g = nm->mkSkolem("g", nm->booleanType());
+  SkolemManager* sm = nm->getSkolemManager();
+  Node g = sm->mkDummySkolem("g", nm->booleanType());
   // ensure that it is a SAT literal
   Node ceLit = d_qstate.getValuation().ensureLiteral(g);
   d_ce_lit[q] = ceLit;
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index 1974e7c7c..5f114c313 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/vts_term_cache.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/rewriter.h"
@@ -60,18 +61,19 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create)
   if (create)
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     if (d_vts_delta_free.isNull())
     {
       d_vts_delta_free =
-          nm->mkSkolem("delta_free",
-                       nm->realType(),
-                       "free delta for virtual term substitution");
+          sm->mkDummySkolem("delta_free",
+                            nm->realType(),
+                            "free delta for virtual term substitution");
       Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
       d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
     }
     if (d_vts_delta.isNull())
     {
-      d_vts_delta = nm->mkSkolem(
+      d_vts_delta = sm->mkDummySkolem(
           "delta", nm->realType(), "delta for virtual term substitution");
       // mark as a virtual term
       VirtualTermSkolemAttribute vtsa;
@@ -86,15 +88,16 @@ Node VtsTermCache::getVtsInfinity(TypeNode tn, bool isFree, bool create)
   if (create)
   {
     NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
     if (d_vts_inf_free[tn].isNull())
     {
-      d_vts_inf_free[tn] = nm->mkSkolem(
+      d_vts_inf_free[tn] = sm->mkDummySkolem(
           "inf_free", tn, "free infinity for virtual term substitution");
     }
     if (d_vts_inf[tn].isNull())
     {
-      d_vts_inf[tn] =
-          nm->mkSkolem("inf", tn, "infinity for virtual term substitution");
+      d_vts_inf[tn] = sm->mkDummySkolem(
+          "inf", tn, "infinity for virtual term substitution");
       // mark as a virtual term
       VirtualTermSkolemAttribute vtsa;
       d_vts_inf[tn].setAttribute(vtsa, true);
-- 
cgit v1.2.3