From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Apr 2020 23:48:21 +0000 (-0500)
Subject: Remove skolem share involving pre_first_ctn. (#4423)
X-Git-Tag: cvc5-1.0.0~3327
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c402c2b3cc036748c83bd75629e9845f9b5a397;p=cvc5.git

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 bdce86d06..4d92c372f 100644
--- 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 38b741ced..1dcdb0a44 100644
--- 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
index 000000000..277a14df8
--- /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 8f41153f3..7cb735a16 100644
--- 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: