projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 27113b1) | patch
[BV] Fix strategy for rewriting `bvnot` (#8297)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 15 Mar 2022 22:20:09 +0000 (15:20 -0700)
committerGitHub <noreply@github.com>
Tue, 15 Mar 2022 22:20:09 +0000 (22:20 +0000)
commit55e02fa8ed99769cdc3546090f42daaeb326b639
tree2f39bf73599816d0ccf83a4242fcf416349ff545tree
parent27113b19f92c94047521c46c882fe74b4d063ccccommit | diff
[BV] Fix strategy for rewriting `bvnot` (#8297)

Fixes #8240. The currenty strategy was returning REWRITE_DONE
incorrectly, e.g., when we had a term like (bvnot (bvnot (bvnot #b0)))
because EvalNot was applied before NotIdemp, so we did not evaluate
the innermost bvnot after removing the double bvnot. The commit
fixes the strategy s.t. we are allowed to return REWRITE_DONE.
src/theory/bv/theory_bv_rewrite_rules_simplification.h diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/issue8240-rewrite-bvnot.smt2 [new file with mode: 0644] blob