projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c6e6639) | patch
Fix relevant domain for parametric operators (#7198)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 16 Sep 2021 17:14:07 +0000 (12:14 -0500)
committerGitHub <noreply@github.com>
Thu, 16 Sep 2021 17:14:07 +0000 (17:14 +0000)
commit59cb18f291e5c3a583f8e8b8b5820ea393bd40ed
tree0394ac3b1ae86c89b498312a844f61d20f4636cetree
parentc6e663987150cab74d0e75393eef36595f9764b9commit | diff
Fix relevant domain for parametric operators (#7198)

Fixes #6531.

This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types.

It does some cleanup on relevant domain in the process.
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.cpp diff | blob | history