From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 25 Jan 2022 17:46:20 +0000 (-0800)
Subject: Send `nth(unit(...), ...)` terms to array solver (#7983)
X-Git-Tag: cvc5-1.0.0~507
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f15ebaeaa34b52e6bd3268cfc5cf411cad4a21f;p=cvc5.git

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 a4ac38d03..90725bd2a 100644
--- 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 d89d7f344..d2148bdfd 100644
--- 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
index 000000000..0965036c0
--- /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)