projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 66a4efb) | patch
bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179)
authorMathias Preiner <mathias.preiner@gmail.com>
Sat, 11 Sep 2021 03:23:47 +0000 (20:23 -0700)
committerGitHub <noreply@github.com>
Sat, 11 Sep 2021 03:23:47 +0000 (03:23 +0000)
commit87453ed0f6fd123a54c7f17b958b2c2c9ca9d47b
tree448b044b8a298491ac5f3605dcd27f6d61e74c65tree
parent66a4efbf7833046373be0db7a427614be08b3160commit | diff
bv: Move IsPowerOfTwo rule to preprocessing pass and use EnvObj. (#7179)

IsPowerOfTwo rule is specific to the BvIntroPow2 preprocessing pass and should not be a general bit-vector rewrite rule.
src/preprocessing/passes/bv_intro_pow2.cpp diff | blob | history
src/preprocessing/passes/bv_intro_pow2.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_simplification.h diff | blob | history
test/regress/regress0/bv/test-bv_intro_pow2.smt2 diff | blob | history