From: Andres Noetzli Date: Thu, 20 Jan 2022 23:03:02 +0000 (-0800) Subject: Fix `Nth-Update` rule, add `Update-Bound` rule (#7968) X-Git-Tag: cvc5-1.0.0~520 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a22355748973e5e567e9543a7f036a23d616bbbd;p=cvc5.git Fix `Nth-Update` rule, add `Update-Bound` rule (#7968) This commit updates the inferences in the sequences array solver to more closely resemble the current rules in the paper. Concretely, it adds an implementation of the `Update-Bound` rule and it fixes the `Nth-Update` rule to take into account all three branches in the conclusion of the rule. Co-authored-by: Yoni Zohar --- diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 0d116b1eb..d7e5fccbe 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -417,6 +417,10 @@ const char* toString(InferenceId i) return "STRINGS_ARRAY_NTH_UPDATE"; case InferenceId::STRINGS_ARRAY_NTH_TERM_FROM_UPDATE: return "STRINGS_ARRAY_NTH_TERM_FROM_UPDATE"; + case InferenceId::STRINGS_ARRAY_UPDATE_BOUND: + return "STRINGS_ARRAY_UPDATE_BOUND"; + case InferenceId::STRINGS_ARRAY_EQ_SPLIT: + return "STRINGS_ARRAY_EQ_SPLIT"; case InferenceId::STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT: return "STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT"; case InferenceId::STRINGS_ARRAY_NTH_REV: return "STRINGS_ARRAY_NTH_REV"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index a82093bab..4970c1cee 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -698,6 +698,10 @@ enum class InferenceId STRINGS_ARRAY_NTH_UPDATE, // reasoning about the nth term from update term STRINGS_ARRAY_NTH_TERM_FROM_UPDATE, + // reasoning about whether an update changes a term or not + STRINGS_ARRAY_UPDATE_BOUND, + // splitting about equality of sequences + STRINGS_ARRAY_EQ_SPLIT, // nth over update when updated with an unit term STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT, // nth over reverse diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 160f289ad..c7e72c11f 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -81,6 +81,21 @@ void ArrayCoreSolver::checkNth(const std::vector& nthTerms) sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_EXTRACT); } } + for (size_t i = 0; i < nthTerms.size(); i++) + { + for (size_t j = i + 1; j < nthTerms.size(); j++) + { + Node x = nthTerms[i][0]; + Node y = nthTerms[j][0]; + Node n = nthTerms[i][1]; + Node m = nthTerms[j][1]; + if (d_state.areEqual(n, m) && !d_state.areEqual(x, y) + && !d_state.areDisequal(x, y)) + { + d_im.sendSplit(x, y, InferenceId::STRINGS_ARRAY_EQ_SPLIT); + } + } + } } void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) @@ -96,8 +111,6 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) // note that the term could rewrites to a skolem // get proxy variable for the update term as t Node termProxy = d_termReg.getProxyVariableFor(n); - std::vector exp; - d_im.addToExplanation(termProxy, n, exp); if (d_registeredUpdates.find(n) == d_registeredUpdates.end()) { @@ -117,11 +130,27 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) Node body2 = nm->mkNode(SEQ_NTH, n[0], n[1]); Node right = nm->mkNode(ITE, cond, body1, body2); Node lem = nm->mkNode(EQUAL, left, right); + + std::vector exp; + d_im.addToExplanation(termProxy, n, exp); d_im.sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_TERM_FROM_UPDATE, false, true); + + // update(s, n, t) + // ------------------------ + // 0 <= n < len(t) and nth(s, n) != nth(update(s, n, t)) || + // s = update(s, n, t) + lem = nm->mkNode( + OR, + nm->mkNode(AND, + left.eqNode(nm->mkNode(SEQ_NTH, n[0], n[1])).notNode(), + cond), + n.eqNode(n[0])); + d_im.sendInference( + exp, lem, InferenceId::STRINGS_ARRAY_UPDATE_BOUND, false, true); } for (const auto& nthIdxs : d_indexMap) @@ -137,46 +166,31 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) const std::set& indexes = nthIdxs.second; Trace("seq-array-core-debug") << " check nth for " << seq << " with indices " << indexes << std::endl; + Node i = n[1]; for (Node j : indexes) { - if (n[2].getKind() == SEQ_UNIT) - { - // Special case for updates using unit - // - // x = update(s, n, unit(t)) - // y = nth(x, m) - // ----------------------------------------- - // n != m => nth(x, m) = nth(s, m) - Node left = n[1].eqNode(j).notNode(); - Node nth1 = nm->mkNode(SEQ_NTH, termProxy, j); - Node nth2 = nm->mkNode(SEQ_NTH, n[0], j); - Node right = nm->mkNode(EQUAL, nth1, nth2); - Node lem = nm->mkNode(IMPLIES, left, right); - sendInference( - exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT); - continue; - } - - // Regular case - // - // x = update(s, n, t) - // y = nth(x, m) - // ----------------------------------------- - // y = ite(n <= m < n + len(t), nth(t, m - n), nth(s, m)) + // nth(update(s, n, t), m) + // ------------------------ + // nth(update(s, n, t)) = + // ite(0 <= m < len(s), + // ite(n = m, nth(t, 0), nth(s, m)), + // Uf(update(s, n, t), m)) Node nth = nm->mkNode(SEQ_NTH, termProxy, j); - Node cond = nm->mkNode( - AND, - nm->mkNode(LEQ, n[1], j), - nm->mkNode( - LT, - j, - nm->mkNode(PLUS, n[1], nm->mkNode(STRING_LENGTH, n[2])))); - Node cases = - nm->mkNode(ITE, - cond, - nm->mkNode(SEQ_NTH, n[2], nm->mkNode(MINUS, j, n[1])), - nm->mkNode(SEQ_NTH, n[0], j)); - Node lem = nm->mkNode(EQUAL, nth, cases); + Node nthInBounds = + nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConstInt(0), j), + nm->mkNode(LT, j, nm->mkNode(STRING_LENGTH, n[0]))); + Node idxEq = i.eqNode(j); + Node updateVal = nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(0)); + Node iteNthInBounds = nm->mkNode( + ITE, i.eqNode(j), updateVal, nm->mkNode(SEQ_NTH, n[0], j)); + Node uf = SkolemCache::mkSkolemSeqNth(n[0].getType(), "Uf"); + Node ufj = nm->mkNode(APPLY_UF, uf, n, j); + Node rhs = nm->mkNode(ITE, nthInBounds, iteNthInBounds, ufj); + Node lem = nth.eqNode(rhs); + + std::vector exp; + d_im.addToExplanation(termProxy, n, exp); sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 53df6519e..1850fdda4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1101,6 +1101,7 @@ set(regress_0_tests regress0/sep/skolem_emp.smt2 regress0/sep/trees-1.smt2 regress0/sep/wand-crash.smt2 + regress0/seq/err1.smt2 regress0/seq/intseq.smt2 regress0/seq/intseq_dt.smt2 regress0/seq/issue4370-bool-terms.smt2 @@ -1110,6 +1111,8 @@ set(regress_0_tests regress0/seq/issue5665-invalid-model.smt2 regress0/seq/issue6337-seq.smt2 regress0/seq/len_simplify.smt2 + regress0/seq/nth-oob.smt2 + regress0/seq/nth-update.smt2 regress0/seq/proj-issue340.smt2 regress0/seq/quant_len_trigger.smt2 regress0/seq/rev.smt2 @@ -1140,6 +1143,7 @@ set(regress_0_tests regress0/seq/seq-types.smt2 regress0/seq/update-concat-non-atomic.smt2 regress0/seq/update-concat-non-atomic2.smt2 + regress0/seq/update-eq.smt2 regress0/seq/update-eq-unsat.smt2 regress0/sets/abt-min.smt2 regress0/sets/abt-te-exh.smt2 diff --git a/test/regress/regress0/seq/array/update-word-eq.smt2 b/test/regress/regress0/seq/array/update-word-eq.smt2 index f81077c6f..98c037383 100644 --- a/test/regress/regress0/seq/array/update-word-eq.smt2 +++ b/test/regress/regress0/seq/array/update-word-eq.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --strings-exp --seq-array=eager +; DISABLE-TESTER: proof (set-logic QF_SLIA) (set-info :status unsat) diff --git a/test/regress/regress0/seq/err1.smt2 b/test/regress/regress0/seq/err1.smt2 new file mode 100644 index 000000000..85f9c8903 --- /dev/null +++ b/test/regress/regress0/seq/err1.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy +; EXPECT: unsat +(set-logic ALL) +(declare-sort E 0) +(declare-fun a () (Seq E)) +(declare-fun a_ () (Seq E)) +(declare-fun _3 () (Seq E)) +(declare-fun _4 () (Seq E)) +(declare-fun _39 () E) +(declare-fun e () E) +(assert (= (str.update _3 0 (seq.unit _39)) (str.update a 1 (seq.unit e)))) +(assert (= a (str.update a 1 (seq.unit (seq.nth (str.update a 1 (seq.unit e)) 2))))) +(assert (= (str.update (str.update _3 0 (seq.unit e)) 0 (seq.unit _39)) (str.update _4 1 (seq.unit e)))) +(assert (= e (seq.nth (str.update _4 1 (seq.unit e)) 2))) +(assert (distinct a (str.update _4 1 (seq.unit (seq.nth (str.update _3 0 (seq.unit e)) 1))))) +(check-sat) diff --git a/test/regress/regress0/seq/nth-oob.smt2 b/test/regress/regress0/seq/nth-oob.smt2 new file mode 100644 index 000000000..723dd5831 --- /dev/null +++ b/test/regress/regress0/seq/nth-oob.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy +; EXPECT: unsat + +(set-logic QF_SLIA) +(declare-const x (Seq Int)) +(declare-const i Int) +(declare-const j Int) +(declare-const v Int) +(assert (not (= (seq.nth (seq.update x i (seq.unit v)) j) (seq.nth x j)))) +(assert (< i 0)) +(assert (< j 0)) +(check-sat) diff --git a/test/regress/regress0/seq/nth-update.smt2 b/test/regress/regress0/seq/nth-update.smt2 new file mode 100644 index 000000000..9ee7e8fa0 --- /dev/null +++ b/test/regress/regress0/seq/nth-update.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy --no-check-models +; EXPECT: sat +(set-logic QF_SLIA) +(declare-const x (Seq Int)) +(declare-const i Int) +(declare-const j Int) +(assert (not (= (seq.nth (seq.update x i (seq.unit 5)) j) (seq.nth x j)))) +(assert (< j 0)) +(check-sat) diff --git a/test/regress/regress0/seq/update-eq.smt2 b/test/regress/regress0/seq/update-eq.smt2 new file mode 100644 index 000000000..30d49ad4c --- /dev/null +++ b/test/regress/regress0/seq/update-eq.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp --seq-array=lazy +(set-logic QF_UFSLIA) +(declare-sort E 0) +(declare-fun x () (Seq E)) +(declare-fun y () (Seq E)) +(assert (= y (seq.update x 0 (seq.unit (seq.nth x 0))))) +(assert (distinct (seq.nth x 1) (seq.nth y 1))) +(set-info :status unsat) +(check-sat)