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

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

2020-04-07	Andrew Reynolds	Enum for all remaining string inferences (#4220)	blob \| commitdiff \| raw
2020-04-05	Andrew Reynolds	Type-independent preregistration of empty word (#4205)	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	blob \| commitdiff \| raw \| diff to current
2020-04-02	Andrew Reynolds	Introduce enums for all string inferences, excluding...	blob \| commitdiff \| raw \| diff to current
2020-04-02	Andres Noetzli	Initialize theory rewriters in theories (#4197)	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andrew Reynolds	Support unicode internal representation and escape...	blob \| commitdiff \| raw \| diff to current
2020-03-26	Andrew Reynolds	Add stats for string reductions, lemmas and conflicts...	blob \| commitdiff \| raw \| diff to current
2020-03-26	Andrew Reynolds	Care graphs based on polymorphic operators in strings...	blob \| commitdiff \| raw \| diff to current
2020-03-25	Andrew Reynolds	Generalize more uses of string-specific functions...	blob \| commitdiff \| raw \| diff to current
2020-03-23	Andres Noetzli	Collect statistics about normal form inferences (#4127)	blob \| commitdiff \| raw \| diff to current
2020-03-20	Andrew Reynolds	Generalize mkConcat for types (#4123)	blob \| commitdiff \| raw \| diff to current
2020-03-20	Andrew Reynolds	Split string-specific operators from TheoryStringsRewri...	blob \| commitdiff \| raw \| diff to current
2020-03-20	Andrew Reynolds	Refactor enumerator for strings (#4014)	blob \| commitdiff \| raw \| diff to current
2020-03-09	Andrew Reynolds	Convert more uses of strings to words (#3921)	blob \| commitdiff \| raw \| diff to current
2020-03-02	Andrew Reynolds	Split collect model info by types in strings (#3847)	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andres Noetzli	Add support for str.from_code (#3829)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Fix large models for strings (#3835)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2020-02-23	Andrew Reynolds	Minor refactoring of equality notifications (#3798)	blob \| commitdiff \| raw \| diff to current
2020-02-22	Andrew Reynolds	Move check memberships to reg exp solver (#3793)	blob \| commitdiff \| raw \| diff to current
2020-02-22	Andrew Reynolds	Move cardinality inference scheme to base solver in...	blob \| commitdiff \| raw \| diff to current
2020-02-21	Andrew Reynolds	Split extended functions solver in strings (#3768)	blob \| commitdiff \| raw \| diff to current
2020-02-15	Andrew Reynolds	Move proxy variables to InferenceManager in strings...	blob \| commitdiff \| raw \| diff to current
2020-02-08	Andrew Reynolds	Split strings finite model finding strategy (#3727)	blob \| commitdiff \| raw \| diff to current
2020-02-08	Andrew Reynolds	Split core solver from the theory of strings (#3713)	blob \| commitdiff \| raw \| diff to current
2020-02-04	Andrew Reynolds	Split base solver from the theory of strings (#3680)	blob \| commitdiff \| raw \| diff to current
2020-02-04	Andres Noetzli	Revert semantic change from refactoring (#3711)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Move disequality list to solver state in strings (...	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andres Noetzli	Better heuristics for marking congruent variables ...	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Modularize more steps in the strings strategy (#3676)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Minor updates to string utilities (#3675)	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-17	Mathias Preiner	Generate code for options with modes. (#3561)	blob \| commitdiff \| raw \| diff to current
2019-12-04	Andres Noetzli	Fix corner case in model construction of strings (...	blob \| commitdiff \| raw \| diff to current
2019-11-27	Andrew Reynolds	Fix indexof range lemma (#3499)	blob \| commitdiff \| raw \| diff to current
2019-11-06	Andrew Reynolds	Move more string utility functions (#3398)	blob \| commitdiff \| raw \| diff to current
2019-11-01	Andres Noetzli	Fix and refactor TheoryStrings::checkFlatForms() (...	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-10-16	Andrew Reynolds	Solver state for theory of strings (#3181)	blob \| commitdiff \| raw \| diff to current
2019-09-27	Andrew Reynolds	Fix case of disjunctive conclusion in strings (#3254)	blob \| commitdiff \| raw \| diff to current
2019-09-25	Andrew Reynolds	Fix off by one error in strings flat form explanation...	blob \| commitdiff \| raw \| diff to current
2019-09-19	Andrew Reynolds	Support context-(in)dependent decision strategies....	blob \| commitdiff \| raw \| diff to current
2019-08-30	Andres Noetzli	Better heuristic for str.code/re.range (#3220)	blob \| commitdiff \| raw \| diff to current
2019-08-23	Andrew Reynolds	Infer emptiness instead of splitting when a string...	blob \| commitdiff \| raw \| diff to current
2019-08-22	Andrew Reynolds	Local substitutions for context-depdendent simplificat...	blob \| commitdiff \| raw \| diff to current
2019-08-13	Andrew Reynolds	Update option to disable symbolic definitions in string...	blob \| commitdiff \| raw \| diff to current
2019-07-31	Andrew Reynolds	Eager conflict detection in strings based on constant...	blob \| commitdiff \| raw \| diff to current
2019-07-30	Andrew Reynolds	Handle RE intersections modulo equality (#3120)	blob \| commitdiff \| raw \| diff to current
2019-07-25	Andrew Reynolds	Split infer info data structure in strings (#3107)	blob \| commitdiff \| raw \| diff to current
2019-07-17	Andrew Reynolds	Minor clean in strings. (#3093)	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-07-06	Andrew Reynolds	Refactor strings to use an inference manager object...	blob \| commitdiff \| raw \| diff to current
2019-06-24	Andrew Reynolds	Stratify unfolding of regular expressions based on...	blob \| commitdiff \| raw \| diff to current
2019-06-18	Andres Noetzli	Strings: More aggressive skolem normalization (#2761)	blob \| commitdiff \| raw \| diff to current
2019-06-14	Andres Noetzli	Add lemma for the range of values of str.indexof (...	blob \| commitdiff \| raw \| diff to current
2019-06-13	Andrew Reynolds	Shorten explanation for strings inference I_Norm_S...	blob \| commitdiff \| raw \| diff to current
2019-06-10	Andrew Reynolds	Optimization for strings normalize disequalities (...	blob \| commitdiff \| raw \| diff to current
2019-05-02	Andrew Reynolds	Simple optimizations to core strings theory. (#2988)	blob \| commitdiff \| raw \| diff to current
2019-04-23	Andrew Reynolds	Refactor normal forms in strings (#2897)	blob \| commitdiff \| raw \| diff to current
2019-04-17	Andrew Reynolds	Fix extended function decomposition (#2960)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2019-03-26	Andrew Reynolds	Fix a few warnings (#2898)	blob \| commitdiff \| raw \| diff to current
2019-03-24	Andrew Reynolds	Split regular expression solver (#2891)	blob \| commitdiff \| raw \| diff to current
2019-03-22	Andrew Reynolds	Revisit strings extended function decomposition (...	blob \| commitdiff \| raw \| diff to current
2019-03-21	Andrew Reynolds	Fix bad comparison in RE solver's addMembership (...	blob \| commitdiff \| raw \| diff to current
2019-03-14	Andrew Reynolds	Fix function term set for theory strings compute care...	blob \| commitdiff \| raw \| diff to current
2019-01-15	Andres Noetzli	Strings: Add option to change loop process mode (#2794)	blob \| commitdiff \| raw \| diff to current
2018-12-07	Andres Noetzli	Strings: Make EXTF_d inference more conservative (...	blob \| commitdiff \| raw \| diff to current
2018-11-27	Andrew Reynolds	Make (T)NodeTrie a general utility (#2489)	blob \| commitdiff \| raw \| diff to current
2018-11-21	Andrew Reynolds	Support string replace all (#2704)	blob \| commitdiff \| raw \| diff to current
2018-10-17	Andrew Reynolds	Fix context-dependent for positive contains reduction...	blob \| commitdiff \| raw \| diff to current
2018-10-16	Andrew Reynolds	Improve strings reductions including skolem caching...	blob \| commitdiff \| raw \| diff to current
2018-10-11	Andrew Reynolds	Fix string ext inference for rewrites that introduce...	blob \| commitdiff \| raw \| diff to current
2018-10-09	Andrew Reynolds	Fix string register extended terms (#2597)	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-19	Andrew Reynolds	Refactor strings extended functions inferences (#2480)	blob \| commitdiff \| raw \| diff to current
2018-09-18	Andrew Reynolds	Decision strategy: incorporate strings fmf. (#2485)	blob \| commitdiff \| raw \| diff to current
2018-09-17	Andrew Reynolds	More aggressive skolem caching for strings, document...	blob \| commitdiff \| raw \| diff to current
2018-09-17	Andrew Reynolds	Make strings model construction robust to lengths that...	blob \| commitdiff \| raw \| diff to current
2018-09-14	Andrew Reynolds	Add Skolem cache for strings, refactor length registrat...	blob \| commitdiff \| raw \| diff to current
2018-09-12	Andrew Reynolds	Fix for when strings process loop is disabled. (#2456)	blob \| commitdiff \| raw \| diff to current
2018-08-30	Andrew Reynolds	Add regular expression elimination module (#2400)	blob \| commitdiff \| raw \| diff to current
2018-08-26	Andres Noetzli	Use uniform length limit for String constants (#2381)	blob \| commitdiff \| raw \| diff to current
2018-08-26	Andrew Reynolds	Fix unsigned integer type issues in strings (#2380)	blob \| commitdiff \| raw \| diff to current
2018-08-23	Andrew Reynolds	Fixing some coverity warnings (#2357)	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-08-07	Andrew Reynolds	Make flat form inferences optional in strings (#2277)	blob \| commitdiff \| raw \| diff to current
2018-08-02	Andrew Reynolds	Make strings robust to regular expression variables...	blob \| commitdiff \| raw \| diff to current
2018-07-06	Andrew Reynolds	Split ext theory to own file and document (#1809)	blob \| commitdiff \| raw \| diff to current
2018-07-05	Andrew Reynolds	Make string length lemmas more robust to rewriting...	blob \| commitdiff \| raw \| diff to current
2018-07-02	Andrew Reynolds	Remove some dead code from theory strings (#2125)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-05-22	Andrew Reynolds	Infrastructure for strings strategies (#1883)	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-04-16	Andrew Reynolds	Make 256 the default cardinality for strings (#1783)	blob \| commitdiff \| raw \| diff to current
2018-04-16	Andrew Reynolds	Make strings fmf apply to all but internally generated...	blob \| commitdiff \| raw \| diff to current
2018-04-15	Andrew Reynolds	Fix type error with regexp (#1778)	blob \| commitdiff \| raw \| diff to current
2018-04-14	Andrew Reynolds	Disable split for negative contains. (#1774)	blob \| commitdiff \| raw \| diff to current
2018-03-25	Andrew Reynolds	Cleanup various exit calls (#1692)	blob \| commitdiff \| raw \| diff to current
next

RSS Atom