diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 05:44:13 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-27 05:44:13 +0000 |
| commit | b390cfa8f095048472cb3dd0b9ccc22fbd51f411 (patch) | |
| tree | de6d485b9b164806f408d714cd50e7da7db5da6c /src/theory/booleans | |
| parent | 28096861af9b01e4bad6059346446d97b9708cb7 (diff) | |
Committing the work on equality engine, I need to see how it does on the regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes
Diffstat (limited to 'src/theory/booleans')
0 files changed, 0 insertions, 0 deletions