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

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

2021-01-08	mudathirmahgoub	Rename getAntecedent to getPremises (#5754)	blob \| commitdiff \| raw
2020-12-11	Andrew Reynolds	Fix length assumption for deq norm emp rule (#5623)	blob \| commitdiff \| raw \| diff to current
2020-12-10	Gereon Kremer	Fixed a bunch of clang warnings. (#5637)	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-09-22	Mathias Preiner	Update copyright header script to support CMake and...	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-02	Andres Noetzli	Ensure strict length constraint for decompose rule...	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-01	Andrew Reynolds	Inferences and model construction taking into account...	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	Cardinality-related inferences per type in theory of...	blob \| commitdiff \| raw \| diff to current
2020-05-26	Andrew Reynolds	(proof-new) Updates to strings skolem cache. (#4524)	blob \| commitdiff \| raw \| diff to current
2020-05-20	Andrew Reynolds	Normal form equality conflicts and uniqueness check...	blob \| commitdiff \| raw \| diff to current
2020-04-22	Andrew Reynolds	Ensure disequality splits are processed as lemmas ...	blob \| commitdiff \| raw \| diff to current
2020-04-20	Andrew Reynolds	Refactor inference manager in strings to be amenable...	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	Explain non-emptiness by non-zero length in strings...	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-06	Andres Noetzli	Refactor disequality processing in string solver (...	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andrew Reynolds	Split sequences rewriter (#4194)	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	Generalize more string-specific functions (#4152)	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-21	Andres Noetzli	Simplify heuristic in `processNEqc` (#4129)	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-13	Andrew Reynolds	Removing a few deprecated options (#4052)	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-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-02-16	Andres Noetzli	Activate reverse variant of F-Split inference (#3745)	blob \| commitdiff \| raw \| diff to current
2020-02-11	Andres Noetzli	Remove `--strings-binary-csp` option (#3743)	blob \| commitdiff \| raw \| diff to current
2020-02-11	Andres Noetzli	Refactor `CoreSolver::processSimpleNEq()` (#3736)	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

RSS Atom