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

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

2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-10-02	Morgan Deters	Merge branch '1.4.x'.	blob \| commitdiff \| raw
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-09-27	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-09-26	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-09-17	Kshitij Bansal	Merge branch '1.4.x' while ignoring commit 8d5eb49.	blob \| commitdiff \| raw
2014-09-17	Kshitij Bansal	Merge branch '1.4.x'	blob \| commitdiff \| raw
2014-09-03	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw
2014-09-03	Kshitij Bansal	check() optimization	blob \| commitdiff \| raw
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-19	lianah	Making getEqualityStatus more powerful for bit-vector...	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-06-26	Morgan Deters	Merge tag 'smtcomp2014-resubmission'	blob \| commitdiff \| raw \| diff to current
2014-06-22	Morgan Deters	Merge tag 'smtcomp2014-application'	blob \| commitdiff \| raw \| diff to current
2014-06-19	lianah	fixed merge conflict	blob \| commitdiff \| raw \| diff to current
2014-06-19	lianah	added model generation to eager bit-blasting and turned...	blob \| commitdiff \| raw \| diff to current
2014-06-16	lianah	fixed bv bug due to applying equisatisfiable transforma...	blob \| commitdiff \| raw \| diff to current
2014-06-15	lianah	Evil bitvector preprocessing pass for simplifying power...	blob \| commitdiff \| raw \| diff to current
2014-06-15	lianah	bv static learning and rewrites for power of 2 terms	blob \| commitdiff \| raw \| diff to current
2014-06-14	lianah	more bv rewrites	blob \| commitdiff \| raw \| diff to current
2014-06-14	lianah	fixed merge	blob \| commitdiff \| raw \| diff to current
2014-06-14	lianah	added bv inequality rewrite	blob \| commitdiff \| raw \| diff to current
2014-06-11	Kshitij Bansal	Merge pull request #31 from kbansal/sets	blob \| commitdiff \| raw \| diff to current
2014-06-11	lianah	fixing bv ackermanization cache bug	blob \| commitdiff \| raw \| diff to current
2014-06-10	lianah	Merging CAV14 paper bit-vector work.	blob \| commitdiff \| raw \| diff to current
2014-04-06	Tim King	Merge pull request #21 from pcc/ite-fix	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-21	Kshitij Bansal	Merge pull request #22 from kbansal/sets-model	blob \| commitdiff \| raw \| diff to current
2014-03-19	Martin Brain	Refactor the theory specific parts of definition expans...	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-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-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-11-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	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-07	Liana Hadarean	merged golden	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 seg fault when bv equality is turned off	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-05-29	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-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-14	lianah	added some extra options to the bit-vector theory	blob \| commitdiff \| raw \| diff to current
2013-05-03	lianah	changed the shifting bit-blasting to potentially be...	blob \| commitdiff \| raw \| diff to current
2013-05-03	Tim King	Merging branch 'soiquickexplain'.	blob \| commitdiff \| raw \| diff to current
2013-05-03	Tim King	Merge branch 'fcexplanations'	blob \| commitdiff \| raw \| diff to current
2013-05-02	lianah	merged master	blob \| commitdiff \| raw \| diff to current
2013-05-02	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-05-01	lianah	removed tracing code causing slowdown; cleaned up some...	blob \| commitdiff \| raw \| diff to current
2013-05-01	lianah	added back BitwiseEq rule	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	fixed merge conflicts	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	merged cvc4 master	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	added several rewrite rules (BitwiseSlicing, Ule/SleEli...	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	added bvule, bvsle operator elimination rulesl; added...	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	added some bv rewrite rules	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	finished implementing bv to bool lifting and added...	blob \| commitdiff \| raw \| diff to current
2013-04-30	lianah	added several rewrite rules (BitwiseSlicing, Ule/SleEli...	blob \| commitdiff \| raw \| diff to current
2013-04-29	Kshitij Bansal	Merge pull request #9 from kbansal/master	blob \| commitdiff \| raw \| diff to current
2013-04-26	Kshitij Bansal	Merge experimental decisionweight branch	blob \| commitdiff \| raw \| diff to current
2013-04-25	lianah	added bvule, bvsle operator elimination rulesl; added...	blob \| commitdiff \| raw \| diff to current
2013-04-21	lianah	added some bv rewrite rules	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-12	lianah	finished implementing bv to bool lifting and added...	blob \| commitdiff \| raw \| diff to current
2013-04-03	Dejan Jovanović	* changing the bitblast-eager to bitblast on pre-register	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	reverted the core solver to do static slicing, added...	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 model generation bug; commented out attempt...	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	Dejan Jovanović	getModelValue implementation in bitvectors	blob \| commitdiff \| raw \| diff to current
2013-03-26	lianah	fixed inequality bugs due to improper explanation	blob \| commitdiff \| raw \| diff to current
next

RSS Atom