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 <yoni206@gmail.com>

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 0d116b1eb9d93825ed4a762b692e2b3935d8861c..d7e5fccbe3ee978177d2e3267084a3b2c4104a31 100644 (file)
--- 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 a82093bab1999da52f621d4294b4c4bf9004d305..4970c1ceedb884934a01e15210620e105692a436 100644 (file)
--- 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 160f289ad5b1aaea784504dca201707ec49c25a5..c7e72c11f8c892d79040491e3da1c8125cb8d8a2 100644 (file)
--- 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<Node>& 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<Node>& updateTerms)
@@ -96,8 +111,6 @@ void ArrayCoreSolver::checkUpdate(const std::vector<Node>& 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<Node> 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<Node>& 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<Node> 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<Node>& updateTerms)
       const std::set<Node>& 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<Node> 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 53df6519e8229a71b0d7c3585acb20db535ecff1..1850fdda46ce7e02fdf3ca432843fcf5593b1385 100644 (file)
--- 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 f81077c6fb47ef54d48da39f8aa0274d25b2512a..98c0373831b21785f0bdb22a3bc8e617bf9835b8 100644 (file)
--- 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 (file)
index 0000000..85f9c89
--- /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 (file)
index 0000000..723dd58
--- /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 (file)
index 0000000..9ee7e8f
--- /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 (file)
index 0000000..30d49ad
--- /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)