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

[cvc5.git] / src / theory / quantifiers / term_database.h

2014-06-16	ajreynol	More proof support for CASC : include skolemization	blob \| commitdiff \| raw
2014-06-03	ajreynol	Support E-matching/QCF for Set operators.	blob \| commitdiff \| raw \| diff to current
2014-05-23	Andrew Reynolds	Fix bug in E-matching Real/Int terms.	blob \| commitdiff \| raw \| diff to current
2014-05-02	Andrew Reynolds	Add option --dt-stc-ind for strengthening skolemization...	blob \| commitdiff \| raw \| diff to current
2014-05-01	Kshitij Bansal	Merge remote-tracking branch 'upstream/master' into...	blob \| commitdiff \| raw \| diff to current
2014-04-30	Tim King	T-entailment work, and QCF (quant conflict find) work...	blob \| commitdiff \| raw \| diff to current
2014-04-01	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-26	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-21	Kshitij Bansal	Merge pull request #22 from kbansal/sets-model	blob \| commitdiff \| raw \| diff to current
2014-03-12	Andrew Reynolds	Work on array pf signature, add working example. Add...	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	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-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-28	Andrew Reynolds	More optimizations of quantifier instantiation data...	blob \| commitdiff \| raw \| diff to current
2013-11-11	Morgan Deters	Flatten libcvc4 build structure; remove some #include...	blob \| commitdiff \| raw \| diff to current
2013-11-07	Morgan Deters	Flatten libcvc4 build structure; remove some #include...	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-06-25	Morgan Deters	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-06-25	Andrew Reynolds	Refactoring of model engine to separate individual...	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-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-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-04-01	Morgan Deters	Merging some cleanup work:	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-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-17	Kshitij Bansal	Merge branch '1.0.x'	blob \| commitdiff \| raw \| diff to current
2013-02-17	Kshitij Bansal	Merge pull request #6 from kbansal/decNewoptions	blob \| commitdiff \| raw \| diff to current
2013-02-16	Morgan Deters	Some cleanup and copyright updating	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
2012-11-14	Andrew Reynolds	replaced all static member data from rewrite rule trigg...	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-02	Andrew Reynolds	more minor updates to inst gen and representative selec...	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-17	Andrew Reynolds	first working version of new inst-gen-style quantifier...	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-10-10	Andrew Reynolds	cleanup up some static data members in the quantifiers...	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	Morgan Deters	Minor cleanup after today's commits:	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

RSS Atom