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

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

2018-05-30	Andrew Reynolds	Fixes for quantifiers + incremental (#2009)	blob \| commitdiff \| raw
2018-04-26	Andrew Reynolds	Fix subgoal generation context (#1816)	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Andrew Reynolds	Make QEffort an enum (#1366)	blob \| commitdiff \| raw \| diff to current
2017-11-01	Andrew Reynolds	(Refactor) Split term util (#1303)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-04-11	ajreynol	Bug fix in conjecture generation for --quant-ind.	blob \| commitdiff \| raw \| diff to current
2016-10-13	Tim King	Revert "Merge branch 'origin' of https://github.com...	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-10-01	Tim King	Merge pull request #93 from timothy-king/clang-format	blob \| commitdiff \| raw \| diff to current
2016-09-29	ajreynol	Address some coverity warnings, add another stat.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-05-05	ajreynol	Compute term indices lazily in TermDb. Optimization...	blob \| commitdiff \| raw \| diff to current
2016-05-02	ajreynol	Clean up issues related to compiled scc in LFSC. Refact...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-13	ajreynol	Handle parametric datatypes with --quant-ind. Minor...	blob \| commitdiff \| raw \| diff to current
2016-04-12	ajreynol	Optimizations for QCF to check relevant domain of varia...	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-09	ajreynol	Minor refactoring of entailment tests and quantifiers...	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-09-25	ajreynol	Clear term caches for quantifiers + incremental, fixes...	blob \| commitdiff \| raw \| diff to current
2015-09-15	ajreynol	Fix bug related to quantifiers + incremental, thanks...	blob \| commitdiff \| raw \| diff to current
2015-09-11	ajreynol	Minor cleanup related to codatatypes.	blob \| commitdiff \| raw \| diff to current
2015-07-28	Tianyi Liang	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2015-07-02	ajreynol	On-demand upper bound lemmas for deltas in quantified...	blob \| commitdiff \| raw \| diff to current
2015-06-29	ajreynol	Module to infer alpha equivalence of quantified formula...	blob \| commitdiff \| raw \| diff to current
2015-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-04-23	Clark Barrett	Merge branch 'master' into google	blob \| commitdiff \| raw \| diff to current
2015-04-23	Clark Barrett	A few more minor updates to match google repository...	blob \| commitdiff \| raw \| diff to current
2015-04-21	Clark Barrett	Fix file permissions	blob \| commitdiff \| raw \| diff to current
2015-04-17	Kshitij Bansal	Merge pull request #72 from kbansal/decision-requirephase	blob \| commitdiff \| raw \| diff to current
2015-04-09	ajreynol	Fix unsat-core issues related to rewrite rules, quantif...	blob \| commitdiff \| raw \| diff to current
2015-04-08	ajreynol	Make fun-def quantifiers carry the function app they...	blob \| commitdiff \| raw \| diff to current
2015-01-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-27	Dejan Jovanovic	Adding an option to the equality engine constructor...	blob \| commitdiff \| raw \| diff to current
2014-12-03	Kshitij Bansal	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-28	ajreynol	Synchronize conjecture generation with E-matching....	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-13	Morgan Deters	Merge pull request #69 from mdeters/bug594	blob \| commitdiff \| raw \| diff to current
2014-11-13	ajreynol	More preparation for filtering relevant terms in TermDb.	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-28	ajreynol	Improve stats in conjecture generator, minor cleanup.	blob \| commitdiff \| raw \| diff to current
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	ajreynol	Initial draft of CEGQI.	blob \| commitdiff \| raw \| diff to current
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-02	Morgan Deters	Merge branch '1.4.x'.	blob \| commitdiff \| raw \| diff to current
2014-10-01	ajreynol	Option for more aggressive merging in UEE.	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-29	ajreynol	Add option for aggressive model filtering in conjecture...	blob \| commitdiff \| raw \| diff to current
2014-09-27	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-26	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-24	ajreynol	Fix infinite loop in datatypes enumerator. Minor work...	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x' while ignoring commit 8d5eb49.	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-17	ajreynol	Refactor entailment filtering for conjecture generator...	blob \| commitdiff \| raw \| diff to current
2014-09-17	ajreynol	More refactoring of conjecture generation. Term genera...	blob \| commitdiff \| raw \| diff to current
2014-09-16	ajreynol	Bug fix variable triggers with --inst-max-level : use...	blob \| commitdiff \| raw \| diff to current
2014-09-16	ajreynol	Refactoring of conjecture generator. Determine subgoal...	blob \| commitdiff \| raw \| diff to current
2014-09-08	ajreynol	Accept user-provided triggers with variable terms....	blob \| commitdiff \| raw \| diff to current
2014-09-03	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2014-09-03	ajreynol	Implement and enable --dt-var-exp-quant, cleanup trace...	blob \| commitdiff \| raw \| diff to current
2014-09-03	ajreynol	Work on conjecture generator : do not generalize subter...	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-19	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-18	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-01	ajreynol	Minor cleanup from previous commit. Better organizatio...	blob \| commitdiff \| raw \| diff to current
2014-07-31	ajreynol	New module for generating candidate equality conjecture...	blob \| commitdiff \| raw \| diff to current

RSS Atom