git.libre-soc.org Git - cvc5.git/commit

author	Mathias Preiner <mathias.preiner@gmail.com>
	Fri, 4 Sep 2020 01:34:19 +0000 (18:34 -0700)
committer	GitHub <noreply@github.com>
	Fri, 4 Sep 2020 01:34:19 +0000 (18:34 -0700)
commit	c9e23f66383a4d490aca6d082d40117fe799ee4b
tree	21c4aaf67d7d1b0c188d9e99d3b364883618b479	tree
parent	a5b834d5af88e372d9c6340653f831a09daf1d39	commit \| diff

Split lazy bit-vector solver from TheoryBV (#5009)

This commit separates the lazy bit-vector solver from TheoryBV, which is now a thin wrapper around a bit-vector solver d_internal . This will allow us to easily swap out the bit-vector solver in the future.

28 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/eager_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/lazy_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.cpp		diff \| blob \| history
src/theory/bv/bv_eager_solver.h		diff \| blob \| history
src/theory/bv/bv_quick_check.cpp		diff \| blob \| history
src/theory/bv/bv_quick_check.h		diff \| blob \| history
src/theory/bv/bv_solver.h	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_lazy.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_lazy.h	[new file with mode: 0644]	blob
src/theory/bv/bv_subtheory.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.h		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/theory_state.cpp		diff \| blob \| history
src/theory/theory_state.h		diff \| blob \| history
test/unit/theory/theory_bv_white.h		diff \| blob \| history

RSS Atom