projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d4c7b0b) | patch
Cardinality-related inferences per type in theory of strings (#4585)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 12 Jun 2020 13:07:47 +0000 (08:07 -0500)
committerGitHub <noreply@github.com>
Fri, 12 Jun 2020 13:07:47 +0000 (08:07 -0500)
commit3c733d68aabc1c90b4f0f8a3e7a6a25f24896744
treec621a56c021757e391fff471e71caf635ef95aeatree
parentd4c7b0b250a419ec149f973abcb1c1bf3886cef3commit | diff
Cardinality-related inferences per type in theory of strings (#4585)

Towards theory of sequences.

This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type.
src/theory/strings/base_solver.cpp diff | blob | history
src/theory/strings/base_solver.h diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/solver_state.cpp diff | blob | history
src/theory/strings/solver_state.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history