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

[cvc5.git] / src / theory / quantifiers / quantifiers_rewriter.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-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-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-27	Morgan Deters	Merge branch '1.3.x'	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	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-17	Kshitij Bansal	Merge branch '1.3.x'	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
2013-12-03	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-11-27	Andrew Reynolds	Bug fix for E-matching select terms, minor fix for...	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-09-15	Andrew Reynolds	Change default option of simple ite lifting within...	blob \| commitdiff \| raw \| diff to current
2013-08-26	Kshitij Bansal	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-25	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-19	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-17	Andrew Reynolds	Make --var-elim-quant true by default. Add rewrite...	blob \| commitdiff \| raw \| diff to current
2013-06-04	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-03	Morgan Deters	Merge tag 'casc24'	blob \| commitdiff \| raw \| diff to current
2013-05-29	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-22	Andrew Reynolds	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-05-22	Andrew Reynolds	Significant work on bounded integer quantification...	blob \| commitdiff \| raw \| diff to current
2013-05-03	Tim King	Merging branch 'soiquickexplain'.	blob \| commitdiff \| raw \| diff to current
2013-05-03	Tim King	Merge branch 'fcexplanations'	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	fixed merge conflicts	blob \| commitdiff \| raw \| diff to current
2013-04-30	Andrew Reynolds	Add option in quantifiers for clause splitting	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	Regenerated copyrights: canonicalized names, no emails	blob \| commitdiff \| raw \| diff to current
2013-04-02	Morgan Deters	update copyrights	blob \| commitdiff \| raw \| diff to current
2013-03-30	Andrew Reynolds	do simple ite rewriting within quantifiers	blob \| commitdiff \| raw \| diff to current
2013-03-15	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-03-14	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-03-13	lianah	post failed attempts at getting the incremental solver...	blob \| commitdiff \| raw \| diff to current
2013-03-06	Andrew Reynolds	fixed two bugs for the new E-matching implementation...	blob \| commitdiff \| raw \| diff to current
2012-11-13	Andrew Reynolds	refactoring of quantifiers rewriter based on code revie...	blob \| commitdiff \| raw \| diff to current
2012-11-10	Tim King	Fix to quantifier rewritting not being idempotent....	blob \| commitdiff \| raw \| diff to current
2012-10-29	Andrew Reynolds	more updates and minor bug fixes for fmf/inst-gen quant...	blob \| commitdiff \| raw \| diff to current
2012-10-16	Andrew Reynolds	more cleanup of quantifiers code	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-10-01	Andrew Reynolds	initial draft of skolemization during pre-processing...	blob \| commitdiff \| raw \| diff to current
2012-09-19	Morgan Deters	General subscriber infrastructure for NodeManager,...	blob \| commitdiff \| raw \| diff to current
2012-08-27	Morgan Deters	* Reversing commit r4258 (which disabled failing regres...	blob \| commitdiff \| raw \| diff to current
2012-08-24	Morgan Deters	* disallow internal uses of mkVar() (you have to mkSkol...	blob \| commitdiff \| raw \| diff to current
2012-07-31	Morgan Deters	Options merge. This commit:	blob \| commitdiff \| raw \| diff to current
2012-07-08	Morgan Deters	another signed-ness warning fix for newer GCC	blob \| commitdiff \| raw \| diff to current
2012-07-07	Morgan Deters	Various fixes to documentation---typos, some incomplete...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Morgan Deters	Merge from quantifiers2-trunkmerge branch.	blob \| commitdiff \| raw \| diff to current

RSS Atom