summaryrefslogtreecommitdiff
path: root/src/theory/strings/term_registry.cpp
AgeCommit message (Expand)Author
2021-11-11Remove `ConstantMap<Rational>`Andres Noetzli
2021-11-09Remove more static option accesses (#7582)Gereon Kremer
2021-11-05Remove many static calls to rewrite (#7580)Andrew Reynolds
2021-10-22Do not use global proxy variable attribute for strings (#7460)Andrew Reynolds
2021-10-07Make the cardinality of the alphabet of strings configurable (#7298)Andrew Reynolds
2021-10-07Miscellaneous fixes from proof-new (#7313)Andrew Reynolds
2021-10-04Eliminating static calls to rewriter from strings (#7302)Andrew Reynolds
2021-09-29Add the strings array solver (#7232)Andrew Reynolds
2021-09-13Remove context getters from `TheoryState` (#7174)Andres Noetzli
2021-06-28Rename internal string kinds to match API (#6797)Andrew Reynolds
2021-06-22Set up fine grained equality notifications (#6734)Andrew Reynolds
2021-06-04Fix handling of start index in `str.indexof_re` (#6674)Andres Noetzli
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-18(proof-new) Miscellaneous updates to strings from proof-new (#6557)Andrew Reynolds
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-21Simplify strings term registration (#6174)Andrew Reynolds
2021-03-16Further standardization of strings statistics (#6128)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-02-10Simplify method for inferring proxy lemmas in strings (#5789)Andrew Reynolds
2020-12-14Fix SAT-context dependent issue in strings preregistration (#5564)Andrew Reynolds
2020-11-06(proof-new) Miscellaneous changes to strings for proofs (#5362)Andrew Reynolds
2020-11-02Update strings proxy variable map to be context independent (#5377)Andrew Reynolds
2020-10-23Fix related to preregistering boolean term variables in strings (#5331)Andrew Reynolds
2020-10-19Expand `seq.nth` lazily (#5287)yoni206
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-09(proof-new) Generalize single step helper in eager proof generator (#5046)Andrew Reynolds
2020-08-19Simplify trigger notifications in equality engine (#4921)Andrew Reynolds
2020-08-19Require `--strings-exp` when using `str.substr` (#4916)Andres Noetzli
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-08-12(proof-new) Proof support in the strings term registry. (#4876)Andrew Reynolds
2020-08-05[Strings] Add eager context-dependent evaluation (#4847)Andres Noetzli
2020-07-12Add support for string/sequence update (#4725)Andrew Reynolds
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
2020-06-19(proof-new) Updates to strings term registry (#4599)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-10Add support for str.replace_re/str.replace_re_all (#4594)Andres Noetzli
2020-05-28Fix term registry for constant case, simplify. (#4538)Andrew Reynolds
2020-05-20Throw logic exception for equality between regular expressions (#4505)Andrew Reynolds
2020-04-28Register lower bound for str.to_int (#4408)Andres Noetzli
2020-04-15Split TermRegistry object from TheoryStrings (#4312)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback