[eprime-minion] Implement modulo

[niklasdewally]

Summary

Implement modulo operator and convert it to Minion. As with all other Minion rules, constraints targeting mod specifically should be provided in minion_constraints. These should include tests for neq, negated eq, and nested constraints.

I imagine that this will work similarly to division (#454), and similar test cases could be used.

Tasks

• [ ] Add UnsafeMod, and bubbling rules to convert this to SafeMod.
• [ ] Parse UnsafeMod
• [ ] Add SafeMod flattening rules

Questions

• What the undefinedness semantics of modulo? Are these the same as division? @ozgurakgun

[ozgurakgun]

Should be identical to div, yes.

[niklasdewally]

@ozgurakgun should savilerow and conjure have the same modulo semantics? If not, which should I follow?

For these models, conjure and savile row give drastically different numbers of solutions:

(conjure: 21 solutions, savilerow 7)

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

(conjure: 60 solutions, savilerow: 1)

language ESSENCE' 1.0

find x : int(5..7)
find y : int(0..3)
find z : int(0..4)

$ variation on 04

such that !(x % (y%z) = 3)

[niklasdewally]

Conjure and Savilerow agree on the div tests that these were based on.

[niklasdewally]

Ignore the above: they agree with -S0!

[ozgurakgun]

I was about to ask what options you are passing, because Conjure basically just passes these through. Stick to -S0 indeed.

[ozgurakgun]

conjure solve -v prints the SR command it runs (among other things) which might be useful.