projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0ec38bb) | patch
Fix for 2 dimensional dependent bounded quantifiers (#6710)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 8 Jun 2021 23:47:40 +0000 (18:47 -0500)
committerGitHub <noreply@github.com>
Tue, 8 Jun 2021 23:47:40 +0000 (23:47 +0000)
commitccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3
treef28b36f9194ccb0a43d37cc0e472f171f3645c15tree
parent0ec38bbddf9b9e37f4535a6c782f42e03f4593e0commit | diff
Fix for 2 dimensional dependent bounded quantifiers (#6710)

This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.

Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.
src/theory/quantifiers/fmf/bounded_integers.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue6635-rre.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/issue6653-4-rre.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/issue6653-rre-small.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/issue6653-rre.smt2 [new file with mode: 0644] blob