projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b0d151f) | patch
Initial infrastructure for BV instantiation via word-level inversions. (#1056)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 12 Sep 2017 23:48:27 +0000 (18:48 -0500)
committerGitHub <noreply@github.com>
Tue, 12 Sep 2017 23:48:27 +0000 (18:48 -0500)
commit51cab64a53daee8e6f2693f12911c71827013f15
treedb037aaeee3d2c7d15b6395394e5df7ae47af4b7tree
parentb0d151fc69779c9e214d89683e005756a9834c2ecommit | diff
Initial infrastructure for BV instantiation via word-level inversions. (#1056)

* Initial infrastructure for BV instantiation via word-level inversions.

* Minor clean up.

* Change visited to unordered set.
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.h diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.h diff | blob | history