projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ba30b69) | patch
Add InferenceIds for sets theory. (#5900)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 18 Feb 2021 21:33:10 +0000 (22:33 +0100)
committerGitHub <noreply@github.com>
Thu, 18 Feb 2021 21:33:10 +0000 (22:33 +0100)
commit94fdbe4bb325b1ff1874a2e699cad6ea76f44185
tree1927e234fb4a59899ceac0aa3920f52e62bbb6abtree
parentba30b690b29e7e52dd8ea1ea953525c401abf3d9commit | diff
Add InferenceIds for sets theory. (#5900)

This PR introduces new InferenceId for the theory of sets 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/sets/cardinality_extension.cpp diff | blob | history
src/theory/sets/inference_manager.cpp diff | blob | history
src/theory/sets/inference_manager.h diff | blob | history
src/theory/sets/term_registry.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_rels.cpp diff | blob | history
src/theory/sets/theory_sets_rels.h diff | blob | history