From 466520464a8ed862c3a323bb2fbcc92332d9384b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 19 Aug 2020 10:12:34 -0700 Subject: [PATCH] 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`. --- src/theory/strings/term_registry.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/seq/intseq.smt2 | 1 + test/regress/regress0/seq/intseq_dt.smt2 | 2 +- test/regress/regress0/seq/seq-ex3.smt2 | 1 + test/regress/regress0/seq/seq-ex4.smt2 | 1 + test/regress/regress0/seq/seq-ex5-dd.smt2 | 1 + test/regress/regress0/seq/seq-nth-uf-z.smt2 | 3 ++- test/regress/regress0/seq/seq-nth-uf.smt2 | 1 + test/regress/regress0/seq/seq-nth-undef.smt2 | 1 + test/regress/regress0/seq/seq-nth.smt2 | 1 + test/regress/regress0/strings/issue2958.smt2 | 1 + test/regress/regress0/strings/issue4915.smt2 | 9 +++++++++ test/regress/regress0/strings/re.all.smt2 | 1 + test/regress/regress0/strings/strings-charat.cvc | 1 + .../regress1/quantifiers/issue2970-string-var-elim.smt2 | 1 + test/regress/regress1/strings/at001.smt2 | 1 + test/regress/regress1/strings/substr001.smt2 | 1 + 18 files changed, 27 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/strings/issue4915.smt2 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) -- 2.30.2