diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-13 14:30:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-13 19:30:03 +0000 |
commit | 10308c88ae5de234eb62c08380d53d4967112ccd (patch) | |
tree | c60187541a2e5aabda5fd1141ab210900e690126 /src/theory/strings | |
parent | cdb5c6e7e03e4717f21c5726f02763962c23a7b2 (diff) |
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.
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 7 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 2 |
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` |