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

[cvc5.git] / src / theory / bv / bv_subtheory_inequality.cpp

2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw
2014-07-01	Morgan Deters	Update copyrights.	blob \| commitdiff \| raw
2014-06-14	lianah	fixed merge	blob \| commitdiff \| raw \| diff to current
2014-06-14	Liana Hadarean	added bv inequality lemmas	blob \| commitdiff \| raw \| diff to current
2014-06-14	Liana Hadarean	added bv inequality lemmas	blob \| commitdiff \| raw \| diff to current
2014-06-12	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-06-12	lianah	fixing bv inequality solver explanation bug	blob \| commitdiff \| raw \| diff to current
2013-12-05	Morgan Deters	Update copyrights, add missing file-level documentation...	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-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-07-22	Andrew Reynolds	Bug fix for --fmf-fmc for non-uninterpreted sort quanti...	blob \| commitdiff \| raw \| diff to current
2013-07-16	Liana Hadarean	fixed bug520	blob \| commitdiff \| raw \| diff to current
2013-04-18	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-04-11	lianah	fixed getModelValue to only query the value of leaves...	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-03-29	Dejan Jovanović	Merge branch 'master' of github.com:CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	fixed inequality checkDisequalities inefficiency	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	fixed some model stuff	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	fixed model generation bug; commented out attempt...	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	inequality solver now only splits on disequalities...	blob \| commitdiff \| raw \| diff to current
2013-03-27	lianah	added model generation for bv subtheories and bv-inequa...	blob \| commitdiff \| raw \| diff to current
2013-03-26	lianah	cleaned up the bv subtheory interface; added check...	blob \| commitdiff \| raw \| diff to current
2013-03-25	lianah	getEqualityStatus now also queries the inequality solver	blob \| commitdiff \| raw \| diff to current
2013-03-25	Liana Hadarean	added support for disequalities in the inequality solver	blob \| commitdiff \| raw \| diff to current
2013-03-23	lianah	non-incremental inequality solver seems to be bug-free...	blob \| commitdiff \| raw \| diff to current
2013-03-22	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	Merge branch 'master' into bv-core	blob \| commitdiff \| raw \| diff to current
2013-03-21	lianah	generalized bv inequality reasoning to handle both...	blob \| commitdiff \| raw \| diff to current
2013-03-20	Liana Hadarean	merged master with dejan's constant evaluating equality...	blob \| commitdiff \| raw \| diff to current
2013-03-20	Liana Hadarean	inequality reasoning works on small examples added...	blob \| commitdiff \| raw \| diff to current
2013-03-19	Liana Hadarean	implementing more inequality graph stuff; work in progr...	blob \| commitdiff \| raw \| diff to current
2013-03-18	lianah	more work on inequality reasoning for bv	blob \| commitdiff \| raw \| diff to current
2013-03-16	lianah	started work on the inequality bv subtheory	blob \| commitdiff \| raw \| diff to current

RSS Atom