diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-15 15:19:43 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-15 15:19:43 -0600 |
| commit | de79f1ad325036ca90be9144a74606310b5dab9b (patch) | |
| tree | ff025f0ccc846073327b1ad823eb9d255f4a8843 /test/regress/regress0/strings | |
| parent | eb6155c5f078a26b7cdddddad6e209fad0f825f8 (diff) | |
Implement --no-strings-lazy-pp as a preprocessing pass (#5777)
This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.
Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.
Diffstat (limited to 'test/regress/regress0/strings')
4 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/issue5608-eager-pp.smt2 b/test/regress/regress0/strings/issue5608-eager-pp.smt2 new file mode 100644 index 000000000..a1a166277 --- /dev/null +++ b/test/regress/regress0/strings/issue5608-eager-pp.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-strings-lazy-pp -i +; EXPECT: sat +; EXPECT: sat +; EXPECT: unsat +(set-logic QF_SLIA) +(declare-fun v6 () Bool) +(declare-fun str6 () String) +(assert (and v6 (str.in_re (str.replace str6 (str.from_int 12) str6) (str.to_re str6)))) +(check-sat) +(check-sat) +(assert (not v6)) +(check-sat) diff --git a/test/regress/regress0/strings/issue5745-eager-pp.smt2 b/test/regress/regress0/strings/issue5745-eager-pp.smt2 new file mode 100644 index 000000000..b869a9ded --- /dev/null +++ b/test/regress/regress0/strings/issue5745-eager-pp.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-strings-lazy-pp +; EXPECT: sat +(set-logic ALL) +(declare-fun i0 () Int) +(declare-fun str4 () String) +(assert (= str4 (str.substr str4 (mod i0 2) 1))) +(assert (not (= "" str4))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5767-eager-pp.smt2 b/test/regress/regress0/strings/issue5767-eager-pp.smt2 new file mode 100644 index 000000000..5e4d29d5a --- /dev/null +++ b/test/regress/regress0/strings/issue5767-eager-pp.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-strings-lazy-pp -q +; EXPECT: sat +(set-logic ALL) +(declare-fun s () String) +(assert (xor (= (str.at s (div 0 0)) "A") (= (div 0 (str.len s)) 0))) +(check-sat) diff --git a/test/regress/regress0/strings/issue5771-eager-pp.smt2 b/test/regress/regress0/strings/issue5771-eager-pp.smt2 new file mode 100644 index 000000000..c3049e72f --- /dev/null +++ b/test/regress/regress0/strings/issue5771-eager-pp.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --no-strings-lazy-pp +; EXPECT: sat +(set-logic ALL) +(declare-fun a () Int) +(assert (str.suffixof "B" (str.from_code a))) +(check-sat) |