projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8f7952b) | patch
Update care graph computations to use standard node trie algorithm (#8298)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 17 Mar 2022 18:56:15 +0000 (13:56 -0500)
committerGitHub <noreply@github.com>
Thu, 17 Mar 2022 18:56:15 +0000 (18:56 +0000)
commit93160e9f24c78b68d3c2b523cd11a2f71acd77e4
tree1c194d11b805c7d1c3db8f80c4359397c7646cddtree
parent8f7952bc092d252a4d0c04c87636c443536833b3commit | diff
Update care graph computations to use standard node trie algorithm (#8298)

Standardizes a few new methods in theory to support this.

This should not change the behavior, only refactors.

This is in preparation for adding efficient care graph computation for bags, and towards possible fixes for arrays.
15 files changed:
src/CMakeLists.txt diff | blob | history
src/theory/care_pair_argument_callback.cpp [new file with mode: 0644] blob
src/theory/care_pair_argument_callback.h [new file with mode: 0644] blob
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets.h diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/theory.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history