projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 482df8b) | patch
Care graphs based on polymorphic operators in strings (#4150)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 26 Mar 2020 06:38:08 +0000 (01:38 -0500)
committerGitHub <noreply@github.com>
Thu, 26 Mar 2020 06:38:08 +0000 (23:38 -0700)
commite7edc09b227af1f58573cf5a636a91674dc2d936
tree91e2e2cc0006d58a420464e2a373f7e139cd3a5ftree
parent482df8bb2914d9c470ab8dd290bf6abe590505c6commit | diff
Care graphs based on polymorphic operators in strings (#4150)

Towards theory of sequences.

To compute a care graphs, we need to group function applications by the string type they are associated with. This PR introduces a utility to function to get the "owning string type" for a function application, and updates the care graph computation so that it partitions function applications according to this type.
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_utils.cpp diff | blob | history
src/theory/strings/theory_strings_utils.h diff | blob | history