git.libre-soc.org Git - cvc5.git/history

[cvc5.git] / src / theory / rewriter.cpp

2020-11-20	Aina Niemetz	Fix compiler warnings. (#5493)	blob \| commitdiff \| raw
2020-11-16	Gereon Kremer	Improve accuracy of resource limitation (#4763)	blob \| commitdiff \| raw \| diff to current
2020-10-21	Andrew Reynolds	(proof-new) Fixes for proofs in rewriter (#5307)	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-02	Andrew Reynolds	(proof-new) Updates to builtin proof checker (#4962)	blob \| commitdiff \| raw \| diff to current
2020-07-15	Andres Noetzli	Use TypeNode in UninterpretedConstant (#4748)	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andrew Reynolds	(proof-new) Skeleton proof support in the Rewriter...	blob \| commitdiff \| raw \| diff to current
2020-07-07	Andrew Reynolds	Transfer ownership of internal Options from NodeManager...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	blob \| commitdiff \| raw \| diff to current
2020-04-02	Andres Noetzli	Initialize theory rewriters in theories (#4197)	blob \| commitdiff \| raw \| diff to current
2020-03-11	Andres Noetzli	Introduce tables in the rewriter (#3742)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	blob \| commitdiff \| raw \| diff to current
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	blob \| commitdiff \| raw \| diff to current
2019-12-15	Andrew Reynolds	Simple optimizations for the core rewriter (#3569)	blob \| commitdiff \| raw \| diff to current
2019-12-09	Andres Noetzli	Make theory rewriters non-static (#3547)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-08-01	Mathias Preiner	Fix memory leak in rewriter (debug mode). (#3141)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-08-08	Andres Noetzli	Require Swig 3 (#2283)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-01-27	Tim King	Removing structurally dead code. (#1540)	blob \| commitdiff \| raw \| diff to current
2017-08-31	Andres Noetzli	Use thread_local instead of compiler extensions (#210)	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Moving from the gnu extensions for hash maps to the...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2017-01-18	Andrew Reynolds	Merge pull request #128 from 4tXJ7f/fix_lfsc_perf	blob \| commitdiff \| raw \| diff to current
2017-01-14	Clark Barrett	Merge pull request #130 from chadbrewbaker/master	blob \| commitdiff \| raw \| diff to current
2017-01-11	Clark Barrett	Merge pull request #129 from timothy-king/regression...	blob \| commitdiff \| raw \| diff to current
2017-01-11	Tim King	Adding regression test scrubbing.	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-27	Liana Hadarean	Merged bit-vector and uf proof branch.	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Adding a new Listener utility class. Changing the Resou...	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-05-28	Liana Hadarean	added options for controlling resource step-count for...	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	Liana Hadarean	Resource-limiting work.	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
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-12-03	lianah	fixed rewriter bug where postRewrite was not caching...	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-10-11	Morgan Deters	Standardizing copyright notice. Touches ALL source...	blob \| commitdiff \| raw \| diff to current
2012-10-06	Morgan Deters	* Fix some regressions' expected outputs.	blob \| commitdiff \| raw \| diff to current
2012-07-31	Morgan Deters	fixes for portfolio	blob \| commitdiff \| raw \| diff to current
2012-06-16	Dejan Jovanović	changing theoryOf in shared mode with arrays to move...	blob \| commitdiff \| raw \| diff to current
2012-06-14	Dejan Jovanović	* removing rewriteEquality from the rewriter	blob \| commitdiff \| raw \| diff to current
2012-06-13	Clark Barrett	Fixes lots of problems in bv rewrite rules and adds...	blob \| commitdiff \| raw \| diff to current
2012-06-12	Dejan Jovanović	bufixes and the bugs	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-28	Clark Barrett	Added some BV rewrites, fixed bugs in array theory...	blob \| commitdiff \| raw \| diff to current
2012-03-28	Dejan Jovanović	adding an extra cache check in the rewriter, speeds...	blob \| commitdiff \| raw \| diff to current
2011-10-17	Dejan Jovanović	Sharing work	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-07-12	Morgan Deters	fix bug 272, array unsoundness, and some array cleanup	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
2011-01-05	Dejan Jovanović	Commit for the theory engine and rewriter changes....	blob \| commitdiff \| raw \| diff to current

RSS Atom