projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c9747ae) | patch
Remove preregister instantiation heuristic (#5713)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Dec 2020 07:49:28 +0000 (01:49 -0600)
committerGitHub <noreply@github.com>
Tue, 22 Dec 2020 07:49:28 +0000 (08:49 +0100)
commit85da37188e1b206fb3dccf202633cf4c1d22da7c
tree393b504da1f95943da51eb096b238ca2310228cbtree
parentc9747ae3a0577498073a04de97a978e1d9464d5dcommit | diff
Remove preregister instantiation heuristic (#5713)

This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.
src/options/quantifiers_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_instantiator.h diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h diff | blob | history
test/regress/regress0/sygus/aig-si.sy diff | blob | history
test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2 diff | blob | history
test/regress/regress1/sygus/parity-si-rcons.sy diff | blob | history