projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7c0191f) | patch
Clean enumerative instantiation options (#7947)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Jan 2022 22:56:46 +0000 (16:56 -0600)
committerGitHub <noreply@github.com>
Fri, 14 Jan 2022 22:56:46 +0000 (22:56 +0000)
commit9b120a987bc0421d2fd9029ec9b9b7c6a78c3897
treee89f9e7ed7262f4ae7421613efb2d57be4343365tree
parent7c0191f914405b6f88eba838af101e045de2d933commit | diff
Clean enumerative instantiation options (#7947)

--full-saturate-quant is kept as a generic option, and implies --enum-inst.
contrib/competitions/smt-comp/run-script-smtcomp-current diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_enumerative.h diff | blob | history
src/theory/quantifiers/inst_strategy_pool.cpp diff | blob | history
src/theory/quantifiers/quantifiers_modules.cpp diff | blob | history
test/regress/regress1/quantifiers/issue3481.smt2 diff | blob | history
test/regress/regress2/quantifiers/syn874-1.smt2 diff | blob | history