projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d0559a2) | patch
BV inverter: Factor out util functions. (#2603)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 9 Oct 2018 01:51:33 +0000 (18:51 -0700)
committerGitHub <noreply@github.com>
Tue, 9 Oct 2018 01:51:33 +0000 (18:51 -0700)
commita1c9b7408ee47ea69ef9866cdac75f839c14bc8d
treedb78b86653ca4372f112ce13d3b19de0c830ec8dtree
parentd0559a21f2ca71e8eaf5978e5c0707d7cf11499fcommit | diff
 BV inverter: Factor out util functions. (#2603)

Previously, all invertibility condition functions were static functions
in theory/quantifiers/bv_inverter.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/bv_inverter_utils.(cpp|h).
src/CMakeLists.txt diff | blob | history
src/Makefile.am diff | blob | history
src/theory/quantifiers/bv_inverter.cpp diff | blob | history
src/theory/quantifiers/bv_inverter_utils.cpp [new file with mode: 0644] blob
src/theory/quantifiers/bv_inverter_utils.h [new file with mode: 0644] blob
test/unit/theory/theory_quantifiers_bv_inverter_white.h diff | blob | history