projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7bb6e79) | patch
Avoid non-terminating check with assumptions in strings rewriter (#7503)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 27 Oct 2021 16:07:19 +0000 (11:07 -0500)
committerGitHub <noreply@github.com>
Wed, 27 Oct 2021 16:07:19 +0000 (16:07 +0000)
commit9cf32b5d3f12a886779b85066d8c5997b49aefc1
treea777c7d24726e3dfee4575864920466163323487tree
parent7bb6e7970de3719308110dd993cf4393031b8d80commit | diff
Avoid non-terminating check with assumptions in strings rewriter (#7503)

These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.

Instead, these rewrites are now moved to the extended rewriter.
src/theory/quantifiers/extended_rewrite.cpp diff | blob | history
src/theory/quantifiers/extended_rewrite.h diff | blob | history
src/theory/strings/arith_entail.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 [new file with mode: 0644] blob
test/unit/theory/sequences_rewriter_white.cpp diff | blob | history