summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
AgeCommit message (Expand)Author
2020-02-07Split strings finite model finding strategy (#3727)Andrew Reynolds
2020-02-07Split core solver from the theory of strings (#3713)Andrew Reynolds
2020-02-04Split base solver from the theory of strings (#3680)Andrew Reynolds
2020-02-04Revert semantic change from refactoring (#3711)Andres Noetzli
2020-01-30Move disequality list to solver state in strings (#3678)Andrew Reynolds
2020-01-29Better heuristics for marking congruent variables (#3677)Andres Noetzli
2020-01-29Modularize more steps in the strings strategy (#3676)Andrew Reynolds
2020-01-29Minor updates to string utilities (#3675)Andrew Reynolds
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-03Fix corner case in model construction of strings (#3524)Andres Noetzli
2019-11-27 Fix indexof range lemma (#3499)Andrew Reynolds
2019-11-06Move more string utility functions (#3398)Andrew Reynolds
2019-11-01Fix and refactor TheoryStrings::checkFlatForms() (#3326)Andres Noetzli
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-16Solver state for theory of strings (#3181)Andrew Reynolds
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
2019-09-25 Fix off by one error in strings flat form explanation (#3273)Andrew Reynolds
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-08-29Better heuristic for str.code/re.range (#3220)Andres Noetzli
2019-08-23 Infer emptiness instead of splitting when a string equality rewrites to a co...Andrew Reynolds
2019-08-22 Local substitutions for context-depdendent simplification in strings (#3204)Andrew Reynolds
2019-08-13Update option to disable symbolic definitions in strings (#3180)Andrew Reynolds
2019-07-31Eager conflict detection in strings based on constant prefix/suffix (#3110)Andrew Reynolds
2019-07-30 Handle RE intersections modulo equality (#3120)Andrew Reynolds
2019-07-25Split infer info data structure in strings (#3107)Andrew Reynolds
2019-07-17Minor clean in strings. (#3093)Andrew Reynolds
2019-07-16Add support for str.tolower and str.toupper (#3092)Andrew Reynolds
2019-07-05Refactor strings to use an inference manager object (#3076)Andrew Reynolds
2019-06-24Stratify unfolding of regular expressions based on polarity (#3067)Andrew Reynolds
2019-06-18 Strings: More aggressive skolem normalization (#2761)Andres Noetzli
2019-06-13Add lemma for the range of values of str.indexof (#3054)Andres Noetzli
2019-06-13 Shorten explanation for strings inference I_Norm_S (#3051)Andrew Reynolds
2019-06-10Optimization for strings normalize disequalities (#3047)Andrew Reynolds
2019-05-02Simple optimizations to core strings theory. (#2988)Andrew Reynolds
2019-04-23Refactor normal forms in strings (#2897)Andrew Reynolds
2019-04-17Fix extended function decomposition (#2960)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-26Fix a few warnings (#2898)Andrew Reynolds
2019-03-24 Split regular expression solver (#2891)Andrew Reynolds
2019-03-22Revisit strings extended function decomposition (#2892)Andrew Reynolds
2019-03-21 Fix bad comparison in RE solver's addMembership (#2880)Andrew Reynolds
2019-03-14Fix function term set for theory strings compute care graph. (#2862)Andrew Reynolds
2019-01-15Strings: Add option to change loop process mode (#2794)Andres Noetzli
2018-12-07Strings: Make EXTF_d inference more conservative (#2740)Andres Noetzli
2018-11-27Make (T)NodeTrie a general utility (#2489)Andrew Reynolds
2018-11-21Support string replace all (#2704)Andrew Reynolds
2018-10-17 Fix context-dependent for positive contains reduction (#2644)Andrew Reynolds
2018-10-16Improve strings reductions including skolem caching for contains (#2641)Andrew Reynolds
2018-10-11 Fix string ext inference for rewrites that introduce negation (#2618)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback