Require `--strings-exp` when using `str.substr` (#4916)

Fixes #4915. Previously, `str.substr` did not require `--strings-exp`.
However, when `--strings-exp` is not active, we do not send terms to the
extended solver for registration, which meant that `str.substr` was
never reduced. This commit adds `str.substr` to the operators that
require `--strings-exp`.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 71b45915fc0a9998e1e46cc3d14d7b73c5bb13d5..353e89668c7fdfcfb84dd1c84ecc4d748c9375c4 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -136,7 +136,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   if (!options::stringExp())
   {
     if (k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI
-        || k == STRING_STRREPL || k == STRING_STRREPLALL
+        || k == STRING_STRREPL || k == STRING_SUBSTR || k == STRING_STRREPLALL
         || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL
         || k == STRING_STRCTN || k == STRING_LEQ || k == STRING_TOLOWER
         || k == STRING_TOUPPER || k == STRING_REV || k == STRING_UPDATE)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 870d83e7e5badb97a30aa1d586598e4ea159ff8c..e7ca73a75622a7e043fc7c1a413ed03ce33a6b68 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -981,6 +981,7 @@ set(regress_0_tests
   regress0/strings/issue4662-consume-nterm.smt2
   regress0/strings/issue4674-recomp-nf.smt2
   regress0/strings/issue4820.smt2
+  regress0/strings/issue4915.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2

diff --git a/test/regress/regress0/seq/intseq.smt2 b/test/regress/regress0/seq/intseq.smt2
index e9d07e050891375efd81b5a22db70435df48f677..25bbd34d8debde7d0da12f19bf3619c7f1f3c284 100644 (file)
--- a/test/regress/regress0/seq/intseq.smt2
+++ b/test/regress/regress0/seq/intseq.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 ;EXPECT: unsat
 (set-logic ALL)
 (declare-fun tickleBool (Bool) Bool)

diff --git a/test/regress/regress0/seq/intseq_dt.smt2 b/test/regress/regress0/seq/intseq_dt.smt2
index 36d2f484249428f42009fc39211872fea7f497de..e7bdcd94b4ce59401a74b181dbc3c7a90b40e9f8 100644 (file)
--- a/test/regress/regress0/seq/intseq_dt.smt2
+++ b/test/regress/regress0/seq/intseq_dt.smt2
@@ -1,4 +1,4 @@
-;COMMAND-LINE: --dt-nested-rec
+;COMMAND-LINE: --dt-nested-rec --strings-exp
 ;EXPECT: unsat
 (set-logic ALL)
 (declare-fun tickleBool (Bool) Bool)

diff --git a/test/regress/regress0/seq/seq-ex3.smt2 b/test/regress/regress0/seq/seq-ex3.smt2
index abafdeddf47bd9c77bec6e08765235bde8bf13ca..dfaa12301b05409c842588b7573ad97da65430bc 100644 (file)
--- a/test/regress/regress0/seq/seq-ex3.smt2
+++ b/test/regress/regress0/seq/seq-ex3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-fun x () (Seq (Seq Int)))

diff --git a/test/regress/regress0/seq/seq-ex4.smt2 b/test/regress/regress0/seq/seq-ex4.smt2
index 93fed72c7487616c92e89d38332fc079f4288db1..439a7b0e07384b927c346f6a5e59e1e818edd6c1 100644 (file)
--- a/test/regress/regress0/seq/seq-ex4.smt2
+++ b/test/regress/regress0/seq/seq-ex4.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-fun z () (Seq Int))

diff --git a/test/regress/regress0/seq/seq-ex5-dd.smt2 b/test/regress/regress0/seq/seq-ex5-dd.smt2
index d9ef5c8ba5829c0ede06cce7c602e1b4e0d82e79..8ec8efa9d05388aeaf4c1e6630d38a36b9205bd9 100644 (file)
--- a/test/regress/regress0/seq/seq-ex5-dd.smt2
+++ b/test/regress/regress0/seq/seq-ex5-dd.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_SLIA)
 (set-info :status sat)
 (declare-fun z () (Seq Int))

diff --git a/test/regress/regress0/seq/seq-nth-uf-z.smt2 b/test/regress/regress0/seq/seq-nth-uf-z.smt2
index 0ae8a702bafcab4579a675186ec46316f03da9f3..6ab4293245be9fa27d8c969b4fcdf1a8c8017b9c 100644 (file)
--- a/test/regress/regress0/seq/seq-nth-uf-z.smt2
+++ b/test/regress/regress0/seq/seq-nth-uf-z.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 ;EXPECT: unsat
 (set-logic ALL)
 (declare-fun a () (Seq Int))
@@ -8,4 +9,4 @@
 (assert (or (= x z) (= y z)))
 (assert (not (= (seq.nth a x) (seq.nth a z))))
 (assert (not (= (seq.nth b y) (seq.nth b z))))
-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress0/seq/seq-nth-uf.smt2 b/test/regress/regress0/seq/seq-nth-uf.smt2
index af0b93170900428221729c4cfe3df8dad0f4e0d1..9c569e6e7aac852bcb282b25de1f15cbb11b68ce 100644 (file)
--- a/test/regress/regress0/seq/seq-nth-uf.smt2
+++ b/test/regress/regress0/seq/seq-nth-uf.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_UFSLIA)
 (set-info :status unsat)
 (declare-fun a () (Seq Int))

diff --git a/test/regress/regress0/seq/seq-nth-undef.smt2 b/test/regress/regress0/seq/seq-nth-undef.smt2
index 765b3e2f626426f1164a734f3596ad1ce72ac182..3ff2ab0966611ed4f80ee0125462d6fbdade2617 100644 (file)
--- a/test/regress/regress0/seq/seq-nth-undef.smt2
+++ b/test/regress/regress0/seq/seq-nth-undef.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 ;EXPECT: sat
 (set-logic ALL)
 (declare-fun s () (Seq Int))

diff --git a/test/regress/regress0/seq/seq-nth.smt2 b/test/regress/regress0/seq/seq-nth.smt2
index 765b3e2f626426f1164a734f3596ad1ce72ac182..3ff2ab0966611ed4f80ee0125462d6fbdade2617 100644 (file)
--- a/test/regress/regress0/seq/seq-nth.smt2
+++ b/test/regress/regress0/seq/seq-nth.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 ;EXPECT: sat
 (set-logic ALL)
 (declare-fun s () (Seq Int))

diff --git a/test/regress/regress0/strings/issue2958.smt2 b/test/regress/regress0/strings/issue2958.smt2
index 99d8462c34756ccf21cfb5cc715780d5af5186a2..bb7166b65221a8c084619bcfa9029c19171dae4c 100644 (file)
--- a/test/regress/regress0/strings/issue2958.smt2
+++ b/test/regress/regress0/strings/issue2958.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-info :smt-lib-version 2.6)
 (set-logic QF_SLIA)
 (set-info :status unsat)

diff --git a/test/regress/regress0/strings/issue4915.smt2 b/test/regress/regress0/strings/issue4915.smt2
new file mode 100644 (file)
index 0000000..e65db3c
--- /dev/null
+++ b/test/regress/regress0/strings/issue4915.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-const Str4 String)
+(declare-const Str18 String)
+(assert (str.in_re Str18 (re.++ (str.to_re Str4) (str.to_re "ewgysobutx"))))
+(assert (= Str18 (str.++ Str4 "ewgysobutx")))
+(assert (>= (str.len (str.substr Str18 0 3)) 937))
+(check-sat)

diff --git a/test/regress/regress0/strings/re.all.smt2 b/test/regress/regress0/strings/re.all.smt2
index d17a0d0499bbb6130a3706de46f9394e982a2895..01d57a6e133cb883ee5eeaab8d7582be54b91df0 100644 (file)
--- a/test/regress/regress0/strings/re.all.smt2
+++ b/test/regress/regress0/strings/re.all.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (declare-const x String)

diff --git a/test/regress/regress0/strings/strings-charat.cvc b/test/regress/regress0/strings/strings-charat.cvc
index 71114d39db50c99277e1a830ed76dacc82c629cc..76c686dbf425696f2cc9b993702be050e1c9557c 100644 (file)
--- a/test/regress/regress0/strings/strings-charat.cvc
+++ b/test/regress/regress0/strings/strings-charat.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --strings-exp
 % EXPECT: unsat
 
 x : STRING;

diff --git a/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2 b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2
index 31a57fc8b449eb0abe1362a076bc3d19d3d9a357..a1b1dc62883512ff1c27a3872654281239aa1b83 100644 (file)
--- a/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2
+++ b/test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun s () String)

diff --git a/test/regress/regress1/strings/at001.smt2 b/test/regress/regress1/strings/at001.smt2
index 04933b8f7ea10de7ccdc85ab4185a8d6a4972693..8dd84a55c81fddf7a05e90cfee404b9673529d8d 100644 (file)
--- a/test/regress/regress1/strings/at001.smt2
+++ b/test/regress/regress1/strings/at001.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_SLIA)
 (set-info :status sat)
 

diff --git a/test/regress/regress1/strings/substr001.smt2 b/test/regress/regress1/strings/substr001.smt2
index 47fa995ff91345853aa0d865adc3ecdbabb405d4..00caf42cee687a64209d46d91902d8816f9c5993 100644 (file)
--- a/test/regress/regress1/strings/substr001.smt2
+++ b/test/regress/regress1/strings/substr001.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --strings-exp
 (set-logic QF_SLIA)
 (set-info :status sat)