From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 3 Feb 2022 05:58:49 +0000 (-0800)
Subject: Send all `nth` terms to the core array solver (#7990)
X-Git-Tag: cvc5-1.0.0~464
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cc4eefe84809af49ad932751070fe392fe3f7c08;p=cvc5.git

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.
---

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<Node> 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<Node> 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