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

[cvc5.git] / src / theory / datatypes / theory_datatypes.cpp

2014-12-27	Dejan Jovanovic	Adding an option to the equality engine constructor...	blob \| commitdiff \| raw
2014-12-22	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-22	ajreynol	Do not collapse wrongly applied selectors for non-well...	blob \| commitdiff \| raw \| diff to current
2014-12-11	ajreynol	Option to enable/disable cyclicity check in datatypes.	blob \| commitdiff \| raw \| diff to current
2014-12-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-06	ajreynol	Fix dt.size care graph.	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-18	ajreynol	Add local theory extensions instantiation strategy...	blob \| commitdiff \| raw \| diff to current
2014-11-17	Morgan Deters	New, uniform checkTime statistic for all theories ...	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-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-09	ajreynol	Fix dt shared terms issue, reenable regression.	blob \| commitdiff \| raw \| diff to current
2014-11-08	ajreynol	Fix bug with incremental+datatypes. Minor cleanup...	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-07	ajreynol	Properly distinguish which EQC to assign values in...	blob \| commitdiff \| raw \| diff to current
2014-11-06	ajreynol	Minor fix for getInstCons	blob \| commitdiff \| raw \| diff to current
2014-11-06	ajreynol	Reenable regression. Add (for now, disabled) changes...	blob \| commitdiff \| raw \| diff to current
2014-11-05	ajreynol	Fix model bug in --mbqi=fmc. Minor cleanup in datatypes.	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	ajreynol	More work on datatypes theory combination: fix bug...	blob \| commitdiff \| raw \| diff to current
2014-11-01	ajreynol	Simplify which lemmas to communicate in dt.	blob \| commitdiff \| raw \| diff to current
2014-11-01	ajreynol	Fix bug 592: introduce skolem for dt instantiate lemma...	blob \| commitdiff \| raw \| diff to current
2014-11-01	ajreynol	Fix some mistakes in datatypes theory combination,...	blob \| commitdiff \| raw \| diff to current
2014-10-31	ajreynol	Do not allow duplication of function definitions. ...	blob \| commitdiff \| raw \| diff to current
2014-10-20	ajreynol	Minor cleanup in datatypes.	blob \| commitdiff \| raw \| diff to current
2014-10-18	ajreynol	Add dt lemma: zero size implies nullary constructor.	blob \| commitdiff \| raw \| diff to current
2014-10-18	ajreynol	Fix for bounded integers when incremental, fixes bug...	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-16	ajreynol	Use n-ary splits instead of binary splits in theory...	blob \| commitdiff \| raw \| diff to current
2014-10-16	ajreynol	Add dt.size to datatypes theory. Add option for fairne...	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-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-09-30	Morgan Deters	Merge branch '1.4.x'	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	Partial support for codatatype models.	blob \| commitdiff \| raw \| diff to current
2014-09-23	ajreynol	Do not throw error when codatatype is not well-founded...	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-03	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2014-09-03	Kshitij Bansal	check() optimization	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-08-27	ajreynol	Fix assertion in rep_set.cpp, avoid full check in datat...	blob \| commitdiff \| raw \| diff to current
2014-08-26	ajreynol	Bug fixes for --purify-triggers, --dt-force-assignment.	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-07-19	ajreynol	Minor fix for explanations for co-datatypes. Bug fix...	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-05-02	ajreynol	More minor optimizations for datatypes.	blob \| commitdiff \| raw \| diff to current
2014-05-01	ajreynol	Minor optimizations to datatypes, revert to checkClash...	blob \| commitdiff \| raw \| diff to current
2014-04-29	ajreynol	Significantly improve performance for producing datatyp...	blob \| commitdiff \| raw \| diff to current
2014-04-28	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-04-28	Kshitij Bansal	Merge pull request #25 from kbansal/sets	blob \| commitdiff \| raw \| diff to current
2014-04-28	Andrew Reynolds	Preparation for models for co-inductive datatypes....	blob \| commitdiff \| raw \| diff to current
2014-04-28	ajreynol	Optimizations for datatypes: check for clashes modulo...	blob \| commitdiff \| raw \| diff to current
2014-04-28	Kshitij Bansal	Merge remote-tracking branch 'upstream/master' into...	blob \| commitdiff \| raw \| diff to current
2014-04-24	ajreynol	Avoid assigning constructor terms to 1-constructor...	blob \| commitdiff \| raw \| diff to current
2014-04-24	Andrew Reynolds	Compute care graph for datatypes. Preliminary results...	blob \| commitdiff \| raw \| diff to current
2014-04-22	Andrew Reynolds	Minor fix to avoid rewriting datatype equalities into...	blob \| commitdiff \| raw \| diff to current
2014-04-17	Kshitij Bansal	simplify mkSkolem naming system: don't use $$	blob \| commitdiff \| raw \| diff to current
2014-04-17	Andrew Reynolds	Minor refactoring and optimizing.	blob \| commitdiff \| raw \| diff to current
2014-04-14	Andrew Reynolds	Fix bug in mbqi=fmc handling theory symbols. Fix mbqi...	blob \| commitdiff \| raw \| diff to current
2014-04-14	Andrew Reynolds	Add initial support for co-datatypes.	blob \| commitdiff \| raw \| diff to current
2014-04-10	Andrew Reynolds	Expand definitions in theory datatypes, now has the...	blob \| commitdiff \| raw \| diff to current
2014-04-10	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-04-10	Andrew Reynolds	Add support for cardinality constraints logic UFC....	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-02-04	Andrew Reynolds	Do not use transitive closure module for cycle detectio...	blob \| commitdiff \| raw \| diff to current
2014-01-27	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-22	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-01-22	Morgan Deters	Delay QuantifiersEngine and UF strong solver initializa...	blob \| commitdiff \| raw \| diff to current
2013-12-03	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-11-27	Morgan Deters	General pre-release cleanup commit	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-11	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-10-10	Andrew Reynolds	Minor bug fix to datatypes.	blob \| commitdiff \| raw \| diff to current
2013-10-10	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2013-10-09	Andrew Reynolds	More improvements to datatypes, eager selector collapsi...	blob \| commitdiff \| raw \| diff to current
2013-10-08	Andrew Reynolds	Optimizations for datatypes theory. There seems to...	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
next

RSS Atom