summaryrefslogtreecommitdiff
path: root/src/theory/strings
AgeCommit message (Expand)Author
2021-11-03Refactor skolem construction (#7561)Andrew Reynolds
2021-11-03Formalize more string skolems (#7554)Andrew Reynolds
2021-10-28Properly guard proof construction for STRINGS_EXTF_EQ_REW (#7519)Andrew Reynolds
2021-10-27Avoid non-terminating check with assumptions in strings rewriter (#7503)Andrew Reynolds
2021-10-27Deterministic variables for RE elim (#7489)Andrew Reynolds
2021-10-24Add new eager conflict detection in strings for integer equivalence classes (...Andrew Reynolds
2021-10-22Refactor theory inference manager constructor (#7457)Andrew Reynolds
2021-10-22Do not use global proxy variable attribute for strings (#7460)Andrew Reynolds
2021-10-20Add basic regular expression type enumerator (#7416)Andrew Reynolds
2021-10-19Support sequences of fixed finite cardinality (#7371)Andrew Reynolds
2021-10-15Fix issues related to proofs of lemmas with duplicate conclusions in strings ...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-07Fast exit for string extended equality rewriter (#7312)Andrew Reynolds
2021-10-06Eliminate more hard coded uses of user context (#7309)Andrew Reynolds
2021-10-04Refactor internally generated bounded quantified formulas (#7291)Andrew Reynolds
2021-10-04Move isFiniteType from theory engine to Env (#7287)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-24Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)Andrew Reynolds
2021-09-23Generalize string enumerator for fixed length sequences (#7234)Andrew Reynolds
2021-09-22Add extensionality option for strings disequalities (#7229)Andrew Reynolds
2021-09-13Remove context getters from `TheoryState` (#7174)Andres Noetzli
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres Noetzli
2021-09-01Lazy proof reconstruction for strings theory solver (#7096)Andrew Reynolds
2021-08-31Fix normal forms context-dependent simplification for strings (#7090)Andrew Reynolds
2021-08-24Uniform treatment of trusted theory inferences in proofs (#7044)Andrew Reynolds
2021-08-23Purify substitutions in strings proof reconstruction (#7035)Andrew Reynolds
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
2021-08-16Use InferenceManager in ExtTheory (#7006)Gereon Kremer
2021-08-16Make Theory class use Env (#7011)Gereon Kremer
2021-08-16[Strings] Make fact detection more robust (#7007)Andres Noetzli
2021-08-05Fix policy for rewriting string equalities (#6916)Andrew Reynolds
2021-07-14Fix models for sequences of infinite element type (#6870)Andrew Reynolds
2021-07-05[Strings] Fix incorrect rewrite (#6837)Andres Noetzli
2021-07-02Fix rewriter for negative constant seq.nth (#6827)Andrew Reynolds
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-28Rename internal string kinds to match API (#6797)Andrew Reynolds
2021-06-21Fix cases of ITE within regular expressions (#6783)Andrew Reynolds
2021-06-22Set up fine grained equality notifications (#6734)Andrew Reynolds
2021-06-08Fix for 2 dimensional dependent bounded quantifiers (#6710)Andrew Reynolds
2021-06-07Fix str.update reduction (#6696)Andrew Reynolds
2021-06-05Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)Andres Noetzli
2021-06-04Fix handling of start index in `str.indexof_re` (#6674)Andres Noetzli
2021-06-02Remove option to ignore negative memberships (#6665)Andres Noetzli
2021-06-02Make `STRINGS_CTN_DECOMPOSE` an explicit conflict (#6663)Andres Noetzli
2021-05-31Compute model values for nested sequences in order (#6631)Andres Noetzli
2021-05-27`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)Andres Noetzli
2021-05-27Fix regular expression aggressive elim (#6627)Andrew Reynolds
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback