summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
AgeCommit message (Expand)Author
2021-10-07Make the cardinality of the alphabet of strings configurable (#7298)Andrew Reynolds
2021-10-06Eliminate more hard coded uses of user context (#7309)Andrew Reynolds
2021-10-04Move isFiniteType from theory engine to Env (#7287)Andrew Reynolds
2021-09-24Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)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-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-05Fix policy for rewriting string equalities (#6916)Andrew Reynolds
2021-07-14Fix models for sequences of infinite element type (#6870)Andrew Reynolds
2021-06-28Rename internal string kinds to match API (#6797)Andrew Reynolds
2021-06-22Set up fine grained equality notifications (#6734)Andrew Reynolds
2021-05-31Compute model values for nested sequences in order (#6631)Andres Noetzli
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-12Ensure sequences of Booleans generate Boolean term variable skolems when appl...Andrew Reynolds
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
2021-04-13Formalize more skolems (#6307)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-05[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)Haniel Barbosa
2021-04-01Simplify caching of regular expression unfolding (#6262)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-29Move decision manager into theory inference manager (#6231)Andrew Reynolds
2021-03-21Simplify strings term registration (#6174)Andrew Reynolds
2021-03-20Improved tracing for equivalence classes of EE (#6169)Andrew Reynolds
2021-03-16Further standardization of strings statistics (#6128)Andrew Reynolds
2021-03-11(proof-new) Clean up uses of witness with skolem lemmas (#6109)Andrew Reynolds
2021-03-10(proof-new) Update ppRewrite to use skolem lemmas (#6102)Andrew Reynolds
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-02-11Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)Gereon Kremer
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
2021-02-08Avoid spurious traversal of terms during preregistration (#5860)Andrew Reynolds
2021-01-15Implement --no-strings-lazy-pp as a preprocessing pass (#5777)Andrew Reynolds
2021-01-13Split eager solver from strings solver state (#5775)Andrew Reynolds
2021-01-08Rename getAntecedent to getPremises (#5754)mudathirmahgoub
2020-12-23(proof-new) Miscelleneous fixes from proof-new (#5714)Andrew Reynolds
2020-12-08Proper implementation of expand definitions for sequences (#5616)Andrew Reynolds
2020-12-07Fix collect model values for sequences of sequences (#5579)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-02Update copyright headers.Aina Niemetz
2020-11-30(proof-new) Proofs for regular expression elimination (#5361)Andrew Reynolds
2020-11-03Add constants from equality engine evaluation to model (#5391)Andres Noetzli
2020-10-29(proof-new) Update the strings inference manager for proofs (#5220)Andrew Reynolds
2020-10-19Expand `seq.nth` lazily (#5287)yoni206
2020-10-03Standardization of Theory (#5181)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-02Make ExtTheory independent of Theory (#5010)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback