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

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

2015-07-02	ajreynol	On-demand upper bound lemmas for deltas in quantified...	blob \| commitdiff \| raw
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