projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dc9af86) | patch
New BV rewrite rules aimed at bv_to_int preprocessing pass (#4769)
authoryoni206 <yoni206@users.noreply.github.com>
Mon, 3 Aug 2020 22:28:29 +0000 (15:28 -0700)
committerGitHub <noreply@github.com>
Mon, 3 Aug 2020 22:28:29 +0000 (17:28 -0500)
commit2fb5ff63e8e80b06450a8a2a33d7d61cc0a0e2ac
tree25f5db204a8f2ba1bdbca779fbc8127212c99806tree
parentdc9af8641003b8c0efd8a952095dfa76997983c1commit | diff
New BV rewrite rules aimed at bv_to_int preprocessing pass (#4769)

This PR adds new rewrite rules for BV.
None of them is meant to be used by the default BV rewriter.
However, they are planned to be used in bv_to_int preprocessing pass.
In the pass we use FixpointRewriteStrategy to call various rewrite rules.
After consulting @4tXJ7f , we thought that the best way to include more rewrite rules in that call is to implement them using the existing BV rewrites infrastructure.
src/theory/bv/theory_bv_rewrite_rules.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h diff | blob | history