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

[cvc5.git] / src / theory / quantifiers_engine.h

2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw
2014-02-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw
2014-01-27	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw
2014-01-27	Andrew Reynolds	More optimization of QCF and instantiation caching...	blob \| commitdiff \| raw
2014-01-26	Andrew Reynolds	More optimization of QCF. Fixed InstMatchTrie for...	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-11-04	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-10-15	Andrew Reynolds	performance optimizations for quantifier instantiation	blob \| commitdiff \| raw \| diff to current
2013-10-15	Andrew Reynolds	performance optimizations for quantifier instantiation	blob \| commitdiff \| raw \| diff to current
2013-10-07	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-10-07	Andrew Reynolds	Multiple fixes for datatypes theory solver: add support...	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-08-26	Kshitij Bansal	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-07-02	Andrew Reynolds	Minor fixes for bounded integers, rewrite engine.	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-05-29	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-21	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-21	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-20	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-05-11	Andrew Reynolds	Preliminary version of finite model finding over bounde...	blob \| commitdiff \| raw \| diff to current
2013-05-09	Kshitij Bansal	Merge branch 'master' of ssh://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-05-09	Andrew Reynolds	Add new method for checking candidate models, --fmf...	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-20	Liana Hadarean	merged master with dejan's constant evaluating equality...	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-11	Andrew Reynolds	ite removal option for quantifiers --ite-remove-quant...	blob \| commitdiff \| raw \| diff to current
2013-03-05	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-03-01	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-26	lianah	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-24	Andrew Reynolds	added option --model-u-dt-enum for outputting uninterpr...	blob \| commitdiff \| raw \| diff to current
2013-02-17	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-16	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-15	Tim King	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-08	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-05	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-05	Kshitij Bansal	Merge remote-tracking branch 'origin/1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-05	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-04	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-04	Morgan Deters	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-04	Andrew Reynolds	Model no longer adds subterms of quantifiers to equalit...	blob \| commitdiff \| raw \| diff to current
2013-02-02	lianah	merged master into branch	blob \| commitdiff \| raw \| diff to current
2013-01-28	Andrew Reynolds	made QuantifiersEngine::d_inst_match_trie and Quantifie...	blob \| commitdiff \| raw \| diff to current
2013-01-28	Andrew Reynolds	made QuantifiersEngine::d_inst_match_trie and Quantifie...	blob \| commitdiff \| raw \| diff to current
2012-12-01	Andrew Reynolds	drastic simplification of quantifiers code regarding...	blob \| commitdiff \| raw \| diff to current
2012-11-30	Andrew Reynolds	quantifiers now uses master equality engine, preparatio...	blob \| commitdiff \| raw \| diff to current
2012-11-14	Andrew Reynolds	replaced all static member data from rewrite rule trigg...	blob \| commitdiff \| raw \| diff to current
2012-10-31	Andrew Reynolds	cleaning up some of the equality query stuff, implement...	blob \| commitdiff \| raw \| diff to current
2012-10-24	Andrew Reynolds	efficient e-matching now specific to rewrite rules	blob \| commitdiff \| raw \| diff to current
2012-10-23	Andrew Reynolds	more major cleanup of quantifiers code, separating...	blob \| commitdiff \| raw \| diff to current
2012-10-23	Andrew Reynolds	more updates to inst gen: fixed partial instantiations...	blob \| commitdiff \| raw \| diff to current
2012-10-16	Andrew Reynolds	more cleanup of quantifiers code	blob \| commitdiff \| raw \| diff to current
2012-10-16	Andrew Reynolds	first draft of new inst gen method (still with bugs...	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-09-25	Morgan Deters	some buggy examples for incrementality, and make bug326...	blob \| commitdiff \| raw \| diff to current
2012-09-22	Morgan Deters	Separate public-facing and internal-facing interfaces...	blob \| commitdiff \| raw \| diff to current
2012-08-31	Andrew Reynolds	merge from fmf-devel branch. more updates to models...	blob \| commitdiff \| raw \| diff to current
2012-07-31	Morgan Deters	Moving some instantiation-related stuff from src/theory...	blob \| commitdiff \| raw \| diff to current
2012-07-27	Andrew Reynolds	merging fmf-devel branch, includes refactored datatype...	blob \| commitdiff \| raw \| diff to current
2012-07-27	François Bobot	Merge quantifiers2-trunk:	blob \| commitdiff \| raw \| diff to current
2012-07-12	Andrew Reynolds	merged fmf-devel branch, includes support for SMT2...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Morgan Deters	Merge from quantifiers2-trunkmerge branch.	blob \| commitdiff \| raw \| diff to current

RSS Atom