projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 71e843a) | patch
Improvements and refactoring for enumeratative strategy (#6030)
authorMikolasJanota <MikolasJanota@users.noreply.github.com>
Thu, 11 Mar 2021 16:28:51 +0000 (17:28 +0100)
committerGitHub <noreply@github.com>
Thu, 11 Mar 2021 16:28:51 +0000 (10:28 -0600)
commitc314b0162c7fa089c400e11bd72c4ca24a26c9d0
tree76c76a32fcccce1177868da5807bd65acb0be8e0tree
parent71e843a8e9e88fc739aaa5a4a5d608004648fafacommit | diff
Improvements and refactoring for enumeratative strategy (#6030)

Refactoring out the code from  `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.

Signed-off-by: mikolas <mikolas.janota@gmail.com>
src/CMakeLists.txt diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/index_trie.cpp [new file with mode: 0644] blob
src/theory/quantifiers/index_trie.h [new file with mode: 0644] blob
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.cpp [new file with mode: 0644] blob
src/theory/quantifiers/term_tuple_enumerator.h [new file with mode: 0644] blob