projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4c7f8d3) | patch
Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add support...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Feb 2014 21:44:21 +0000 (15:44 -0600)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Feb 2014 21:44:36 +0000 (15:44 -0600)
commiteb5debabce433774a0dbfd46745efb8fcf38b8ab
tree265975eab00a2919d53eb32c6bb993ed7490cbd4tree
parent4c7f8d38445f067bb85f38cf3ea343cc92e41ef2commit | diff
Make QCF more incremental.  Fix bug in QCF handling of ITE formulas, add support for ITE terms.  Add full-delay inst-when mode.  Make strings come before quantifiers in check.  Minor cleanup.
src/Makefile.am diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/modes.h 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/quant_conflict_find.h diff | blob | history
src/theory/quantifiers/trigger.h diff | blob | history