From cc4eefe84809af49ad932751070fe392fe3f7c08 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 2 Feb 2022 21:58:49 -0800 Subject: [PATCH] Send all `nth` terms to the core array solver (#7990) This updates our policy for the sequences array solver to send all updates to the array core solver. --- src/theory/strings/array_solver.cpp | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp index 89dadd695..cc844b229 100644 --- a/src/theory/strings/array_solver.cpp +++ b/src/theory/strings/array_solver.cpp @@ -125,6 +125,13 @@ void ArraySolver::checkTerm(Node t, bool checkInv) NormalForm& nf = d_csolver.getNormalForm(r); Trace("seq-array-debug") << "...normal form " << nf.d_nf << std::endl; std::vector nfChildren; + + if (k == SEQ_NTH) + { + // The core solver must process all `nth` terms + d_currTerms[SEQ_NTH].push_back(t); + } + if (checkInv) { if (k != STRING_UPDATE) @@ -196,7 +203,6 @@ void ArraySolver::checkTerm(Node t, bool checkInv) Node uf = SkolemCache::mkSkolemSeqNth(t[0].getType(), "Uf"); elseBranch = nm->mkNode(APPLY_UF, uf, t[0], t[1]); iid = InferenceId::STRINGS_ARRAY_NTH_UNIT; - d_currTerms[k].push_back(t); } std::vector exp; d_im.addToExplanation(t[0], nf.d_nf[0], exp); @@ -214,7 +220,6 @@ void ArraySolver::checkTerm(Node t, bool checkInv) } else if (ck != CONST_SEQUENCE) { - bool isAtomic = true; if (k == STRING_UPDATE) { // If the term we are updating is atomic, but the update itself @@ -222,18 +227,14 @@ void ArraySolver::checkTerm(Node t, bool checkInv) // concat rule, based on the normal form of the term itself. rself = d_state.getRepresentative(t); NormalForm& nfSelf = d_csolver.getNormalForm(rself); - if (nfSelf.d_nf.size() > 1) + if (nfSelf.d_nf.size() == 1) { - isAtomic = false; + // otherwise, if the normal form is not a constant sequence, and we + // are an atomic update term, then this term will be given to the + // core array solver. + d_currTerms[k].push_back(t); } } - if (isAtomic) - { - // otherwise, if the normal form is not a constant sequence, and we - // are not a non-atomic update term, then this term will be given to - // the core array solver. - d_currTerms[k].push_back(t); - } return; } else -- 2.30.2