projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b22b24e) | patch
bv2int: improving bvand tables (#5235)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 13 Oct 2020 17:25:25 +0000 (10:25 -0700)
committerGitHub <noreply@github.com>
Tue, 13 Oct 2020 17:25:25 +0000 (12:25 -0500)
commite9f0e4d473fe4415a93b889561656e2148fdd97f
tree7a6bc385330be35e00e2ff0aa3764ed019c4de8btree
parentb22b24ed70962fb9a5ce50d4cd202d70d7380beecommit | diff
bv2int: improving bvand tables (#5235)

The bv-to-int preprocessing pass introduces large ite terms that correspond to truth tables of bvand for various bit-widths.
Previously there were two inefficiencies in those tables:

They weren't being cached
The ite was not optimized
This PR adds a cache for the tables that induce the ite terms.
In addition, it computes smaller ite terms by computing the most common value of each table and using it as the default value of the ite.
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/theory/arith/nl/iand_table.cpp diff | blob | history
src/theory/arith/nl/iand_table.h diff | blob | history