Simplify equalities using their domains

[niklasdewally]

Description

Implement simplifier rules for = and != based on the domains of their arguments:

• a = b ~> false if domain(a) ∩ domain(b) = {} (the domains of a and b are completely different)

• a != b ~> true if domain(a) ∩ domain(b) = {}

• Do the != case pairwise for an allDiff.

For example, for test mod_undefzero-04-nested-neq, Savile Row does:

Model before undef handling:
language ESSENCE' 1.0
find x : int(5..7)
find y : int(0..3)
find z : int(0..4)
such that
((x%((y%z)))!=3)
Rule:savilerow.TransformMakeSafe
Model has changed. Model after rule application:
language ESSENCE' 1.0
find x : int(5..7)
find y : int(0..3)
find z : int(0..4)
such that
((z != 0) /\ ((((y%z)) != 0) /\ ((x%((y%z)))!=3)))
Model after rule application and simplify:
language ESSENCE' 1.0
find x : int(5..7)
find y : int(0..3)
find z : int(0..4)
such that
(z != 0),
((y%z) != 0)

To do this well, we need the notion of a category, and to cache an expressions category, domain, and type inside its Metadata.

Features

• [x] #459
• [ ] Implement categories andExpression::category_of.
• [ ] Memoise an expressions category and domain inside Metadata.
• [ ] Implement simplifiers for a=b and a!=b based on the domains of the arguments.
• Implement an alldiff simplifier based on the domains of the arguments.
• [ ] Refactor rule checks in rules::utils to use categories where possible.

CC: @ozgurakgun

[niklasdewally]

don't feel like you have to do this in this PR, in fact you probably shouldn't, but we should first have:

an optional type (this already exists) an optional domain an optional category in the metadata.

we would store the int domain for all Atomic entries, and calculate the domain for all composite expressions.

we can look into how SR calculates bounds to work out the domains. for example for mod and div.

once we calculate the domain of both sides of !=, a rule (maybe the partial eval) should rewrite that expr to true

note: SR's getBounds returns an IntPair but we should maintain a Domain since we will have more kinds of domains, not just ints.

(@ozgurakgun in #456)

[ozgurakgun]

You might want to divorce the alldif one from this plan to make it a bit more manageable. Also remember SR's simplifications for all diff, there is more you can do like pigeonhole analysis: count the number of values and variables you have in the alldiff etc.

The rest sounds good to me!

[niklasdewally]

CC: @YehorBoiar @lixitrixi

Having a way to invalidate fields in metadata might affect your current rewriter engine work?

Not sure what you have already, but for example you could call an empty method called Expression::invalidate() / Metadata::invalidate() when an expression has changed, and then whoever takes this on can fill in the memoization logic later?

[lixitrixi]

a = b ~> true if domain(a) / domain(b) = {} (the domains of a and b are identical)

I may be misunderstanding but this seems to only hold when the domains additionally contain just one element? A and B having the same domains doesn't mean they are always equal!

What would make more sense: a = b ~> true if domain(a) / domain(b) = {} and |domain(a)| = 1

The second one makes sense to me; you could also write an = ~> false version of it.

[niklasdewally]

What would make more sense: a = b ~> true if domain(a) / domain(b) = {} and |domain(a)| = 1

The second one makes sense to me; you could also write an = ~> false version of it.

Oops! Checked Savile Row, and it should be a = b ~> false if domain(a) ∩ domain(b) = {}

I've edited the issue