projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 46c7d9d) | patch
Add option for using bound inference for relevant assertions (#7152)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 8 Sep 2021 16:33:40 +0000 (11:33 -0500)
committerGitHub <noreply@github.com>
Wed, 8 Sep 2021 16:33:40 +0000 (16:33 +0000)
commitddce3af579b12b3eb8f69baec3806bc33f4ac23c
treee2b49c145544fe9245fd6cb40ed30831125df79btree
parent46c7d9d919c40962ec0c538754dac5a975eedb25commit | diff
Add option for using bound inference for relevant assertions (#7152)

The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.
src/options/arith_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history