diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-01 17:02:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 22:02:33 +0000 |
| commit | ef2f19f8ba2a72d43586d1f4f364822dbe389aec (patch) | |
| tree | 24bab218bc3930f360010f537a0be6cbefe0433d /test | |
| parent | 7fa534c85cbb6eb2863f10840b39501a21acc0b9 (diff) | |
Simplify caching of regular expression unfolding (#6262)
This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context.
This fixes the second benchmark from #6203.
This PR also improves our traces for checking models in strings.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6203-2-re-ccache.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 232a7f7ab..64c584f7a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2040,6 +2040,7 @@ set(regress_1_tests regress1/strings/issue6132-non-unique-skolem.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 regress1/strings/issue6191-replace-all.smt2 + regress1/strings/issue6203-2-re-ccache.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 b/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 new file mode 100644 index 000000000..2deffdadd --- /dev/null +++ b/test/regress/regress1/strings/issue6203-2-re-ccache.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(assert + (xor (str.in_re a (re.++ (re.* re.allchar) (str.to_re "A") re.allchar (re.* re.allchar))) + (str.in_re a (re.++ (re.* (str.to_re a)) (str.to_re "A") re.allchar)))) +(check-sat) |