Formalize more skolems (#6307)

This formalizes more skolems in preparation for moving Theory::expandDefinitions to Rewriter::expandDefinitions.

It also adds proof support for datatypes purification.

4 files changed, 8 insertions, 6 deletions

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index f68d7805b..eb2df1285 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -141,15 +141,18 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn,
 
 Node SkolemCache::mkSkolemSeqNth(TypeNode seqType, const char* c)
 {
+  // Note this method is static and does not rely on any local caching.
+  // It is used by expand definitions and by (dynamic) reductions, thus
+  // it is centrally located here.
   Assert(seqType.isSequence());
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   std::vector<TypeNode> argTypes;
   argTypes.push_back(seqType);
   argTypes.push_back(nm->integerType());
   TypeNode elemType = seqType.getSequenceElementType();
   TypeNode ufType = nm->mkFunctionType(argTypes, elemType);
-  return mkTypedSkolemCached(
-      ufType, Node::null(), Node::null(), SkolemCache::SK_NTH, c);
+  return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType);
 }
 
 Node SkolemCache::mkSkolem(const char* c)
diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h
index 1006a758c..d64e4d5ae 100644
--- a/src/theory/strings/skolem_cache.h
+++ b/src/theory/strings/skolem_cache.h
@@ -164,7 +164,7 @@ class SkolemCache
    * Specific version for seq.nth, used for cases where the index is out of
    * range for sequence type seqType.
    */
-  Node mkSkolemSeqNth(TypeNode seqType, const char* c);
+  static Node mkSkolemSeqNth(TypeNode seqType, const char* c);
   /** Returns a (uncached) skolem of type string with name c */
   Node mkSkolem(const char* c);
   /** Returns true if n is a skolem allocated by this class */
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ea0fc5ea8..0ed003cc7 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -560,7 +560,6 @@ TrustNode TheoryStrings::expandDefinition(Node node)
   if (node.getKind() == kind::SEQ_NTH)
   {
     NodeManager* nm = NodeManager::currentNM();
-    SkolemCache* sc = d_termReg.getSkolemCache();
     Node s = node[0];
     Node n = node[1];
     // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
@@ -568,7 +567,7 @@ TrustNode TheoryStrings::expandDefinition(Node node)
                            nm->mkNode(LEQ, d_zero, n),
                            nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
     Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
-    Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+    Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
     Node u = nm->mkNode(APPLY_UF, uf, s, n);
     Node ret = nm->mkNode(ITE, cond, ss, u);
     Trace("strings-exp-def") << "...return " << ret << std::endl;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1fd2bb519..5e6b27e1b 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -445,7 +445,7 @@ Node StringsPreprocess::reduce(Node t,
     Node b1 = nm->mkNode(AND, b11, b12, b13);
 
     // nodes for the case where `seq.nth` is undefined.
-    Node uf = sc->mkSkolemSeqNth(s.getType(), "Uf");
+    Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
     Node b2 = nm->mkNode(EQUAL, skt, nm->mkNode(APPLY_UF, uf, s, n));
 
     // the full ite, split on definedness of `seq.nth`