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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Tue, 22 Sep 2020 22:40:48 +0000 (15:40 -0700)
committer	GitHub <noreply@github.com>
	Tue, 22 Sep 2020 22:40:48 +0000 (17:40 -0500)
commit	30e6dc83aed15ef002087e55cf228f0735c63f40
tree	76547d252a34cc2b56015957e2d5f9740b1002b2	tree
parent	e4a29a6033ecc7ba5ec266f37e8f151f09ead020	commit \| diff

Add simple BV solver (#5065)

This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.

21 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/bv_options.toml		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/theory/bv/bv_solver.h		diff \| blob \| history
src/theory/bv/bv_solver_simple.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_solver_simple.h	[new file with mode: 0644]	blob
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/theory_state.cpp		diff \| blob \| history
src/theory/theory_state.h		diff \| blob \| history
test/regress/regress0/bv/ackermann1.smt2		diff \| blob \| history
test/regress/regress0/bv/bool-model.smt2		diff \| blob \| history
test/regress/regress0/bv/bool-to-bv-ite.smt2		diff \| blob \| history
test/regress/regress0/bv/bug734.smt2		diff \| blob \| history
test/regress/regress0/bv/issue-4076.smt2		diff \| blob \| history
test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2		diff \| blob \| history
test/regress/regress1/bug520.smt2		diff \| blob \| history