git.libre-soc.org Git - cvc5.git/history - src/theory/quantifiers/quant_conflict

[cvc5.git] / src / theory / quantifiers / quant_conflict_find.cpp

2014-03-12	Andrew Reynolds	Minor fixes post-merge of RR.	blob \| commitdiff \| raw
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Andrew Reynolds	Initial refactor of rewrite rules, make theory_rewriter...	blob \| commitdiff \| raw \| diff to current
2014-03-10	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-08	Tim King	Merge remote-tracking branch 'CVC4root/master'	blob \| commitdiff \| raw \| diff to current
2014-03-08	Morgan Deters	Remove --ite-remove-quant; support pulling ground ITEs...	blob \| commitdiff \| raw \| diff to current
2014-03-01	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-27	Andrew Reynolds	Bug fix for QCF algorithm, was missing instantiations...	blob \| commitdiff \| raw \| diff to current
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-20	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-20	Andrew Reynolds	Fix ite and iff handling in QCF. Add option for heuris...	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-17	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-14	Andrew Reynolds	Make QCF more incremental. Fix bug in QCF handling...	blob \| commitdiff \| raw \| diff to current
2014-02-11	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-09	Andrew Reynolds	More complete guess instantiation strategy, cvc4 now...	blob \| commitdiff \| raw \| diff to current
2014-02-05	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-05	Andrew Reynolds	Bug fix for theory strings related to old cycle detecti...	blob \| commitdiff \| raw \| diff to current
2014-02-04	Andrew Reynolds	Add variable ordering for QCF to accelerate matching...	blob \| commitdiff \| raw \| diff to current
2014-02-03	Andrew Reynolds	Handle nested (universal) quantifiers in QCF algorithm...	blob \| commitdiff \| raw \| diff to current
2014-01-30	Andrew Reynolds	Refactor QCF slightly. Bug fix for relevant domain...	blob \| commitdiff \| raw \| diff to current
2014-01-27	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-27	Andrew Reynolds	More optimization of QCF and instantiation caching...	blob \| commitdiff \| raw \| diff to current
2014-01-26	Andrew Reynolds	More optimization of QCF. Fixed InstMatchTrie for...	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-01-24	Andrew Reynolds	Simplify the QCF algorithm by more aggressive flattenin...	blob \| commitdiff \| raw \| diff to current
2014-01-18	Andrew Reynolds	Performance optimization for E-matching, working on...	blob \| commitdiff \| raw \| diff to current
2014-01-18	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-01-18	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-17	Andrew Reynolds	More optimizations for quantifiers conflict find. ...	blob \| commitdiff \| raw \| diff to current
2014-01-17	Kshitij Bansal	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-16	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-01-15	Andrew Reynolds	Optimizations for quantifiers conflict find: better...	blob \| commitdiff \| raw \| diff to current
2014-01-10	Andrew Reynolds	Add stats to quantifiers conflict find. Added option...	blob \| commitdiff \| raw \| diff to current
2014-01-10	Andrew Reynolds	Add new method --quant-cf for finding conflicts eagerly...	blob \| commitdiff \| raw \| diff to current

RSS Atom