projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a1c9b74) | patch
BV instantiator: Factor out util functions. (#2604)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 9 Oct 2018 02:44:22 +0000 (19:44 -0700)
committerGitHub <noreply@github.com>
Tue, 9 Oct 2018 02:44:22 +0000 (19:44 -0700)
commit0d310d6716d1ab679cd466a2e47e5c0f6cdd8569
tree146e3a070038a6d847204c5f4173d9a3bf7b619dtree
parenta1c9b7408ee47ea69ef9866cdac75f839c14bc8dcommit | diff
BV instantiator: Factor out util functions. (#2604)

Previously, all util functions for the BV instantiator were static functions
in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding
unit test, it was therefore required to include this cpp file in order to
test these functions. This factors out these functions into a
theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h).

Asan reported errors for the corresponing unit test because of this.
src/CMakeLists.txt diff | blob | history
src/Makefile.am diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp [new file with mode: 0644] blob
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h [new file with mode: 0644] blob
test/unit/theory/theory_quantifiers_bv_instantiator_white.h diff | blob | history