From 0f15ebaeaa34b52e6bd3268cfc5cf411cad4a21f Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 25 Jan 2022 09:46:20 -0800 Subject: [PATCH] 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. --- src/theory/strings/array_solver.cpp | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress0/seq/nth-unit.smt2 | 11 +++++++++++ 3 files changed, 13 insertions(+) create mode 100644 test/regress/regress0/seq/nth-unit.smt2 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 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) -- 2.30.2