projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: dab7f46) | patch
Changing the way the equality engine explains disequalities.
authorguykatzz <katz911@gmail.com>
Sat, 6 Feb 2016 00:10:36 +0000 (16:10 -0800)
committerguykatzz <katz911@gmail.com>
Sat, 6 Feb 2016 00:10:36 +0000 (16:10 -0800)
commit3c4c4420ebae4d27d53084453591363942eb4d2e
treeade8c2bc56a3900911c987d8708be9db675b9446tree
parentdab7f460511bf0f36c286eaf456a4be11f4fea4bcommit | diff
Changing the way the equality engine explains disequalities.

The explanation for a != b is now:
1. a == find(a)
2. ( find(a) == find(b) ) == false
3. find(b) == b

This simplifies the creation of transitivity proofs for disequalities.
src/theory/uf/equality_engine.cpp diff | blob | history