summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
AgeCommit message (Expand)Author
2015-10-02Improvements to rewriter for regexp, contains, indexof. Improvements and fixe...ajreynol
2015-10-01Evaluate extended operators on partially concrete arguments. More aggressive ...ajreynol
2015-10-01More improvements to strings. More aggressive inference of constant eqc, redu...ajreynol
2015-09-30Refactor strings, bug fix inferences vs lemmas.ajreynol
2015-09-28Minor fixajreynol
2015-09-28Minor fixes to strings, add regressions.ajreynol
2015-09-28Fix bug for trivial extf inferences in strings. Improve caching for splits in...ajreynol
2015-09-27Improved handling of extended operators. Do preprocess on memberships eagerl...ajreynol
2015-09-26Lazy preprocessing of extended operators in strings. Add regressions. Fixes ...ajreynol
2015-09-09Fix bug in strings rewriter regarding lengths of substr terms.ajreynol
2015-08-17fix for bug663Tianyi Liang
2015-07-30Implement virtual term substitution for non-nested quantifiers. Fix soundnes...ajreynol
2015-04-17Patch for Kshitij's fix on requriePhaseTianyi Liang
2015-04-09Bug fix negative contains cache.ajreynol
2015-03-25change const are triggers from false to true in equality enginesKshitij Bansal
2015-03-16Add requirePhase len(x) = 0.Tianyi Liang
2015-03-11Strings split on constant lengths, add length=0 to split lemma for empty string.ajreynol
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2014-12-26Adding an option to the equality engine constructor to treat all constants asDejan Jovanovic
2014-12-22bug fix for constant regular expression model buildingTianyi Liang
2014-12-06Added C++/Java api examples;Tianyi Liang
2014-12-04Relaxed the constant requirement for regular expression loop;Tianyi Liang
2014-11-26add more functions for regular expressionsTianyi Liang
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. Chang...ajreynol
2014-11-17New, uniform checkTime statistic for all theories (as discussed in meeting).Morgan Deters
2014-11-09Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().Morgan Deters
2014-10-21Fixed bug 589Tianyi Liang
2014-10-17Minor change for performance according to Andy's suggestion.Tianyi Liang
2014-09-03check() optimizationKshitij Bansal
2014-07-25patch for regular expression intersection cachingTianyi Liang
2014-07-24merging...Tianyi Liang
2014-07-24add delayed length lemmasTianyi Liang
2014-07-01Update copyrights.Morgan Deters
2014-06-24Squashed commit of the following:Morgan Deters
2014-05-18minor fix for string equality engine assertion.Tianyi Liang
2014-05-11Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.Tianyi Liang
2014-05-07patch to the last commit: add a single character caseTianyi Liang
2014-05-07fix a bug in containTianyi Liang
2014-05-07add splitsTianyi Liang
2014-05-05fix a bug in replace and containsTianyi Liang
2014-04-29fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlrTianyi Liang
2014-04-28add strings-opt2 for regular splittingTianyi Liang
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-24minor change: add a heuristic for preventing constant splitting.Tianyi Liang
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-03-31add str to u16/u32, and u16/u32 to strTianyi Liang
2014-03-28minor printer fix; intersection fixTianyi Liang
2014-03-27adds new feature: re.loopTianyi Liang
2014-03-27deriv symbolic regexpTianyi Liang
2014-03-27adds intersectionTianyi Liang
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback