projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8828e54) | patch
Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 3 Sep 2020 22:58:03 +0000 (00:58 +0200)
committerGitHub <noreply@github.com>
Thu, 3 Sep 2020 22:58:03 +0000 (17:58 -0500)
commit19ff08d652de2890eee4674d2a6debe10e879f1f
treea1e10e4c354fd44bd1073683b2e4edea8a054e41tree
parent8828e545cfb838d806a0ad382671a9af131e8431commit | diff
Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)

Motivated by #4936, this PR adds a new BV rewrite rule:
(bvugt (bvurem T x) x) ==> (ite (= x 0) (bvugt T 0) false)
Fixes #4936.
src/theory/bv/theory_bv_rewrite_rules.h diff | blob | history
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/pr4993-bvugt-bvurem-a.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 [new file with mode: 0644] blob