From 76465f3dbe7d9a54ef4ea6c10997b4f0996590fa Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 20 Apr 2022 22:28:52 -0700 Subject: [PATCH] [Seq] Remove `SkolemCache::mkSkolemSeqNth()` (#8643) This removes the `SkolemCache::mkSkolemSeqNth()` method. Instead of handling the out-of-bounds case with a UF, we just use `seq.nth` in its original form for the out-of-bounds case (and rely on the fact that the equality engine is configured to perform congruence closure on that kind). This is part of the changes for the paper on sequences. --- src/expr/skolem_manager.cpp | 1 - src/expr/skolem_manager.h | 2 - src/theory/strings/array_core_solver.cpp | 8 ++- src/theory/strings/array_solver.cpp | 53 +++++++++---------- src/theory/strings/skolem_cache.cpp | 16 ------ src/theory/strings/skolem_cache.h | 5 -- .../strings/theory_strings_preprocess.cpp | 17 +++--- 7 files changed, 35 insertions(+), 67 deletions(-) diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 05ca1b0bb..4d5a53fd7 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -61,7 +61,6 @@ const char* toString(SkolemFunId id) return "TRANSCENDENTAL_PURIFY_ARG"; case SkolemFunId::SELECTOR_WRONG: return "SELECTOR_WRONG"; case SkolemFunId::SHARED_SELECTOR: return "SHARED_SELECTOR"; - case SkolemFunId::SEQ_NTH_OOB: return "SEQ_NTH_OOB"; case SkolemFunId::STRINGS_NUM_OCCUR: return "STRINGS_NUM_OCCUR"; case SkolemFunId::STRINGS_OCCUR_INDEX: return "STRINGS_OCCUR_INDEX"; case SkolemFunId::STRINGS_OCCUR_LEN: return "STRINGS_OCCUR_LEN"; diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 68ea25520..5736b1722 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -50,8 +50,6 @@ enum class SkolemFunId SELECTOR_WRONG, /** a shared selector */ SHARED_SELECTOR, - /** an application of seq.nth that is out of bounds */ - SEQ_NTH_OOB, //----- string skolems are cached based on two strings (a, b) /** exists k. ( b occurs k times in a ) */ STRINGS_NUM_OCCUR, diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 595f3c2c7..ff3dced65 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -174,13 +174,13 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) for (Node j : indexes) { // nth(x, m) - // y = update(s, n, t), m) + // y = update(s, n, t) // x = y or x = s // ------------------------ // nth(update(s, n, t)) = // ite(0 <= m < len(s), // ite(n = m, nth(t, 0), nth(s, m)), - // Uf(update(s, n, t), m)) + // nth(update(s, n, t), m)) Node nth = nm->mkNode(SEQ_NTH, termProxy, j); Node nthInBounds = nm->mkNode(AND, @@ -190,9 +190,7 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) Node updateVal = nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(0)); Node iteNthInBounds = nm->mkNode( ITE, i.eqNode(j), updateVal, nm->mkNode(SEQ_NTH, n[0], j)); - Node uf = SkolemCache::mkSkolemSeqNth(n[0].getType(), "Uf"); - Node ufj = nm->mkNode(APPLY_UF, uf, n, j); - Node rhs = nm->mkNode(ITE, nthInBounds, iteNthInBounds, ufj); + Node rhs = nm->mkNode(ITE, nthInBounds, iteNthInBounds, nth); Node lem = nth.eqNode(rhs); std::vector exp; diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index 1c6830621..0dfe2d180 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -198,43 +198,44 @@ void ArraySolver::checkTerm(Node t, bool checkInv) Trace("seq-array-debug") << "...unit case" << std::endl; // do we know whether n = 0 ? // x = (seq.unit m) => (seq.update x n z) = ite(n=0, z, (seq.unit m)) - // x = (seq.unit m) => (seq.nth x n) = ite(n=0, m, Uf(x, n)) - Node thenBranch; - Node elseBranch; + // x = (seq.unit m) ^ n=0 => (seq.nth x n) = m InferenceId iid; + Node eq; + std::vector exp; + std::vector nexp; + d_im.addToExplanation(t[0], nf.d_nf[0], exp); + d_im.addToExplanation(r, t[0], exp); if (k == STRING_UPDATE) { - thenBranch = t[2]; - elseBranch = nf.d_nf[0]; iid = InferenceId::STRINGS_ARRAY_UPDATE_UNIT; + eq = nm->mkNode( + ITE, t[1].eqNode(d_zero), t.eqNode(t[2]), t.eqNode(nf.d_nf[0])); } else { Assert(k == SEQ_NTH); + Node val; if (ck == CONST_SEQUENCE) { const Sequence& seq = nf.d_nf[0].getConst(); - thenBranch = seq.getVec()[0]; + val = seq.getVec()[0]; } else { - thenBranch = nf.d_nf[0][0]; + val = nf.d_nf[0][0]; } - Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf"); - elseBranch = nm->mkNode(APPLY_UF, uf, t[0], t[1]); iid = InferenceId::STRINGS_ARRAY_NTH_UNIT; + eq = t.eqNode(val); + if (t[1] != d_zero) + { + exp.push_back(t[1].eqNode(d_zero)); + nexp.push_back(t[1].eqNode(d_zero)); + } } - std::vector exp; - d_im.addToExplanation(t[0], nf.d_nf[0], exp); - d_im.addToExplanation(r, t[0], exp); - Node eq = nm->mkNode(ITE, - t[1].eqNode(d_zero), - t.eqNode(thenBranch), - t.eqNode(elseBranch)); if (d_eqProc.find(eq) == d_eqProc.end()) { d_eqProc.insert(eq); - d_im.sendInference(exp, eq, iid); + d_im.sendInference(exp, nexp, eq, iid); } return; } @@ -353,12 +354,13 @@ void ArraySolver::checkTerm(Node t, bool checkInv) // z = (seq.++ x y) => // (seq.update z n l) = // (seq.++ (seq.update x n 1) (seq.update y (- n len(x)) 1)) - // z = (seq.++ x y) => + // z = (seq.++ x y) ^ (>= n 0) ^ (< n (+ (str.len x) (str.len y)))) => // (seq.nth z n) = - // (ite (or (< n 0) (>= n (+ (str.len x) (str.len y)))) (Uf z n) // (ite (< n (str.len x)) (seq.nth x n) - // (seq.nth y (- n (str.len x))))) + // (seq.nth y (- n (str.len x)))) InferenceId iid; + std::vector exp; + std::vector nexp; Node eq; if (k == STRING_UPDATE) { @@ -380,19 +382,16 @@ void ArraySolver::checkTerm(Node t, bool checkInv) { std::reverse(cchildren.begin(), cchildren.end()); std::reverse(cond.begin(), cond.end()); - Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf"); eq = t.eqNode(cchildren[0]); for (size_t i = 1, ncond = cond.size(); i < ncond; i++) { eq = nm->mkNode(ITE, cond[i], t.eqNode(cchildren[i]), eq); } - Node ufa = nm->mkNode(APPLY_UF, uf, t[0], t[1]); - Node oobCond = - nm->mkNode(OR, nm->mkNode(LT, t[1], d_zero), cond[0].notNode()); - eq = nm->mkNode(ITE, oobCond, t.eqNode(ufa), eq); + Node inBoundsCond = nm->mkNode(AND, nm->mkNode(GEQ, t[1], d_zero), cond[0]); + exp.push_back(inBoundsCond); + nexp.push_back(inBoundsCond); iid = InferenceId::STRINGS_ARRAY_NTH_CONCAT; } - std::vector exp; if (checkInv) { NormalForm& nfSelf = d_csolver.getNormalForm(rself); @@ -408,7 +407,7 @@ void ArraySolver::checkTerm(Node t, bool checkInv) { d_eqProc.insert(eq); Trace("seq-array") << "- send lemma - " << eq << std::endl; - d_im.sendInference(exp, eq, iid); + d_im.sendInference(exp, nexp, eq, iid); } } diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 0984ff0c1..1cf1d5f9e 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -154,22 +154,6 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn, return mkTypedSkolemCached(tn, a, Node::null(), id, c); } -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 argTypes; - argTypes.push_back(seqType); - argTypes.push_back(nm->integerType()); - TypeNode elemType = seqType.getSequenceElementType(); - TypeNode ufType = nm->mkFunctionType(argTypes, elemType); - return sm->mkSkolemFunction(SkolemFunId::SEQ_NTH_OOB, ufType); -} - Node SkolemCache::mkSkolem(const char* c) { // TODO: eliminate this diff --git a/src/theory/strings/skolem_cache.h b/src/theory/strings/skolem_cache.h index 39f10ee09..ca55e0410 100644 --- a/src/theory/strings/skolem_cache.h +++ b/src/theory/strings/skolem_cache.h @@ -135,11 +135,6 @@ class SkolemCache TypeNode tn, Node a, Node b, SkolemId id, const char* c); /** Same as mkTypedSkolemCached above for (a,[null],id) */ Node mkTypedSkolemCached(TypeNode tn, Node a, SkolemId id, const char* c); - /** - * Specific version for seq.nth, used for cases where the index is out of - * range for sequence type seqType. - */ - 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_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8783457f3..1d32a310d 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -521,19 +521,14 @@ Node StringsPreprocess::reduce(Node t, Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12)); Node b1 = nm->mkNode(AND, b11, b12, b13); - // nodes for the case where `seq.nth` is undefined. - 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` - Node lemma = nm->mkNode(ITE, cond, b1, b2); + // the lemma for `seq.nth` + Node lemma = nm->mkNode(IMPLIES, cond, b1); // assert: - // IF n >=0 AND n < len( s ) - // THEN: s = sk1 ++ unit(skt) ++ sk2 AND - // len( sk1 ) = n AND - // ( len( sk2 ) = len( s )- (n+1) - // ELSE: skt = Uf(s, n), where Uf is a cached skolem function. + // n >=0 AND n < len( s ) + // IMPLIES: s = sk1 ++ unit(skt) ++ sk2 AND + // len( sk1 ) = n AND + // ( len( sk2 ) = len( s )- (n+1) asserts.push_back(lemma); retNode = skt; } -- 2.30.2