Remove skolem share involving pre_first_ctn. (#4423)

This fixes a soundness issue in strings caused by an incorrect skolem share.

This adds a regression that corresponds to the rewrite that this skolem share was justified by, which is "sat" (the rewrite does not hold). This benchmark in fact was answered "unsat" by CVC4 prior to this PR.

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index bdce86d0608e46fe150bb7b9a9ee3cb5d1f2c0d8..4d92c372f85c560bcd3dcc1c4ab7a63f7a32f5be 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -182,15 +182,6 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
     b = b[1];
   }
 
-  if (id == SK_FIRST_CTN_PRE)
-  {
-    // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y)
-    while (a.getKind() == kind::STRING_SUBSTR && a[1] == d_zero)
-    {
-      a = a[0];
-    }
-  }
-
   Trace("skolem-cache") << "normalizeStringSkolem end: (" << id << ", " << a
                         << ", " << b << ")" << std::endl;
   return std::make_tuple(id, a, b);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 38b741ced84083b8bccae54f08bc08f025183e3a..1dcdb0a448b534c45c730a4c7e639e289970a050 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1775,6 +1775,7 @@ set(regress_1_tests
   regress1/strings/nterm-re-inter-sigma.smt2
   regress1/strings/pierre150331.smt2
   regress1/strings/policy_variable.smt2
+  regress1/strings/pre_ctn_no_skolem_share.smt2
   regress1/strings/query4674.smt2
   regress1/strings/query8485.smt2
   regress1/strings/re-all-char-hard.smt2

diff --git a/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 b/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2
new file mode 100644 (file)
index 0000000..277a14d
--- /dev/null
+++ b/test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2
@@ -0,0 +1,18 @@
+(set-info :smt-lib-version 2.6)
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun z () String)
+(declare-fun n () Int)
+(declare-fun y () String)
+
+;(define-fun z () String "AB")
+;(define-fun n () Int 0)
+;(define-fun y () String "B")
+
+(assert (not (=
+(str.substr (str.substr z 0 n) 0 (str.indexof (str.substr z 0 n) y 0))
+(str.substr z 0 (str.indexof z y 0))
+)))
+
+(check-sat)
+(get-model)

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index 8f41153f3987d053790a2dfd126b9c658c717ba1..7cb735a162c3df494b10a718058f6dcc75d5cae8 100644 (file)
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -72,28 +72,6 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
       Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
       TS_ASSERT_EQUALS(s1, s2);
     }
-
-    // Check that skolems are shared between:
-    //
-    // SK_FIRST_CTN(c, b)
-    //
-    // SK_FIRST_CTN((str.substr c), b)
-    {
-      Node s1 = sk.mkSkolemCached(c, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      Node s2 = sk.mkSkolemCached(sc, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      TS_ASSERT_EQUALS(s1, s2);
-    }
-
-    // Check that skolems are shared between:
-    //
-    // SK_PURIFY((str.substr a 0 (str.indexof a b 0)))
-    //
-    // SK_FIRST_CTN(a, b)
-    {
-      Node s1 = sk.mkSkolemCached(sa, b, SkolemCache::SK_PURIFY, "foo");
-      Node s2 = sk.mkSkolemCached(a, b, SkolemCache::SK_FIRST_CTN_PRE, "foo");
-      TS_ASSERT_EQUALS(s1, s2);
-    }
   }
 
  private: