projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c3f7c3c) | patch
Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Apr 2020 21:27:29 +0000 (16:27 -0500)
committerGitHub <noreply@github.com>
Tue, 14 Apr 2020 21:27:29 +0000 (16:27 -0500)
commitc84db60dabd8104928c7261c9df7bd9ef2917e9f
tree25dfaeb4549fc995fddbc2940d94dfe5084e8860tree
parentc3f7c3c9203a355a9c45bf820e3fea0e29b439decommit | diff
Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)

Fixes #4228. That benchmark now times out.
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/term_util.cpp diff | blob | history
src/theory/quantifiers/term_util.h diff | blob | history