diff options
| author | guykatzz <katz911@gmail.com> | 2016-02-05 16:10:36 -0800 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2016-02-05 16:10:36 -0800 |
| commit | 3c4c4420ebae4d27d53084453591363942eb4d2e (patch) | |
| tree | ade8c2bc56a3900911c987d8708be9db675b9446 /src/theory/theory_model.h | |
| parent | dab7f460511bf0f36c286eaf456a4be11f4fea4b (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.
Diffstat (limited to 'src/theory/theory_model.h')
0 files changed, 0 insertions, 0 deletions