projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5fb5d60) | patch
Remove support for lazy BV extended function reductions and inferences (#6728)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 11 Jun 2021 13:54:32 +0000 (08:54 -0500)
committerGitHub <noreply@github.com>
Fri, 11 Jun 2021 13:54:32 +0000 (08:54 -0500)
commit18aef1113bbdb5ce8e007d115f032e425ad10797
treeeb5c01e6f7f7d48c4418db17de353eedaea4f412tree
parent5fb5d6030aa031d5f63676ec29ffa8e158fa5c6acommit | diff
Remove support for lazy BV extended function reductions and inferences (#6728)

solve-int-as-bv is now the preferred method for solving these benchmarks.

Adds solve-int-as-bv to a regression that became slow in my previous commit.
src/options/bv_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/bv/bv_solver_lazy.cpp diff | blob | history
src/theory/bv/bv_solver_lazy.h diff | blob | history
src/theory/bv/bv_subtheory_core.cpp diff | blob | history
src/theory/bv/bv_subtheory_core.h diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history
test/regress/regress1/bv/bv2nat-simp-range-sat.smt2 diff | blob | history