projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2bf6f49) | patch
FP: Add option to word-blast more lazily. (#6904)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 23 Jul 2021 17:51:22 +0000 (10:51 -0700)
committerGitHub <noreply@github.com>
Fri, 23 Jul 2021 17:51:22 +0000 (17:51 +0000)
commit6931c8b3d078e9f5386837955dde2d786fcb1547
treeba4d6762714f4d4d6aca57f23d24c983fb5db311tree
parent2bf6f49039b7c9fee6a7da846e329eb9be75713ccommit | diff
FP: Add option to word-blast more lazily. (#6904)

When enabled, this does not word-blast when registering term but at preNotifyFact (= more lazily) instead.
This is enabled via option --fp-lazy-wb.
src/options/fp_options.toml diff | blob | history
src/theory/bv/bv_solver_bitblast.h diff | blob | history
src/theory/fp/fp_converter.cpp diff | blob | history
src/theory/fp/fp_converter.h diff | blob | history
src/theory/fp/theory_fp.cpp diff | blob | history
src/theory/fp/theory_fp.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fp/word-blast.smt2 [new file with mode: 0644] blob