projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 531ec6e) | patch
Fix ite and iff handling in QCF. Add option for heuristic instantiation in QCF ...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 20 Feb 2014 16:37:32 +0000 (10:37 -0600)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 20 Feb 2014 16:37:46 +0000 (10:37 -0600)
commitf37804c3da98f4eb1888991fd8b7157437aeeb44
tree0baeed78ff7107a2f8ac32d8b2a8cc3d6e10de91tree
parent531ec6e52b75cd2f600a3fc781383e7539f2335acommit | diff
Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF (not working yet).  Improve automatic option setting for quantifiers.
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/modes.h diff | blob | history
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/quant_conflict_find.h diff | blob | history