feat: FastSetUnification

[JonathanStarup]

Including fuzzer

[magnus-madsen]

What's the plan for polish? I think it makes sense to do a thorough pass through the code before I look at it in detail.

[JonathanStarup]

Yeah ill give it a full look over and ping you

[magnus-madsen]

Yeah ill give it a full look over and ping you

Ok. Since this is a such a central piece of what we do, I have a high standard :)

It would be good to ensure all comments are up to date and that the code is as clean as possible.

[magnus-madsen]

I will add general comments before code-level comments:

• Test cases do not seem to contain elements.
• I am not sure I like SetEval it seems like an extra level of abstraction. At least it should not be written in OO-style.
• Why does Term suddenly have both & and inter? How many ways do we know have to construct terms? :)
• What is freeUnknowns?
• toRawString ugh? Maybe some of this can be moved to a debugging class.
• I still don't understand why Inter is defined the way it is with an option. It seems very asymmetric.

[JonathanStarup]

• Test cases do not seem to contain elements.
  • The fuzzed tests do. Do you want me to extract examples for std lib?
• I am not sure I like SetEval it seems like an extra level of abstraction. At least it should not be written in OO-style.
  • I've changed it to func style.
  • I like that we don't have to know the universe. and its just 20 lines (excluding comments)
• Why does Term suddenly have both & and inter? How many ways do we know have to construct terms? :)
  • Oversigt, its simplified now
• What is freeUnknowns?
  • Constants and variables. Before we called flexify that converted csts to vars. instead evaluate now just views constants like that to begin with, saving a formula conversion
• toRawString ugh? Maybe some of this can be moved to a debugging class.
  • Moved to the fuzzer. We can also delete it, it was just useful for debugging.
• I still don't understand why Inter is defined the way it is with an option. It seems very asymmetric.
  • {e_12} ∩ {e_42} = empty so structurally we reflected that. union doesn't behave like that so it is asymmetric. I can also make it a zero/singleton set if you want.

[JonathanStarup]

@magnus-madsen ive given it all a read-through and rewrite but it probably requires multiple, being so long.

[magnus-madsen]

• Test cases do not seem to contain elements.

  * The fuzzed tests do. Do you want me to extract examples for std lib?
  

Yes, definitely. This would be very useful.

  * Constants and variables. Before we called flexify that converted csts to vars. instead evaluate now just views constants like that to begin with, saving a formula conversion

Do we assume the domains are disjoint?

  * `{e_12} ∩ {e_42} = empty` so structurally we reflected that. union doesn't behave like that so it is asymmetric. I can also make it a zero/singleton set if you want.

But what about {throw, print} ∩ ef. Why is that not allowed to have a compact representation?

[JonathanStarup]

Do we assume the domains are disjoint?

That was already assumed, noted in FastBoolUnification

Yes, definitely. This would be very useful.

It is less cool since we don't use minus yet, but I can find some examples

But what about {throw, print} ∩ ef. Why is that not allowed to have a compact representation?

we can/should do it for sure, but it adds extra logic in many of the functions. i think it be better not to make this PR larger

[magnus-madsen]

It is less cool since we don't use minus yet, but I can find some examples

Regions should be their own effects. Then there is plenty to take from.

[magnus-madsen]

we can/should do it for sure, but it adds extra logic in many of the functions. i think it be better not to make this PR larger

Since there is no dependency on this PR, I suggest we iterate as much as needed.

[JonathanStarup]

Compact concrete sets:

1. We could change the element part of an intersection to represent a union
   a. This means that the most compact element rep is an intersection and that {a} u {b} should simplify to Inter({a, b}, empty...)
   b. This allows simplifying fx ({a} u {b}) inter ({b} u {c}) since it becomes a nested intersection
2. We could change Elem(Int) to ElemSet(Set[Int])
   a. both union and intersection will just have zero/one element set
   b. The most compact element rep is an element set

I think the second is the most comprehensible, do you have a comment @magnus-madsen?

[magnus-madsen]

@JonathanStarup Can we do both?

[JonathanStarup]

both? doesnt that just give inconsistent representation?

[JonathanStarup]

Efficient really is the enemy of elegant

[magnus-madsen]

We should definitely do (2) then we can fight over (1).