projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 65e5a90) | patch
bv: Refactor ppRewrite and move to TheoryBV. (#7271)
authorMathias Preiner <mathias.preiner@gmail.com>
Thu, 30 Sep 2021 19:52:09 +0000 (12:52 -0700)
committerGitHub <noreply@github.com>
Thu, 30 Sep 2021 19:52:09 +0000 (19:52 +0000)
commit31c108fadfd76419b57d89dae4ca5e8b4487c4af
tree53e6cd4a3401ed368d3e61beb6153e9dae1b62a7tree
parent65e5a909b10855d2e6b3844f7bc4efb7fbe4fe2fcommit | diff
bv: Refactor ppRewrite and move to TheoryBV. (#7271)

This commit moves and refactors the ppRewrite() and ppStaticLearn() code from the layered solver to TheoryBV in order to apply a default set of preprocessing rules for each solver. BV solver can still implement additional rules.

Note: Some of the rewrite rules in ppRewrite() have been removed since cluster runs showed that they don't improve anything, but actually makes the solver a lot worse.
src/options/bv_options.toml diff | blob | history
src/preprocessing/passes/bv_intro_pow2.cpp diff | blob | history
src/preprocessing/passes/bv_intro_pow2.h diff | blob | history
src/theory/bv/bv_solver_layered.cpp diff | blob | history
src/theory/bv/bv_solver_layered.h diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history