projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fb5e311) | patch
TheoryIds for UF theory. (#5901)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 17 Feb 2021 15:10:43 +0000 (16:10 +0100)
committerGitHub <noreply@github.com>
Wed, 17 Feb 2021 15:10:43 +0000 (16:10 +0100)
commitf52cd17ba0f9c455db1d45341ba39f04b319e621
treef74b8241764dc2d7ecfc026ba60516b5211dc701tree
parentfb5e3113312322c21a00062b22c358c30fa27101commit | diff
TheoryIds for UF theory. (#5901)

This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/uf/cardinality_extension.cpp diff | blob | history
src/theory/uf/ho_extension.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history