projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7a6c462) | patch
Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the default...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Feb 2014 14:34:59 +0000 (08:34 -0600)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Feb 2014 14:35:14 +0000 (08:35 -0600)
commit251fd73a759a8e5e94103e9b76a06491a92e425b
tree193cd049c7422b30c6a65ce119f1ac18615037f9tree
parent7a6c462b0ce3adf52a9d44a5f98c53065fedc33dcommit | diff
Bug fix for QCF algorithm, was missing instantiations.  Make prop-eq the default QCF setting.  Bug fix to prevent non-ground terms from entering relevant domains.
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history