Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[eprime-minion] Implement modulo #456

Closed
3 tasks done
Tracked by #171
niklasdewally opened this issue Nov 16, 2024 · 9 comments · Fixed by #460
Closed
3 tasks done
Tracked by #171

[eprime-minion] Implement modulo #456

niklasdewally opened this issue Nov 16, 2024 · 9 comments · Fixed by #460
Assignees

Comments

@niklasdewally
Copy link
Collaborator

niklasdewally commented Nov 16, 2024

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
@niklasdewally niklasdewally changed the title modulo_undefzero Modulo Rules Nov 16, 2024
@niklasdewally niklasdewally self-assigned this Nov 16, 2024
@niklasdewally niklasdewally changed the title Modulo Rules [eprime-minion support] Implement modulo Nov 16, 2024
@niklasdewally niklasdewally changed the title [eprime-minion support] Implement modulo [eprime-minion] Implement modulo Nov 16, 2024
@ozgurakgun
Copy link
Contributor

Should be identical to div, yes.

@niklasdewally
Copy link
Collaborator Author

@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
Copy link
Collaborator Author

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

@niklasdewally
Copy link
Collaborator Author

niklasdewally commented Nov 16, 2024

Ignore the above: they agree with -S0!

@ozgurakgun
Copy link
Contributor

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

@ozgurakgun
Copy link
Contributor

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

@niklasdewally
Copy link
Collaborator Author

niklasdewally commented Nov 16, 2024

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)

Is the simplifcation here to rewrite not equals expressions where the lhs and rhs domains are disjoint to true?

niklasdewally added a commit to niklasdewally/conjure-oxide that referenced this issue Nov 16, 2024
Add modulo expressions, parsing, and conversion rules to Minion.

The undefinedness semantics for modulo are similar to those for
division: it requires a bubble rule, asserting that for x % y, y!=0, to
make it safe.

Due to their similarity, the test cases for modulo in this patch are
based on the division ones.

See also: conjure-cp#454

Closes: conjure-cp#456
niklasdewally added a commit to niklasdewally/conjure-oxide that referenced this issue Nov 16, 2024
Add modulo expressions, parsing, and conversion rules to Minion.

The undefinedness semantics for modulo are similar to those for
division: it requires a bubble rule, asserting that for x % y, y!=0, to
make it safe.

Due to their similarity, the test cases for modulo in this patch are
based on the division ones.

See also: conjure-cp#454 (implementation of division rules)

Closes: conjure-cp#456
niklasdewally added a commit to niklasdewally/conjure-oxide that referenced this issue Nov 16, 2024
Add modulo expressions, parsing, and conversion rules to Minion.

The undefinedness semantics for modulo are similar to those for
division: it requires a bubble rule, asserting that for x % y, y!=0, to
make it safe.

Due to their similarity, the test cases for modulo in this patch are
based on the division ones.

See also: conjure-cp#454 (implementation of division rules)

Closes: conjure-cp#456
niklasdewally added a commit to niklasdewally/conjure-oxide that referenced this issue Nov 16, 2024
Add modulo expressions, parsing, and conversion rules to Minion.

The undefinedness semantics for modulo are similar to those for
division: it requires a bubble rule, asserting that for x % y, y!=0, to
make it safe.

Due to their similarity, the test cases for modulo in this patch are
based on the division ones.

See also: conjure-cp#454 (implementation of division rules)

Closes: conjure-cp#456
niklasdewally added a commit to niklasdewally/conjure-oxide that referenced this issue Nov 16, 2024
Add modulo expressions, parsing, and conversion rules to Minion.

The undefinedness semantics for modulo are similar to those for
division: it requires a bubble rule, asserting that for x % y, y!=0, to
make it safe.

Due to their similarity, the test cases for modulo in this patch are
based on the division ones.

See also: conjure-cp#454 (implementation of division rules)

Closes: conjure-cp#456
@ozgurakgun
Copy link
Contributor

ozgurakgun commented Nov 16, 2024

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.

@niklasdewally
Copy link
Collaborator Author

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.

captured this in #461

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants