Do not eagerly preprocess seq.nth (#8937)

Fixes #8936.

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8d5687ec22f05b53507884dc414332d4a9f1b907..8c0ab9038dfafeefc761cf8ba6d9bed7090b4168 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -1065,7 +1065,12 @@ Node StringsPreprocess::simplifyRec(Node t, std::vector<Node>& asserts)
       if( changed ){
         tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
       }
-      retNode = simplify(tmp, asserts);
+      // We cannot statically reduce seq.nth due to it being partial function.
+      // Reducing it here would violate the functional property of seq.nth.
+      if (tmp.getKind() != SEQ_NTH)
+      {
+        retNode = simplify(tmp, asserts);
+      }
     }
     d_visited[t] = retNode;
     return retNode;

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index 49691d35c6f68a02f32ae66ca2a090c3c86d0121..9b10066ea002aaab5e78ece740b3cfaff91c8b36 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -83,6 +83,8 @@ class StringsPreprocess : protected EnvObj
    *   (exists k) asserts => t = t'
    * is valid, where k are the free skolems introduced when constructing
    * asserts.
+   *
+   * This method is called only for eager preprocessing of extended functions.
    */
   Node processAssertion(Node t, std::vector<Node>& asserts);
 
@@ -97,6 +99,8 @@ class StringsPreprocess : protected EnvObj
    * Applies simplify to all top-level extended function subterms of t. New
    * assertions created in this reduction are added to asserts. The argument
    * visited stores a cache of previous results.
+   *
+   * This method is called only for eager preprocessing of extended functions.
    */
   Node simplifyRec(Node t, std::vector<Node>& asserts);
   /**

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index a5979dd5b5f757f21a67050b366074515ef9b302..67c6cc8d4f8b52793f060cdb134a64e399bd1d1a 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2440,6 +2440,7 @@ set(regress_1_tests
   regress1/sep/wand-simp-unsat.smt2
   regress1/seq/issue8148-2-const-mv.smt2
   regress1/seq/issue8148-const-mv.smt2
+  regress1/seq/issue8936-nth-eager-red.smt2
   regress1/sets/choose.cvc.smt2
   regress1/sets/choose1.smt2
   regress1/sets/choose2.smt2

diff --git a/test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2 b/test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2
new file mode 100644 (file)
index 0000000..acbb67b
--- /dev/null
+++ b/test/regress/cli/regress1/seq/issue8936-nth-eager-red.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () (Seq Int))
+(declare-fun b () (Seq Int))
+(declare-fun c () Int)
+(assert (= a b))
+(assert (not (= (seq.nth a c) (seq.nth b c))))
+(check-sat)

diff --git a/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2 b/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2
index afa6fa238d50f8bb123c71d524710a7973b853e2..7b75f724bf3245d71e6d6a34da3365e93ae76f10 100644 (file)
--- a/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2
+++ b/test/regress/cli/regress1/strings/issue6777-seq-nth-eval-cm.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE: --strings-exp -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)