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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Thu, 15 Jul 2021 01:54:33 +0000 (18:54 -0700)
committer	GitHub <noreply@github.com>
	Thu, 15 Jul 2021 01:54:33 +0000 (01:54 +0000)
commit	bb6813731ef1059ab38cedcc5af026b6e75bd6be
tree	42613e96a0e119fe21fadb8e031fd92c3dbfb50c	tree
parent	ffdf7434ba53191546e13663764894852e8bc6dd	commit \| diff

bv: Rename lazy solver to layered solver. (#6889)

28 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/bv_options.toml		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_layered.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_layered.h	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_lazy.cpp	[deleted file]	blob \| history
src/theory/bv/bv_solver_lazy.h	[deleted file]	blob \| history
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/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history

RSS Atom