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

[cvc5.git] / src / theory / strings / theory_strings.cpp

2014-04-17	Kshitij Bansal	simplify mkSkolem naming system: don't use $$	blob \| commitdiff \| raw
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-31	Tianyi Liang	add str to u16/u32, and u16/u32 to str	blob \| commitdiff \| raw \| diff to current
2014-03-31	Tianyi Liang	add str to u16/u32, and u16/u32 to str	blob \| commitdiff \| raw \| diff to current
2014-03-28	Tianyi Liang	minor printer fix; intersection fix	blob \| commitdiff \| raw \| diff to current
2014-03-27	Tianyi Liang	adds new feature: re.loop	blob \| commitdiff \| raw \| diff to current
2014-03-27	Tianyi Liang	deriv symbolic regexp	blob \| commitdiff \| raw \| diff to current
2014-03-27	Tianyi Liang	adds intersection	blob \| commitdiff \| raw \| diff to current
2014-03-27	Tianyi Liang	adds new feature: re.loop	blob \| commitdiff \| raw \| diff to current
2014-03-26	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-26	Tianyi Liang	deriv symbolic regexp	blob \| commitdiff \| raw \| diff to current
2014-03-26	Tianyi Liang	adds intersection	blob \| commitdiff \| raw \| diff to current
2014-03-26	Tianyi Liang	deriv symbolic regexp	blob \| commitdiff \| raw \| diff to current
2014-03-25	Tianyi Liang	adds intersection	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-17	Tianyi Liang	hot fix for pre-reg term caching in strings	blob \| commitdiff \| raw \| diff to current
2014-03-17	Tianyi Liang	hot fix for pre-reg term caching in strings	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-03-10	Tianyi Liang	adds intro vars length cache	blob \| commitdiff \| raw \| diff to current
2014-03-10	Tianyi Liang	minor change for strings-fmf	blob \| commitdiff \| raw \| diff to current
2014-03-10	Tianyi Liang	minor change for strings-fmf	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	bring back D-Norm	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	bring back D-Norm	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	adds incremental for strings; clean-up codes	blob \| commitdiff \| raw \| diff to current
2014-03-07	Tianyi Liang	adds incremental for strings; clean-up codes	blob \| commitdiff \| raw \| diff to current
2014-03-01	Tianyi Liang	minor clean-up, bring back derivatives	blob \| commitdiff \| raw \| diff to current
2014-03-01	Tianyi Liang	a new regular expression engine for solving both positi...	blob \| commitdiff \| raw \| diff to current
2014-02-28	Tianyi Liang	minor clean-up, bring back derivatives	blob \| commitdiff \| raw \| diff to current
2014-02-28	Tianyi Liang	a new regular expression engine for solving both positi...	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	Tianyi Liang	reorganize substr, fix some potential bugs, adds cache...	blob \| commitdiff \| raw \| diff to current
2014-02-21	Tianyi Liang	reorganize substr, fix some potential bugs, adds cache...	blob \| commitdiff \| raw \| diff to current
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-20	Tianyi Liang	hot fix for str2int/int2str	blob \| commitdiff \| raw \| diff to current
2014-02-20	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-20	Tianyi Liang	hot fix for str2int/int2str	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch 'master' of github.com:CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-18	Tianyi Liang	switch to total function str.to.int: maps invalid and...	blob \| commitdiff \| raw \| diff to current
2014-02-18	Tianyi Liang	add str2int	blob \| commitdiff \| raw \| diff to current
2014-02-17	Tianyi Liang	type conversion	blob \| commitdiff \| raw \| diff to current
2014-02-17	Tianyi Liang	type conversion	blob \| commitdiff \| raw \| diff to current
2014-02-14	Tianyi Liang	partial function charat	blob \| commitdiff \| raw \| diff to current
2014-02-14	Tianyi Liang	fix expanding def	blob \| commitdiff \| raw \| diff to current
2014-02-12	Tianyi Liang	bug fix for reverse check	blob \| commitdiff \| raw \| diff to current
2014-02-11	Tianyi Liang	resolve merge conflicts	blob \| commitdiff \| raw \| diff to current
2014-02-11	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-11	Tianyi Liang	minor fix for merge	blob \| commitdiff \| raw \| diff to current
2014-02-11	Tianyi Liang	minor cleanup for merge	blob \| commitdiff \| raw \| diff to current
2014-02-11	Tianyi Liang	minor fix for merge	blob \| commitdiff \| raw \| diff to current
2014-02-06	Tianyi Liang	minor cleanup for merge	blob \| commitdiff \| raw \| diff to current
2014-02-06	Tianyi Liang	minor fix for merge	blob \| commitdiff \| raw \| diff to current
2014-02-06	Tianyi Liang	minor cleanup for merge	blob \| commitdiff \| raw \| diff to current
2014-02-05	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-05	Tianyi Liang	minor fix for merge	blob \| commitdiff \| raw \| diff to current
2014-02-05	Tianyi Liang	minor fix for merge	blob \| commitdiff \| raw \| diff to current
2014-02-05	Andrew Reynolds	Bug fix for theory strings related to old cycle detecti...	blob \| commitdiff \| raw \| diff to current
2014-01-31	Tianyi Liang	Substr fix: (= (str.substr "" 0 3) "xxx") should be...	blob \| commitdiff \| raw \| diff to current
2014-01-30	Tianyi Liang	stats for eq/diseq splits	blob \| commitdiff \| raw \| diff to current
2014-01-30	Tianyi Liang	change string stats text names	blob \| commitdiff \| raw \| diff to current
2014-01-30	Tianyi Liang	adds stats	blob \| commitdiff \| raw \| diff to current
2014-01-29	Tianyi Liang	roll back to uf implementation for substr and charat	blob \| commitdiff \| raw \| diff to current
2014-01-29	Tianyi Liang	add prefixof, suffixof	blob \| commitdiff \| raw \| diff to current
2014-01-28	Tianyi Liang	merge internal and user of charat & substr into one	blob \| commitdiff \| raw \| diff to current
2014-01-27	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-25	Tianyi Liang	replace charat uf with internal one	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	rev diseq	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	rev const split	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	optimize for the reverse direction	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	rev diseq	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	rev const split	blob \| commitdiff \| raw \| diff to current
2014-01-24	Tianyi Liang	optimize for the reverse direction	blob \| commitdiff \| raw \| diff to current
2014-01-23	Tianyi Liang	fix: constants are inferred to be the same	blob \| commitdiff \| raw \| diff to current
2014-01-23	Tianyi Liang	minor fix	blob \| commitdiff \| raw \| diff to current
2014-01-22	Tianyi Liang	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-01-22	Tianyi Liang	commented out all_supported in strings for now, it...	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	Tianyi Liang	add warning for using strings in ALL_SUPPORTED	blob \| commitdiff \| raw \| diff to current
2014-01-22	Morgan Deters	Delay QuantifiersEngine and UF strong solver initializa...	blob \| commitdiff \| raw \| diff to current
2014-01-20	Tianyi Liang	improve string contains	blob \| commitdiff \| raw \| diff to current
2014-01-18	Tianyi Liang	strings with new ideas	blob \| commitdiff \| raw \| diff to current
2014-01-18	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-17	Tianyi Liang	strings with new ideas	blob \| commitdiff \| raw \| diff to current
2014-01-17	Kshitij Bansal	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-15	Tianyi Liang	adds smt2 print for strings	blob \| commitdiff \| raw \| diff to current
2014-01-15	Tianyi Liang	adds smt2 print for strings	blob \| commitdiff \| raw \| diff to current
2014-01-10	Tianyi Liang	normal form breaking	blob \| commitdiff \| raw \| diff to current
2014-01-10	Tianyi Liang	move new functions under exp options	blob \| commitdiff \| raw \| diff to current
2014-01-09	Tianyi Liang	add constant replace, indexof	blob \| commitdiff \| raw \| diff to current
2014-01-09	Tianyi Liang	add constant replace, indexof	blob \| commitdiff \| raw \| diff to current
2014-01-09	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-09	Tianyi Liang	Another way to handle negative contain	blob \| commitdiff \| raw \| diff to current
2014-01-08	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-08	Tianyi Liang	clean some code	blob \| commitdiff \| raw \| diff to current
2014-01-08	Tianyi Liang	remove a warning in strings	blob \| commitdiff \| raw \| diff to current
2014-01-08	Tianyi Liang	minor fix, bring back the assertion.	blob \| commitdiff \| raw \| diff to current
2014-01-08	Tianyi Liang	string contain changes	blob \| commitdiff \| raw \| diff to current
next

RSS Atom