Send `nth(unit(...), ...)` terms to array solver (#7983)

This commit changes our policy of which terms we send to the array core
solver. Previously, we were not sending nth terms that
were applied to unit sequences. This was incorrect, because for example
the split STRINGS_ARRAY_EQ_SPLIT has to be applied to nth of units,
too, to guarantee model soundness: For example, if we have a disequality
nth(t1, i) != nth(unit(v), i), then we have to reason about the
(dis)equality of t1 and unit(v), because of the UF for the
out-of-bounds case of nth (i.e., we have to reason that Uf(t1, i) != Uf(unit(v), i), which requires t1 != unit(v)). Splitting on t1 = unit(v) is done by STRINGS_ARRAY_EQ_SPLIT.

diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index a4ac38d03f464848397562f861b410651226851c..90725bd2a479b533233a49d7445fe62526a91bc1 100644 (file)
--- a/src/theory/strings/array_solver.cpp
+++ b/src/theory/strings/array_solver.cpp
@@ -196,6 +196,7 @@ 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);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d89d7f3445c85240deb87879a9ab1c09e09e29a0..d2148bdfd956dd5e9c205652b7bd2117002887b8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1112,6 +1112,7 @@ set(regress_0_tests
   regress0/seq/issue6337-seq.smt2
   regress0/seq/len_simplify.smt2
   regress0/seq/nth-oob.smt2
+  regress0/seq/nth-unit.smt2
   regress0/seq/nth-update.smt2
   regress0/seq/proj-issue340.smt2
   regress0/seq/quant_len_trigger.smt2

diff --git a/test/regress/regress0/seq/nth-unit.smt2 b/test/regress/regress0/seq/nth-unit.smt2
new file mode 100644 (file)
index 0000000..0965036
--- /dev/null
+++ b/test/regress/regress0/seq/nth-unit.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --seq-array=lazy
+(set-logic QF_SLIA)
+(declare-fun s () (Seq Int))
+(declare-fun j () Int)
+(assert (and 
+  (= (seq.unit 0) (str.update s 0 (seq.unit 0)))
+  (distinct
+    (seq.nth s j)
+    (seq.nth (seq.unit (seq.nth s 0)) j))))
+(set-info :status unsat)
+(check-sat)