summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Expand)Author
2020-03-09Convert more uses of strings to words (#3921)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-03-02 Split collect model info by types in strings (#3847)Andrew Reynolds
2020-02-29Convert more uses of string to word (#3834)Andrew Reynolds
2020-02-28Add support for str.from_code (#3829)Andres Noetzli
2020-02-27Fix large models for strings (#3835)Andrew Reynolds
2020-02-26Add support for is_digit and regular expression difference (#3828)Andrew Reynolds
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-26Some initial work on using words (#3819)Andrew Reynolds
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-26Move equivalence class info to its own file in strings (#3799)Andrew Reynolds
2020-02-24Utilities for words (#3797)Andrew Reynolds
2020-02-22Minor refactoring of equality notifications (#3798)Andrew Reynolds
2020-02-22 Move check memberships to reg exp solver (#3793)Andrew Reynolds
2020-02-21Move cardinality inference scheme to base solver in strings (#3792)Andrew Reynolds
2020-02-21Split extended functions solver in strings (#3768)Andrew Reynolds
2020-02-16Activate reverse variant of F-Split inference (#3745)Andres Noetzli
2020-02-15Move proxy variables to InferenceManager in strings (#3758)Andrew Reynolds
2020-02-11Remove `--strings-binary-csp` option (#3743)Andres Noetzli
2020-02-10Refactor `CoreSolver::processSimpleNEq()` (#3736)Andres Noetzli
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
2020-01-09Optimize str.substr reduction (#3595)Andres Noetzli
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-12-06Simplify rewrite for character matching (#3545)Andres Noetzli
2019-12-06Use str.subtr in str.to.int/int.to.str reduction (#3544)Andres Noetzli
2019-12-06Add lemma for str.to.int/int.to.str (#3541)Andres Noetzli
2019-12-05Bi-directional unrolling of R* regular expressions (#3532)Andres Noetzli
2019-12-03Fix corner case in model construction of strings (#3524)Andres Noetzli
2019-12-03Rewrite `str.contains` used for character matching (#3519)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-23Fixes for SyGuS + regular expressions (#3313)Andrew Reynolds
2019-10-16Solver state for theory of strings (#3181)Andrew Reynolds
2019-10-14Minor refactor in strings rewriter (#3387)Andrew Reynolds
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
2019-10-06Fix str to int reduction (#3358)Andrew Reynolds
2019-09-29Add rewrite for splitting equalities (#2957)Andres Noetzli
2019-09-28Introduce template classes for simple type rules (#2835)Andres Noetzli
2019-09-27Fix case of disjunctive conclusion in strings (#3254)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback