projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c5a7dc7) | patch
(proof-new) Improving proof-production in Equality Engine (#4871)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 12 Aug 2020 14:31:30 +0000 (11:31 -0300)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 14:31:30 +0000 (09:31 -0500)
commita852ea2c368a81c37eadccc02b3d36aec1a55c12
treea6c07d8537223a33dc317017676aa6435606691ctree
parentc5a7dc772788ea3f1d568da0d8ef4effca080b9ccommit | diff
(proof-new) Improving proof-production in Equality Engine (#4871)

This commit improves functionalities of the equality engine so that it is easier to produce proofs for its reasoning. They are:

avoiding assertion of already entailed predicates/equalities.
better EqProof of disequalities with constants
correct EqProof involving n-ary congruence kinds
src/theory/uf/equality_engine.cpp diff | blob | history
src/theory/uf/equality_engine.h diff | blob | history