From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 19 Aug 2020 17:12:34 +0000 (-0700)
Subject: Require `--strings-exp` when using `str.substr` (#4916)
X-Git-Tag: cvc5-1.0.0~2978
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=466520464a8ed862c3a323bb2fbcc92332d9384b;p=cvc5.git

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 71b45915f..353e89668 100644
--- 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 870d83e7e..e7ca73a75 100644
--- 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 e9d07e050..25bbd34d8 100644
--- 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 36d2f4842..e7bdcd94b 100644
--- 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 abafdeddf..dfaa12301 100644
--- 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 93fed72c7..439a7b0e0 100644
--- 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 d9ef5c8ba..8ec8efa9d 100644
--- 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 0ae8a702b..6ab429324 100644
--- 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 af0b93170..9c569e6e7 100644
--- 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 765b3e2f6..3ff2ab096 100644
--- 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 765b3e2f6..3ff2ab096 100644
--- 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 99d8462c3..bb7166b65 100644
--- 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
index 000000000..e65db3c56
--- /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 d17a0d049..01d57a6e1 100644
--- 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 71114d39d..76c686dbf 100644
--- 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 31a57fc8b..a1b1dc628 100644
--- 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 04933b8f7..8dd84a55c 100644
--- 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 47fa995ff..00caf42ce 100644
--- 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)