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

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

2016-07-21	ajreynol	Fixes for strings, explanations for constant split...	blob \| commitdiff \| raw
2016-07-20	ajreynol	Infer conflicts in strings based on abstracting equalit...	blob \| commitdiff \| raw \| diff to current
2016-07-16	ajreynol	Refactor strings extf evaluation info. Ensure strings...	blob \| commitdiff \| raw \| diff to current
2016-07-15	ajreynol	Minor simplification to normal form explanations.	blob \| commitdiff \| raw \| diff to current
2016-07-08	ajreynol	Minor fix to last commit.	blob \| commitdiff \| raw \| diff to current
2016-07-08	ajreynol	Simplifications for strings normal forms, fix case...	blob \| commitdiff \| raw \| diff to current
2016-07-07	ajreynol	Refactoring of strings preprocess module. When enabled...	blob \| commitdiff \| raw \| diff to current
2016-07-06	ajreynol	Minor cleanup in strings, mostly related to negated...	blob \| commitdiff \| raw \| diff to current
2016-07-06	ajreynol	Add comment field for model, resolves hack for printing...	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-06-08	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-06	guykatzz	Merge pull request #85 from CVC4/master_for_proof_merge	blob \| commitdiff \| raw \| diff to current
2016-06-03	ajreynol	Remove NodeListMap from strings, fixes memory leaks...	blob \| commitdiff \| raw \| diff to current
2016-06-01	ajreynol	Initial infrastructure for bounded set quantification...	blob \| commitdiff \| raw \| diff to current
2016-05-21	ajreynol	Minor fix for strings.	blob \| commitdiff \| raw \| diff to current
2016-05-20	ajreynol	Minor fix to strings, cleanup in datatypes.	blob \| commitdiff \| raw \| diff to current
2016-05-20	ajreynol	Improvements to theory combination + strings: do not...	blob \| commitdiff \| raw \| diff to current
2016-05-06	ajreynol	Minor clean up, fixes related to sygus.	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-03-07	ajreynol	Minor change to F-Length inference in strings. No inter...	blob \| commitdiff \| raw \| diff to current
2016-03-03	ajreynol	Add missing code to track dependencies recursively...	blob \| commitdiff \| raw \| diff to current
2016-03-01	ajreynol	Shorter explanations for strings based on tracking...	blob \| commitdiff \| raw \| diff to current
2016-02-26	ajreynol	Refactoring of inferences in strings. Add several options.	blob \| commitdiff \| raw \| diff to current
2016-02-25	ajreynol	Minor improvement to partial qe. Add options for repres...	blob \| commitdiff \| raw \| diff to current
2016-02-24	ajreynol	Add entailment checks between length terms to reduce...	blob \| commitdiff \| raw \| diff to current
2016-02-02	Tim King	Moving dump., command., model.*, and ite_removal...	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2016-01-13	ajreynol	Lemma cache datatypes. Do not send true lemma in quanti...	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Removing StatisticsRegistry's static functions current...	blob \| commitdiff \| raw \| diff to current
2016-01-06	Tim King	Add SmtGlobals Class	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-11-17	ajreynol	Improve relevant domain computation for arithmetic...	blob \| commitdiff \| raw \| diff to current
2015-10-24	ajreynol	Fixes related to string contains.	blob \| commitdiff \| raw \| diff to current
2015-10-21	ajreynol	Minor refactoring in strings related to length.	blob \| commitdiff \| raw \| diff to current
2015-10-20	ajreynol	Refactor strings, remove old cycle checks in normalize...	blob \| commitdiff \| raw \| diff to current
2015-10-19	ajreynol	Clean up explanations involving string length. Add...	blob \| commitdiff \| raw \| diff to current
2015-10-19	ajreynol	Improve stratification of strings extended function...	blob \| commitdiff \| raw \| diff to current
2015-10-19	ajreynol	Improve regexp rewriter, simplify regexp preprocess...	blob \| commitdiff \| raw \| diff to current
2015-10-15	ajreynol	Fix congruence check in strings, fixes bug 686.	blob \| commitdiff \| raw \| diff to current
2015-10-15	ajreynol	Change semantics of str.substr to allow endpoint out...	blob \| commitdiff \| raw \| diff to current
2015-10-15	ajreynol	Decompose string contains, minor refactoring.	blob \| commitdiff \| raw \| diff to current
2015-10-11	ajreynol	Fix strings preprocessing + incremental, fixes bug...	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-07	ajreynol	Minor improvements, add endpoint eq inference to strings.	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	Fixes related to explanations for cycles, sym inference...	blob \| commitdiff \| raw \| diff to current
2015-10-02	ajreynol	Improvements to rewriter for regexp, contains, indexof...	blob \| commitdiff \| raw \| diff to current
2015-10-01	ajreynol	Evaluate extended operators on partially concrete argum...	blob \| commitdiff \| raw \| diff to current
2015-10-01	ajreynol	More improvements to strings. More aggressive inference...	blob \| commitdiff \| raw \| diff to current
2015-09-30	ajreynol	Refactor strings, bug fix inferences vs lemmas.	blob \| commitdiff \| raw \| diff to current
2015-09-28	ajreynol	Minor fix	blob \| commitdiff \| raw \| diff to current
2015-09-28	ajreynol	Minor fixes to strings, add regressions.	blob \| commitdiff \| raw \| diff to current
2015-09-28	ajreynol	Fix bug for trivial extf inferences in strings. Improve...	blob \| commitdiff \| raw \| diff to current
2015-09-27	ajreynol	Improved handling of extended operators. Do preprocess...	blob \| commitdiff \| raw \| diff to current
2015-09-26	ajreynol	Lazy preprocessing of extended operators in strings...	blob \| commitdiff \| raw \| diff to current
2015-09-09	ajreynol	Fix bug in strings rewriter regarding lengths of substr...	blob \| commitdiff \| raw \| diff to current
2015-08-18	Tianyi Liang	fix for bug663	blob \| commitdiff \| raw \| diff to current
2015-07-30	ajreynol	Implement virtual term substitution for non-nested...	blob \| commitdiff \| raw \| diff to current
2015-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-04-22	Kshitij Bansal	Merge pull request #73 from kbansal/parser-dont-tokenize	blob \| commitdiff \| raw \| diff to current
2015-04-17	Tianyi Liang	Patch for Kshitij's fix on requriePhase	blob \| commitdiff \| raw \| diff to current
2015-04-17	Kshitij Bansal	Merge pull request #72 from kbansal/decision-requirephase	blob \| commitdiff \| raw \| diff to current
2015-04-09	ajreynol	Bug fix negative contains cache.	blob \| commitdiff \| raw \| diff to current
2015-04-02	Kshitij Bansal	Merge pull request #71 from kbansal/const-are-triggers	blob \| commitdiff \| raw \| diff to current
2015-03-25	Kshitij Bansal	change const are triggers from false to true in equalit...	blob \| commitdiff \| raw \| diff to current
2015-03-16	Tianyi Liang	Add requirePhase len(x) = 0.	blob \| commitdiff \| raw \| diff to current
2015-03-11	ajreynol	Strings split on constant lengths, add length=0 to...	blob \| commitdiff \| raw \| diff to current
2015-02-06	Tianyi Liang	Improved string performance, thanks to Peter's benchmarks.	blob \| commitdiff \| raw \| diff to current
2015-02-06	Tianyi Liang	Improved string performance, thanks to Peter's benchmarks.	blob \| commitdiff \| raw \| diff to current
2015-01-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-27	Dejan Jovanovic	Adding an option to the equality engine constructor...	blob \| commitdiff \| raw \| diff to current
2014-12-22	Tianyi Liang	bug fix for constant regular expression model building	blob \| commitdiff \| raw \| diff to current
2014-12-22	Tianyi Liang	bug fix for constant regular expression model building	blob \| commitdiff \| raw \| diff to current
2014-12-06	Tianyi Liang	Added C++/Java api examples;	blob \| commitdiff \| raw \| diff to current
2014-12-06	Tianyi Liang	Added C++/Java api examples;	blob \| commitdiff \| raw \| diff to current
2014-12-05	Tianyi Liang	Relaxed the constant requirement for regular expression...	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-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	add more functions for regular expressions	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	add more functions for regular expressions	blob \| commitdiff \| raw \| diff to current
2014-11-20	ajreynol	Disable constants sharing in eq engine, disable hack...	blob \| commitdiff \| raw \| diff to current
2014-11-17	Morgan Deters	New, uniform checkTime statistic for all theories ...	blob \| commitdiff \| raw \| diff to current
2014-11-11	Kshitij Bansal	Merge pull request #64 from mdeters/theorysets-hashset...	blob \| commitdiff \| raw \| diff to current
2014-11-10	Tianyi Liang	Merge pull request #63 from mdeters/theorystrings-hashs...	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-09	Morgan Deters	Update TheoryStrings to use CDHashSet<>::key_begin...	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-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-17	Tianyi Liang	Minor change for performance according to Andy's sugges...	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
next

RSS Atom