projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0e09af0) | patch
Enhancement: make the bool-to-bv pass more robust and targeted (#3021)
authormakaimann <makaim@stanford.edu>
Tue, 10 Mar 2020 04:13:21 +0000 (21:13 -0700)
committerGitHub <noreply@github.com>
Tue, 10 Mar 2020 04:13:21 +0000 (21:13 -0700)
commit5cbc35e70c2a80094dade1a58605882e3eb1d326
tree5ec95a56e934b8aeb119ba8ad289ae720401013ctree
parent0e09af0be57ec4df28869e4383a40d847c0a6b5acommit | diff
Enhancement: make the bool-to-bv pass more robust and targeted (#3021)

This pull request is an improvement to the bool-to-bv preprocessing pass. The existing pass is both too weak and too strong, depending on the circumstance. Throughout this description, "lower" refers to lowering a boolean to a bit-vector.
src/preprocessing/passes/bool_to_bv.cpp diff | blob | history
src/preprocessing/passes/bool_to_bv.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bool-to-bv-all-array-bool.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bool-to-bv-all-test.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bool-to-bv-ite-array-bool.smt2 [new file with mode: 0644] blob