Reconsider `Ord` trait on `BddValuation`

[daemontus]

Right now, this is a "derived" trait implementation. But this may be slightly unintuitive, because it is just a "lexicographic" ordering. On surface, this is reasonable because it follows the normal iteration order. But there are a few considerations to be made:

• Is this even useful? Do we expect people to compare valuations like this?
• Should ordering fail on incompatible valuations? (i.e. different variable count).
• Shouldn't there rather be a PartialOrd between BDD valuations and partial valuations that is instead based on "inclusion"? Wouldn't this be a more natural ordering on valuations?

[daemontus]

Just a quick note that the earliest point where we can safely change this is the 1.0.0 version, since this would be a breaking change.

[zao111222333]

Hi, in this time can we directly add derived PartialOrd to Bdd and BddNode?

I understand this implementation mightly be useless and confused for most of people... But here is one scenarios when I want to sort some BooleanExpression according their Bdd. I don't care the sorting metric, just clustering the same logic as near as possible. (e.g., A&B, B&A should be close to each other and far from A&!B).

Thank you!

[daemontus]

Hi! Sorry for the late response.

I am a bit reluctant to add an ordering to BDDs directly, since this could be interpreted in many different ways. For example, one could order BDDs by size (in terms of nodes), one could order them by the number of positive results the function gives (function weight/cardinality), one could order them by implication (i.e. A <= B if A implies B), etc. There really isn't a one true "normal" ordering.

However, I see your point. Since Rust supports Vec::sort_by, I would propose the following:

Add a collection of pre-made sorting methods that can be used with sort_by in various scenarios. Some of these would be total, while some can be only partial. So you could use vec.sort_by(Bdd::size_sort), vec.sort_by(Bdd::cardinality_sort), vec.sort_by(Bdd::structural_sort) (your suggestion), and vec.sort_by(Bdd::implication_sort), etc.

Would this work for you?

[daemontus]

I've added the comparator methods here as Bdd::cmp_*: https://github.com/sybila/biodivine-lib-bdd/commit/932984c487969a29acd5e1c91a2126dac7c8f1a5

This is now included in the library since version 0.5.18.

[zao111222333]

Hi! Thank you a lot for your help!

I've used the Bdd::cmp_* to my cases, it is a very useful API (especially Bdd::cmp_structural for me). I know it's a hard work to implement so many ways to do comparsion. Thank you!