projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0e08fa4) | patch
Eliminate use of quantifiers engine in enumerative instantiation (#6217)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 29 Mar 2021 15:00:33 +0000 (10:00 -0500)
committerGitHub <noreply@github.com>
Mon, 29 Mar 2021 15:00:33 +0000 (15:00 +0000)
commit064bce0045368fd74beee10f3545899de2d20bf9
tree2d47102709656fcd14b2151ae7ba44fcfaf85fc7tree
parent0e08fa4ff925b201d42544dd4b28c74d1b245bd7commit | diff
Eliminate use of quantifiers engine in enumerative instantiation (#6217)

This also makes minor updates to how term tuple enumerators are constructed.
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.cpp diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.h diff | blob | history