projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8ca7aa9) | patch
Rewrite POW to POW2 when the base is 2 (#6806)
authoryoni206 <yoni206@users.noreply.github.com>
Mon, 28 Jun 2021 23:42:13 +0000 (16:42 -0700)
committerGitHub <noreply@github.com>
Mon, 28 Jun 2021 23:42:13 +0000 (23:42 +0000)
commit5652f1bcb3702ff60ebe3248a6e027a3138d5c99
tree038f1a3ae4ec8567858420645c87abdaec1dca37tree
parent8ca7aa981af4c6229746aa0c1b3f3f67ddb68b23commit | diff
Rewrite POW to POW2 when the base is 2 (#6806)

This PR introduces a rewrite from (^ 2 t) to (pow2 t) in order to make use of the specialized pow2 solver.
One regression that expects an error when t is not a constant is changed accordingly.
src/theory/arith/arith_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/pow2-pow.smt2 [new file with mode: 0644] blob
test/regress/regress1/arith/bug716.1.cvc diff | blob | history