projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 558e2a0) | patch
[Strings] Fix rewriter for `re.loop` (#7956)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 17 Jan 2022 03:55:27 +0000 (19:55 -0800)
committerGitHub <noreply@github.com>
Mon, 17 Jan 2022 03:55:27 +0000 (03:55 +0000)
commit12f3384db0d6afade79252c28532ee6830fe767f
tree8cd5488f9364d838831f042781cdb41ef7d18ceetree
parent558e2a06bdd961d906c265c4fbd3abbc85ed48a3commit | diff
[Strings] Fix rewriter for `re.loop` (#7956)

Fixes cvc5/cvc5-projects#409. Our
strings/sequences rewriter was applying rewrites for re.loop in the
wrong order. As a result, it rewrote ((_ re.loop 2 1) re.all) to
re.all instead of re.none as required by the SMT-LIB standard when
the lower bound is greater than the upper bound. This commit changes the
order s.t. the bounds check happens first.
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/proj-issue409-re-loop-none.smt2 [new file with mode: 0644] blob