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

[cvc5.git] / src / theory / strings / theory_strings_rewriter.h

2020-02-22	Andrew Reynolds	Move cardinality inference scheme to base solver in...	blob \| commitdiff \| raw
2020-02-16	Andres Noetzli	Activate reverse variant of F-Split inference (#3745)	blob \| commitdiff \| raw \| diff to current
2020-02-11	Andres Noetzli	Refactor `CoreSolver::processSimpleNEq()` (#3736)	blob \| commitdiff \| raw \| diff to current
2019-12-23	Andrew Reynolds	Initial support for string reverse (#3581)	blob \| commitdiff \| raw \| diff to current
2019-12-09	Andres Noetzli	Make theory rewriters non-static (#3547)	blob \| commitdiff \| raw \| diff to current
2019-07-24	Andrew Reynolds	Move string util functions (#3115)	blob \| commitdiff \| raw \| diff to current
2019-07-16	Andrew Reynolds	Add support for str.tolower and str.toupper (#3092)	blob \| commitdiff \| raw \| diff to current
2019-06-01	Andrew Reynolds	Fix rewriter for regular expression consume (#3029)	blob \| commitdiff \| raw \| diff to current
2019-04-24	Mathias Preiner	Do not use __ prefix for header guards. (#2974)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2019-03-23	Andres Noetzli	Strip non-matching beginning from indexof operator...	blob \| commitdiff \| raw \| diff to current
2019-01-23	Andres Noetzli	Strings: Strengthen multiset reasoning (#2817)	blob \| commitdiff \| raw \| diff to current
2019-01-18	Andres Noetzli	Strings: Introduce checkEntailContains() (#2809)	blob \| commitdiff \| raw \| diff to current
2018-12-15	Andres Noetzli	Revert "Move ss-combine rewrite to extended rewriter...	blob \| commitdiff \| raw \| diff to current
2018-11-22	Andres Noetzli	Move ss-combine rewrite to extended rewriter (#2703)	blob \| commitdiff \| raw \| diff to current
2018-11-21	Andrew Reynolds	Support string replace all (#2704)	blob \| commitdiff \| raw \| diff to current
2018-10-19	Andres Noetzli	Add helper to detect length one string terms (#2654)	blob \| commitdiff \| raw \| diff to current
2018-10-18	Andrew Reynolds	Constant length regular expression elimination (#2646)	blob \| commitdiff \| raw \| diff to current
2018-10-15	Andres Noetzli	Add more (str.replace x y z) rewrites (#2628)	blob \| commitdiff \| raw \| diff to current
2018-10-04	Andrew Reynolds	Infrastructure for string length entailments via approx...	blob \| commitdiff \| raw \| diff to current
2018-09-30	Andrew Reynolds	Add rewrite for solving stoi (#2532)	blob \| commitdiff \| raw \| diff to current
2018-09-25	Andrew Reynolds	Refactor strings equality rewriting (#2513)	blob \| commitdiff \| raw \| diff to current
2018-09-24	Andres Noetzli	Unify rewrites related to (str.contains x y) --> (...	blob \| commitdiff \| raw \| diff to current
2018-08-09	Andrew Reynolds	Fix char overflow issues in regular expression solver...	blob \| commitdiff \| raw \| diff to current
2018-07-25	Andrew Reynolds	Move reg exp rewrites from prerewrite to postrewrite...	blob \| commitdiff \| raw \| diff to current
2018-07-05	Andres Noetzli	sygusComp2018: Improve string rewriter (#2141)	blob \| commitdiff \| raw \| diff to current
2018-07-04	Andrew Reynolds	More cleanup in strings (#2138)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-06-13	Andrew Reynolds	Fix simple regexp consume (#2066)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Andrew Reynolds	Support for str.<= and str.< (#1882)	blob \| commitdiff \| raw \| diff to current
2018-05-07	Andrew Reynolds	Add support for str.code (#1821)	blob \| commitdiff \| raw \| diff to current
2018-03-27	Andres Noetzli	Better normalization of string concatenation (#1719)	blob \| commitdiff \| raw \| diff to current
2018-03-26	Andres Noetzli	Add reasoning for inequalities in str rewriter (#1713)	blob \| commitdiff \| raw \| diff to current
2018-03-26	Andres Noetzli	Rewrites for substr of strings of length one (#1712)	blob \| commitdiff \| raw \| diff to current
2018-03-21	Andrew Reynolds	More rewrites for indexof (#1648)	blob \| commitdiff \| raw \| diff to current
2018-03-06	Andrew Reynolds	Update semantics for string indexof and replace (#1630)	blob \| commitdiff \| raw \| diff to current
2018-02-22	Andrew Reynolds	Minor improvements to string rewriter (#1572)	blob \| commitdiff \| raw \| diff to current
2018-01-02	Andrew Reynolds	Improve rewriter for string equality (#1427)	blob \| commitdiff \| raw \| diff to current
2017-12-02	Andrew Reynolds	Improve rewriter for string replace (#1416)	blob \| commitdiff \| raw \| diff to current
2017-11-28	Andrew Reynolds	Improve rewrite for string substr (#1337)	blob \| commitdiff \| raw \| diff to current
2017-11-06	Andrew Reynolds	Improve rewriting for string contains part 2 (#1300)	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andrew Reynolds	Improve strings rewriter for contains (#1207)	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-07-26	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-26	ajreynol	Minor improvements to strings related to constant split...	blob \| commitdiff \| raw \| diff to current
2016-07-20	ajreynol	Infer conflicts in strings based on abstracting equalit...	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
2015-10-08	ajreynol	Minor improvements to strings. Refactor rewriter. Enabl...	blob \| commitdiff \| raw \| diff to current
2015-10-06	ajreynol	More improvements to strings rewriter for regexps,...	blob \| commitdiff \| raw \| diff to current
2015-10-02	ajreynol	Improvements to rewriter for regexp, contains, indexof...	blob \| commitdiff \| raw \| diff to current
2015-01-07	Tianyi Liang	added initial AX rules;	blob \| commitdiff \| raw \| diff to current
2015-01-07	Tianyi Liang	added initial AX rules;	blob \| commitdiff \| raw \| diff to current
2014-12-03	Kshitij Bansal	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-03	Tianyi Liang	disable inter cache	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	add intersection rewriting	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-22	Tianyi Liang	Fixed bug 589	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-11-04	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-10-22	Tianyi Liang	remove nested re or; opt loop	blob \| commitdiff \| raw \| diff to current
2013-10-15	Tianyi Liang	removes some junks	blob \| commitdiff \| raw \| diff to current
2013-10-15	Tianyi Liang	removes some junks	blob \| commitdiff \| raw \| diff to current
2013-10-14	Tianyi Liang	Adds Regular Expression support.	blob \| commitdiff \| raw \| diff to current
2013-10-11	Tianyi Liang	Adds regular expression support, it is actually CFL...	blob \| commitdiff \| raw \| diff to current
2013-10-11	Tianyi Liang	add constant membership	blob \| commitdiff \| raw \| diff to current
2013-10-11	Tianyi Liang	add constant membership	blob \| commitdiff \| raw \| diff to current
2013-09-30	Liana Hadarean	merged golden	blob \| commitdiff \| raw \| diff to current
2013-09-13	Kshitij Bansal	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2013-09-11	Tianyi Liang	Theory of strings.	blob \| commitdiff \| raw \| diff to current

RSS Atom