projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e4e19cd) | patch
Enable default equality proofs for sets (#6931)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 26 Jul 2021 21:03:48 +0000 (16:03 -0500)
committerGitHub <noreply@github.com>
Mon, 26 Jul 2021 21:03:48 +0000 (21:03 +0000)
commit9a098337f9f25e7e2df07e493e6a120f6b8ce520
tree8953168e00fd442e350ab9af1fec2564f3cb70b0tree
parente4e19cd62b3eebed2de5b9b627509df0ffec23e1commit | diff
Enable default equality proofs for sets (#6931)

This enables default support for equality proofs in the theory of sets.

This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.
src/proof/proof_rule.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/sets/inference_manager.cpp diff | blob | history
src/theory/sets/inference_manager.h diff | blob | history
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/theory_inference_manager.cpp diff | blob | history
src/theory/theory_inference_manager.h diff | blob | history