From: Ying Sheng Date: Fri, 17 Dec 2021 22:28:12 +0000 (-0800) Subject: Array-inspired Sequence Solver - Fixing several issues in the ArrayCoreSolver class... X-Git-Tag: cvc5-1.0.0~635 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c67bbf88a0da5c7c066de5ba9e31b58f00594b9b;p=cvc5.git Array-inspired Sequence Solver - Fixing several issues in the ArrayCoreSolver class and options (#7820) This commit fixes several issues in the ArrayCoreSolver class and the options: 1. Add range checking for an update rule. 2. Assign different inference ids to different rules. 3. small syntax optimizations. --- diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index ced885abb..af18d3eef 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -411,6 +411,10 @@ const char* toString(InferenceId i) return "STRINGS_ARRAY_NTH_EXTRACT"; case InferenceId::STRINGS_ARRAY_NTH_UPDATE: return "STRINGS_ARRAY_NTH_UPDATE"; + case InferenceId::STRINGS_ARRAY_NTH_TERM_FROM_UPDATE: + return "STRINGS_ARRAY_NTH_TERM_FROM_UPDATE"; + 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"; case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT"; case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index f0c726f78..8eaeeab75 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -692,6 +692,10 @@ enum class InferenceId STRINGS_ARRAY_NTH_EXTRACT, // nth over update STRINGS_ARRAY_NTH_UPDATE, + // reasoning about the nth term from update term + STRINGS_ARRAY_NTH_TERM_FROM_UPDATE, + // nth over update when updated with an unit term + STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT, // nth over reverse STRINGS_ARRAY_NTH_REV, //-------------------- regexp solver diff --git a/src/theory/strings/array_core_solver.cpp b/src/theory/strings/array_core_solver.cpp index 9e3921e29..fd48eab6b 100644 --- a/src/theory/strings/array_core_solver.cpp +++ b/src/theory/strings/array_core_solver.cpp @@ -95,15 +95,11 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) // inference rule is: // (seq.update x i a) in TERMS // (seq.nth t j) in TERMS - // t == (seq.update x i a) - // ---------------------------------------------------------------------- + // t = (seq.update x i a) + // --------------------------------------------------------------------- // (seq.nth (seq.update x i a) j) = // (ITE, j in range(i, i+len(a)), (seq.nth a (j - i)), (seq.nth x j)) - // t == (seq.update x i a) => - // (seq.nth t j) = (ITE, j in range(i, i+len(a)), (seq.nth a (j - i)), - // (seq.nth x j)) - // note that the term could rewrites to a skolem // get proxy variable for the update term as t Node termProxy = d_termReg.getProxyVariableFor(n); @@ -111,26 +107,35 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) std::vector exp; d_im.addToExplanation(termProxy, n, exp); - // optimization: add a short cut t == (seq.update n[0] n[1] n[2]) => t[i] == - // n[2][0] + // reasoning about nth(t, n[1]) even if it does not exist. + // x = update(s, n, t) + // --------------------------------------------------------------------- + // nth(x, n) = ite(n in range(0, len(s)), nth(t, 0), nth(s, n)) Node left = nm->mkNode(SEQ_NTH, termProxy, n[1]); - Node right = - nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(Rational(0))); // n[2][0] + Node cond = + nm->mkNode(AND, + nm->mkNode(GEQ, n[1], nm->mkConstInt(Rational(0))), + nm->mkNode(LT, n[1], nm->mkNode(STRING_LENGTH, n[0]))); + Node body1 = nm->mkNode(SEQ_NTH, n[2], nm->mkConstInt(Rational(0))); + 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); - Trace("seq-array-debug") << "enter" << std::endl; - sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE); + sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_TERM_FROM_UPDATE); // enumerate possible index - for (auto nth : d_index_map) + for (const auto& nth : d_index_map) { Node seq = nth.first; if (d_state.areEqual(seq, n) || d_state.areEqual(seq, n[0])) { - std::set indexes = nth.second; + const std::set& indexes = nth.second; for (Node j : indexes) { - // optimization: add a short cut for special case (seq.update n[0] - // n[1] (seq.unit e)) + // optimization: add a short cut for special case + // x = update(s, n, unit(t)) + // y = nth(s, m) + // ----------------------------------------- + // n != m => nth(x, m) = nth(s, m) if (n[2].getKind() == SEQ_UNIT) { left = nm->mkNode(DISTINCT, n[1], j); @@ -138,20 +143,22 @@ void ArrayCoreSolver::checkUpdate(const std::vector& updateTerms) Node nth2 = nm->mkNode(SEQ_NTH, n[0], j); right = nm->mkNode(EQUAL, nth1, nth2); lem = nm->mkNode(IMPLIES, left, right); - sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE); + sendInference( + exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE_WITH_UNIT); + continue; } // normal cases left = nm->mkNode(SEQ_NTH, termProxy, j); - Node cond = nm->mkNode( + 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 body1 = nm->mkNode(SEQ_NTH, n[2], nm->mkNode(MINUS, j, n[1])); - Node body2 = nm->mkNode(SEQ_NTH, n[0], j); + body1 = nm->mkNode(SEQ_NTH, n[2], nm->mkNode(MINUS, j, n[1])); + body2 = nm->mkNode(SEQ_NTH, n[0], j); right = nm->mkNode(ITE, cond, body1, body2); lem = nm->mkNode(EQUAL, left, right); sendInference(exp, lem, InferenceId::STRINGS_ARRAY_NTH_UPDATE); @@ -193,16 +200,7 @@ void ArrayCoreSolver::check(const std::vector& nthTerms, Trace("seq-update") << "- " << r << ": " << n[1] << " -> " << n << std::endl; d_writeModel[r][n[1]] = n; - if (d_index_map.find(r) == d_index_map.end()) - { - std::set indexes; - indexes.insert(n[1]); - d_index_map[r] = indexes; - } - else - { - d_index_map[r].insert(n[1]); - } + d_index_map[r].insert(n[1]); if (n[0].getKind() == STRING_REV) {