From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Jul 2022 19:15:07 +0000 (-0500)
Subject: Do not eagerly preprocess seq.nth (#8937)
X-Git-Tag: cvc5-1.0.1~16
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd6db957a9c780216624fac2d58fd8a9ea51aec2;p=cvc5.git

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 8d5687ec2..8c0ab9038 100644
--- 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 49691d35c..9b10066ea 100644
--- 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 a5979dd5b..67c6cc8d4 100644
--- 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
index 000000000..acbb67b80
--- /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 afa6fa238..7b75f724b 100644
--- 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)