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

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

2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	blob \| commitdiff \| raw
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	blob \| commitdiff \| raw \| diff to current
2021-03-29	Andrew Reynolds	Move decision manager into theory inference manager...	blob \| commitdiff \| raw \| diff to current
2021-03-21	Andrew Reynolds	Simplify strings term registration (#6174)	blob \| commitdiff \| raw \| diff to current
2021-03-20	Andrew Reynolds	Improved tracing for equivalence classes of EE (#6169)	blob \| commitdiff \| raw \| diff to current
2021-03-16	Andrew Reynolds	Further standardization of strings statistics (#6128)	blob \| commitdiff \| raw \| diff to current
2021-03-11	Andrew Reynolds	(proof-new) Clean up uses of witness with skolem lemmas...	blob \| commitdiff \| raw \| diff to current
2021-03-10	Andrew Reynolds	(proof-new) Update ppRewrite to use skolem lemmas ...	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-03-02	Gereon Kremer	Clean up includes to reduce compile times (#6031)	blob \| commitdiff \| raw \| diff to current
2021-02-11	Gereon Kremer	Add InferenceId member to TheoryInference, adapt all...	blob \| commitdiff \| raw \| diff to current
2021-02-11	Gereon Kremer	Merge InferenceIds into one enum (#5892)	blob \| commitdiff \| raw \| diff to current
2021-02-08	Andrew Reynolds	Avoid spurious traversal of terms during preregistratio...	blob \| commitdiff \| raw \| diff to current
2021-01-15	Andrew Reynolds	Implement --no-strings-lazy-pp as a preprocessing pass...	blob \| commitdiff \| raw \| diff to current
2021-01-13	Andrew Reynolds	Split eager solver from strings solver state (#5775)	blob \| commitdiff \| raw \| diff to current
2021-01-08	mudathirmahgoub	Rename getAntecedent to getPremises (#5754)	blob \| commitdiff \| raw \| diff to current
2020-12-23	Andrew Reynolds	(proof-new) Miscelleneous fixes from proof-new (#5714)	blob \| commitdiff \| raw \| diff to current
2020-12-08	Andrew Reynolds	Proper implementation of expand definitions for sequenc...	blob \| commitdiff \| raw \| diff to current
2020-12-08	Andrew Reynolds	Fix collect model values for sequences of sequences...	blob \| commitdiff \| raw \| diff to current
2020-12-07	Andrew Reynolds	Do not expand theory definitions at the beginning of...	blob \| commitdiff \| raw \| diff to current
2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-11-30	Andrew Reynolds	(proof-new) Proofs for regular expression elimination...	blob \| commitdiff \| raw \| diff to current
2020-11-04	Andres Noetzli	Add constants from equality engine evaluation to model...	blob \| commitdiff \| raw \| diff to current
2020-10-29	Andrew Reynolds	(proof-new) Update the strings inference manager for...	blob \| commitdiff \| raw \| diff to current
2020-10-20	yoni206	Expand `seq.nth` lazily (#5287)	blob \| commitdiff \| raw \| diff to current
2020-10-03	Andrew Reynolds	Standardization of Theory (#5181)	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	Make ExtTheory independent of Theory (#5010)	blob \| commitdiff \| raw \| diff to current
2020-08-31	Andrew Reynolds	(new theory) Update TheoryStrings to new standard ...	blob \| commitdiff \| raw \| diff to current
2020-08-31	Andrew Reynolds	Simplify interface for computing relevant terms. (...	blob \| commitdiff \| raw \| diff to current
2020-08-24	Andrew Reynolds	Extend the standard Theory template based on equality...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Remove spurious theory methods calls (#4931)	blob \| commitdiff \| raw \| diff to current
2020-08-19	Andrew Reynolds	Make sets and strings solver states inherit from Theory...	blob \| commitdiff \| raw \| diff to current
2020-08-19	Gereon Kremer	Changes assertion (about maximum set cardinality) to...	blob \| commitdiff \| raw \| diff to current
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	blob \| commitdiff \| raw \| diff to current
2020-08-17	Andrew Reynolds	(proof-new) Prepare the theory of strings for proof...	blob \| commitdiff \| raw \| diff to current
2020-08-15	Andrew Reynolds	(proof-new) Add the strings proof checker (#4858)	blob \| commitdiff \| raw \| diff to current
2020-08-09	Andrew Reynolds	Make valuation class more robust to null underlying...	blob \| commitdiff \| raw \| diff to current
2020-08-06	Andrew Reynolds	(proof-new) Refactor regular expression operation ...	blob \| commitdiff \| raw \| diff to current
2020-08-05	Andres Noetzli	[Strings] Add eager context-dependent evaluation (...	blob \| commitdiff \| raw \| diff to current
2020-07-28	yoni206	Supporting seq.nth (#4723)	blob \| commitdiff \| raw \| diff to current
2020-07-17	Andrew Reynolds	(proof-new) Updates to strings core solver (#4642)	blob \| commitdiff \| raw \| diff to current
2020-07-16	Andrew Reynolds	Make ExtTheory a utility and not a member of Theory...	blob \| commitdiff \| raw \| diff to current
2020-07-13	Andrew Reynolds	Add support for string/sequence update (#4725)	blob \| commitdiff \| raw \| diff to current
2020-07-11	Andrew Reynolds	(proof-new) Update Theory interface for proof-new ...	blob \| commitdiff \| raw \| diff to current
2020-07-01	Andrew Reynolds	Inferences and model construction taking into account...	blob \| commitdiff \| raw \| diff to current
2020-06-19	Andrew Reynolds	(proof-new) Updates to strings term registry (#4599)	blob \| commitdiff \| raw \| diff to current
2020-06-19	Andrew Reynolds	Clean the header file of TheoryStrings (#4272)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-12	Andrew Reynolds	(proof-new) Minor updates to strings base solver (...	blob \| commitdiff \| raw \| diff to current
2020-06-12	Andrew Reynolds	Cardinality-related inferences per type in theory of...	blob \| commitdiff \| raw \| diff to current
2020-06-10	Andres Noetzli	Add support for str.replace_re/str.replace_re_all ...	blob \| commitdiff \| raw \| diff to current
2020-05-22	Andrew Reynolds	(proof-new) Minor update to strings solver state (...	blob \| commitdiff \| raw \| diff to current
2020-05-20	Andrew Reynolds	Do not eliminate variables that are equal to unevaluata...	blob \| commitdiff \| raw \| diff to current
2020-05-19	mudathirmahgoub	Renamed operator CHOICE to WITNESS (#4207)	blob \| commitdiff \| raw \| diff to current
2020-04-28	Andrew Reynolds	Update cardinality in strings to unicode standard ...	blob \| commitdiff \| raw \| diff to current
2020-04-16	Andrew Reynolds	Eliminate remaining references to parent TheoryStrings...	blob \| commitdiff \| raw \| diff to current
2020-04-15	Andrew Reynolds	Split TermRegistry object from TheoryStrings (#4312)	blob \| commitdiff \| raw \| diff to current
2020-04-10	Andrew Reynolds	Add a few stats to strings (#4252)	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-04-07	Andrew Reynolds	Enum for all remaining string inferences (#4220)	blob \| commitdiff \| raw \| diff to current
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
next

RSS Atom