projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5495cc0) | patch
Make inst constant attribute robust to purification variables (#8573)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 5 Apr 2022 15:45:46 +0000 (10:45 -0500)
committerGitHub <noreply@github.com>
Tue, 5 Apr 2022 15:45:46 +0000 (08:45 -0700)
commit4a388e0b0cfb872e6bb8e8024542ba20aa9f3002
tree6b092a6ef21539cd017b116c04b69edb3db7670ftree
parent5495cc021e6e7a52c6e94d8be6a471168a91c691commit | diff
Make inst constant attribute robust to purification variables (#8573)

Fixes #8572.

Certain combinations of cegqi/sygus-inst may be solution unsound when combined with E-matching, due to using skolems that have dependencies on instantiation constants are used in instantiations.
src/theory/quantifiers/ematching/candidate_generator.cpp diff | blob | history
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.cpp diff | blob | history
src/theory/quantifiers/term_util.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2 [new file with mode: 0644] blob