projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 63905da) | patch
(proof-new) Add the proof equality engine (#4881)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Aug 2020 20:04:03 +0000 (15:04 -0500)
committerGitHub <noreply@github.com>
Thu, 27 Aug 2020 20:04:03 +0000 (15:04 -0500)
commit4adff162770a841d136ec44146928c2296eaf1b2
tree8da07340688f598a4d5a6c7af94df85685112c08tree
parent63905da0f55f99dfc1f4ab40a1ce61d3e7d58ce1commit | diff
(proof-new) Add the proof equality engine (#4881)

This is a (partial) layer on top of EqualityEngine that is a universal black box proof generator for users of the equality engine.
src/CMakeLists.txt diff | blob | history
src/theory/uf/proof_equality_engine.cpp [new file with mode: 0644] blob
src/theory/uf/proof_equality_engine.h [new file with mode: 0644] blob