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

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

2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw
2020-02-03	Andrew Reynolds	Example inference utility (#3670)	blob \| commitdiff \| raw \| diff to current
2019-04-18	Andrew Reynolds	Fail fast strategy for propagating instances (#2939)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-11-30	Andrew Reynolds	Remove remaining references to QuantArith (#1408)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Andrew Reynolds	Make QEffort an enum (#1366)	blob \| commitdiff \| raw \| diff to current
2017-11-02	Andrew Reynolds	(Move-only) Split quant util (#1306)	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andrew Reynolds	Document quant arith (#1271)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge datatype shared selectors/sygus comp 2017 branch...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-04-04	Clark Barrett	Merge pull request #141 from 4tXJ7f/remove_def	blob \| commitdiff \| raw \| diff to current
2017-04-03	Andrew Reynolds	Merge pull request #142 from timothy-king/nlAlgMerge	blob \| commitdiff \| raw \| diff to current
2017-04-03	Tim King	Adding a model based axiom instantiation scheme for...	blob \| commitdiff \| raw \| diff to current
2017-03-29	ajreynol	Add quantifiers options related to model and master...	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2016-12-06	ajreynol	Improve bounds for global heap in sep, refactor preproc...	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-09-15	ajreynol	Refactor setIncomplete in quantifiers.	blob \| commitdiff \| raw \| diff to current
2016-09-14	ajreynol	Lemma cache in theory sep. Minor optimization for sets...	blob \| commitdiff \| raw \| diff to current
2016-09-13	ajreynol	Minor changes to sep logic, epr, quantifier splitting.	blob \| commitdiff \| raw \| diff to current
2016-08-26	ajreynol	Basic support for EPR+CBQI. Minor cleanup.	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-06-20	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-17	ajreynol	Support for separation logic. Enable cbqi by default...	blob \| commitdiff \| raw \| diff to current
2016-04-28	ajreynol	More work on inst propagate. Optimization for qcf...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	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
2016-04-01	ajreynol	Improvements to equality inference module: add missing...	blob \| commitdiff \| raw \| diff to current
2016-03-30	ajreynol	Updates to E-matching to avoid entailed instantiations...	blob \| commitdiff \| raw \| diff to current
2016-03-28	ajreynol	Minor cleanup from last commit (quant util, equality...	blob \| commitdiff \| raw \| diff to current
2016-03-28	ajreynol	Implement equality inference module for arithmetic...	blob \| commitdiff \| raw \| diff to current
2016-02-15	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-02-11	ajreynol	More aggressive conditional rewriting for quantified...	blob \| commitdiff \| raw \| diff to current
2015-11-25	ajreynol	Infrastructure for partially single invocation properti...	blob \| commitdiff \| raw \| diff to current
2015-11-10	ajreynol	Fix infinite loop in datatype enumerator. Minor fixes...	blob \| commitdiff \| raw \| diff to current
2015-11-05	Tim King	Merging the google branch back into master.	blob \| commitdiff \| raw \| diff to current
2015-10-31	ajreynol	Improvements to handling of mixed Int/Real quantifiers.	blob \| commitdiff \| raw \| diff to current
2015-10-26	ajreynol	Promote InstStrategyCbqi to quantifier module. Cleanup...	blob \| commitdiff \| raw \| diff to current
2015-09-02	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2015-08-24	ajreynol	Improvements to vts in cbqi, bug fix vts for non-atomic...	blob \| commitdiff \| raw \| diff to current
2015-08-21	ajreynol	Fix disequality bounds in cbqi, record literals for...	blob \| commitdiff \| raw \| diff to current
2015-06-16	ajreynol	Avoid completion for large finite types. Fix bug for...	blob \| commitdiff \| raw \| diff to current
2015-03-04	ajreynol	More work on arithmetic single invocation synthesis...	blob \| commitdiff \| raw \| diff to current
2015-02-26	ajreynol	Robust strategy for single invocation LIA synthesis...	blob \| commitdiff \| raw \| diff to current
2015-02-06	ajreynol	Handle missing cases for single inv solution reconstruc...	blob \| commitdiff \| raw \| diff to current
2015-02-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2015-02-04	ajreynol	Start work on simplifying single inv solutions. Minor.	blob \| commitdiff \| raw \| diff to current
2015-02-02	ajreynol	Single invocation module for counterexample guided...	blob \| commitdiff \| raw \| diff to current
2015-01-29	ajreynol	Restrict LtePartialInst instantiations based on E-match...	blob \| commitdiff \| raw \| diff to current
2015-01-24	ajreynol	Variable patterns only look at eligible terms. Minor...	blob \| commitdiff \| raw \| diff to current
2015-01-22	ajreynol	Add option --lte-partial-inst. Remove inst-closure.	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-16	ajreynol	Add term db mode. Minor changes to quantifiers rewrite...	blob \| commitdiff \| raw \| diff to current
2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw \| diff to current
2014-07-01	Morgan Deters	Update copyrights.	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-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-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-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-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-19	Morgan Deters	Merge branch '1.2.x'	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-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-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-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
next

RSS Atom