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

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

2020-12-15	Andrew Reynolds	Remove bv divide by zero option (#5672)	blob \| commitdiff \| raw
2020-09-22	Mathias Preiner	Add simple BV solver (#5065)	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-03	Gereon Kremer	Added a new rule to simplify (bvugt (bvurem T x) x...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2019-12-09	Andres Noetzli	Make theory rewriters non-static (#3547)	blob \| commitdiff \| raw \| diff to current
2019-05-18	Andres Noetzli	Fix BV ITE rewrite (#3004)	blob \| commitdiff \| raw \| diff to current
2019-04-01	Andres Noetzli	Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-10-20	Aina Niemetz	BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_X...	blob \| commitdiff \| raw \| diff to current
2018-10-17	Aina Niemetz	BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_O...	blob \| commitdiff \| raw \| diff to current
2018-10-16	Aina Niemetz	BV rewrites (mined): Rule 35: ConcatPullUp (BITVECTOR_A...	blob \| commitdiff \| raw \| diff to current
2018-08-08	Andres Noetzli	Require Swig 3 (#2283)	blob \| commitdiff \| raw \| diff to current
2018-08-07	Aina Niemetz	Add rewrite for nested BITVECTOR_ITE that can be merged...	blob \| commitdiff \| raw \| diff to current
2018-08-04	Aina Niemetz	Add rewrite for nested BITVECTOR_ITE with cond_outer...	blob \| commitdiff \| raw \| diff to current
2018-08-04	Aina Niemetz	Add rewrite for BITVECTOR_ITE with const children....	blob \| commitdiff \| raw \| diff to current
2018-08-03	Aina Niemetz	Add rewrite for BITVECTOR_ITE with term_then == term_el...	blob \| commitdiff \| raw \| diff to current
2018-08-02	Aina Niemetz	Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-04-05	Mathias Preiner	Add more general SignExtendUltConst rewriting. (#1385)	blob \| commitdiff \| raw \| diff to current
2017-12-21	Mathias Preiner	Add rewriting rule for ranking benchmarks. (#1448)	blob \| commitdiff \| raw \| diff to current
2017-10-21	Mathias Preiner	Add rewriting rules for Eq/Ult with sign_extend and...	blob \| commitdiff \| raw \| diff to current
2017-09-01	Andres Noetzli	Replace CVC4_THREADLOCAL in interactive_shell (#1065)	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-06-21	Andrew Reynolds	Merge pull request #175 from CVC4/fix_uninit	blob \| commitdiff \| raw \| diff to current
2017-06-15	Clark Barrett	Merge pull request #167 from CVC4/fix_div	blob \| commitdiff \| raw \| diff to current
2017-06-14	Andres Noetzli	Remove UdivSelf rewrite, add UdivZero rewrite	blob \| commitdiff \| raw \| diff to current
2017-03-06	Clark Barrett	Adding support for bool-to-bv	blob \| commitdiff \| raw \| diff to current
2016-11-10	ajreynol	Add option for enabling/disabling lazy extended functio...	blob \| commitdiff \| raw \| diff to current
2016-10-13	ajreynol	Merging bv parts of ajr/bvExt branch, minor additions...	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-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Removing StatisticsRegistry's static functions current...	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-07-28	Tianyi Liang	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2015-07-20	ajreynol	Squashed merge of SygusComp 2015 branch.	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-17	lianah	added command line option for extractArith bv 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-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-23	lianah	Fixed inefficiency in bit-vector rewrite rule.	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-11	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-06-11	lianah	switched bv equality order	blob \| commitdiff \| raw \| diff to current
2014-06-10	lianah	Merging CAV14 paper bit-vector work.	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-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-09	lianah	fixed options::proof() segfault	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-09-18	Morgan Deters	Support for bv2nat/int2bv in parser and BV rewriter.	blob \| commitdiff \| raw \| diff to current
2013-08-26	Kshitij Bansal	Merge branch '1.2.x'	blob \| commitdiff \| raw \| diff to current
2013-07-16	Morgan Deters	Minor bugfixes to model-building	blob \| commitdiff \| raw \| diff to current
2013-05-07	lianah	one more fix for rewrites	blob \| commitdiff \| raw \| diff to current
2013-05-07	lianah	fixed bv rewrite blow-up	blob \| commitdiff \| raw \| diff to current
2013-05-07	Liana Hadarean	fixed bv rewrite rule bug	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-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	updated the author name	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	updated the author name	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-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-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
2012-11-13	Liana Hadarean	fixed failed bv regressions by refactoring out some...	blob \| commitdiff \| raw \| diff to current
2012-11-13	Liana Hadarean	added support for division by zero for bit-vector divis...	blob \| commitdiff \| raw \| diff to current
2012-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-10-09	Liana Hadarean	fixed bv rewriter to evaluate bvurem over constants	blob \| commitdiff \| raw \| diff to current
2012-06-13	Clark Barrett	Fixes more problems in bv rewrites	blob \| commitdiff \| raw \| diff to current
2012-06-12	Clark Barrett	Changed bitvector theory rewriter so that equalities...	blob \| commitdiff \| raw \| diff to current
2012-06-11	Clark Barrett	OK, now the rewrite issues are fixed	blob \| commitdiff \| raw \| diff to current
2012-06-11	Clark Barrett	Fix for array bug with decision heuristic	blob \| commitdiff \| raw \| diff to current
2012-06-10	Clark Barrett	Added a very fruitful assertion to the rewriter: checks...	blob \| commitdiff \| raw \| diff to current
2012-05-30	Clark Barrett	Added BitwiseEq bitvector rewrite	blob \| commitdiff \| raw \| diff to current
2012-05-29	Clark Barrett	Enabled SolveEq bv rewrite	blob \| commitdiff \| raw \| diff to current
2012-05-28	Clark Barrett	Added some BV rewrites, fixed bugs in array theory...	blob \| commitdiff \| raw \| diff to current
2012-04-04	Liana Hadarean	* added propagation as lemmas to TheoryBV:	blob \| commitdiff \| raw \| diff to current
2012-03-29	Tim King	Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is...	blob \| commitdiff \| raw \| diff to current
2012-03-22	Liana Hadarean	Merged updated version of the bitvector theory:	blob \| commitdiff \| raw \| diff to current
2012-02-25	Liana Hadarean	Refactored CnfStream to work with the bv theory Bitblaster:	blob \| commitdiff \| raw \| diff to current
2012-02-20	Morgan Deters	portfolio merge	blob \| commitdiff \| raw \| diff to current
2011-09-02	Morgan Deters	Merge from my post-smtcomp branch. Includes:	blob \| commitdiff \| raw \| diff to current
2011-03-22	Dejan Jovanović	updating debug output usage to eliviate impact of bug 252	blob \| commitdiff \| raw \| diff to current
2011-03-20	Dejan Jovanović	commit for the version of bitvectors that passes all...	blob \| commitdiff \| raw \| diff to current
2011-02-26	Morgan Deters	Commit to fix bug 241 (improper "using namespace std...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom