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

author	yoni206 <yoni206@users.noreply.github.com>
	Mon, 13 Dec 2021 16:16:08 +0000 (18:16 +0200)
committer	GitHub <noreply@github.com>
	Mon, 13 Dec 2021 16:16:08 +0000 (16:16 +0000)
commit	ad885db118e388687be7f657ddc943e74a0a9601
tree	7759b009f9fe21aba612fac7ce7752faa408dadb	tree
parent	05f2d5f39a2e1021bbaf8fc5ba3c9a0d053759a1	commit \| diff

Integrate new int-blaster (#7781)

This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module.

Tests are updated and added, as well as other minor changes.

Solves the following issues (and contains corresponding tests):
cvc5/cvc5-projects#345
cvc5/cvc5-projects#344
cvc5/cvc5-projects#343

@mpreiner FYI

35 files changed:

src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.h		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/bv/int_blaster.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
test/api/cpp/CMakeLists.txt		diff \| blob \| history
test/api/cpp/proj-issue344.cpp	[new file with mode: 0644]	blob
test/api/cpp/proj-issue345.cpp	[new file with mode: 0644]	blob
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/bv/bv_to_int1.smt2		diff \| blob \| history
test/regress/regress0/bv/bv_to_int_bvmul2.smt2		diff \| blob \| history
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2		diff \| blob \| history
test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2		diff \| blob \| history
test/regress/regress0/bv/bv_to_int_elim_err.smt2		diff \| blob \| history
test/regress/regress0/bv/bv_to_int_int1.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/bv_to_int_zext.smt2		diff \| blob \| history
test/regress/regress0/bv/proj-issue343.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bv_to_int2.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_ashr.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_bitwise.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_bvmul1.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_inc1.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_mask_array_1.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_mask_array_2.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_mask_array_3.smt2		diff \| blob \| history
test/regress/regress2/bv_to_int_quantifiers_bvand.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bv_to_int_shifts.smt2		diff \| blob \| history
test/regress/regress3/bv_to_int_and_or.smt2		diff \| blob \| history
test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2		diff \| blob \| history
test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2		diff \| blob \| history
test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2		diff \| blob \| history
test/unit/theory/theory_bv_int_blaster_white.cpp		diff \| blob \| history

RSS Atom