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.

Sign up for GitHub

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

Jump to bottom

rules(minion): add modulo #460

Merged
merged 2 commits into from
Nov 17, 2024
Merged

rules(minion): add modulo #460

merged 2 commits into from
Nov 17, 2024

Conversation

niklasdewally
Copy link
Collaborator

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: #454

Closes: #456

@niklasdewally niklasdewally self-assigned this Nov 16, 2024
@niklasdewally
rules(minion): add modulo
7579a40 
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
ozgurakgun reviewed Nov 16, 2024
View reviewed changes
Copy link
Contributor

@ozgurakgun ozgurakgun left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

looks good, I just have a question about naming.

crates/conjure_core/src/ast/expressions.rs Outdated Show resolved Hide resolved
@niklasdewally
refactor(ast): Rename DivEq and ModEq
77107a0 
Rename DivEq to DivEqUndefZero and ModEq to ModulusEqUndefZero. The
latter names match more closely to the underlying Minion constraints
being used, reflecting that we are using the undefzero variants of both
@github-actions GitHub Actions
Copy link
Contributor

Code and Documentation Coverage Report

Documentation Coverage

Click to view documentation coverage for this PR 
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/conjure_macros/src/lib.rs    |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| ...m_compatability_macro/src/lib.rs |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/tree_morph/src/commands.rs   |          1 |     100.0% |          0 |       0.0% |
| crates/tree_morph/src/helpers.rs    |          0 |       0.0% |          0 |       0.0% |
| crates/tree_morph/src/lib.rs        |          1 |     100.0% |          1 |     100.0% |
| crates/tree_morph/src/reduce.rs     |          2 |     100.0% |          0 |       0.0% |
| crates/tree_morph/src/reduction.rs  |          0 |       0.0% |          0 |       0.0% |
| crates/tree_morph/src/rule.rs       |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          4 |      40.0% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/minion/src/ast.rs           |         11 |      11.0% |          0 |       0.0% |
| solvers/minion/src/error.rs         |          8 |     100.0% |          0 |       0.0% |
| solvers/minion/src/lib.rs           |          1 |     100.0% |          1 |     100.0% |
| solvers/minion/src/run.rs           |          2 |     100.0% |          1 |     100.0% |
| solvers/minion/src/wrappers.rs      |          1 |     100.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         23 |      20.5% |          2 |      11.8% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/conjure_core/src/ast/atom.rs |          1 |      33.3% |          0 |       0.0% |
| .../conjure_core/src/ast/domains.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/ast/expressions.rs |         27 |      93.1% |          0 |       0.0% |
| ...conjure_core/src/ast/literals.rs |          1 |      33.3% |          0 |       0.0% |
| crates/conjure_core/src/ast/mod.rs  |          0 |       0.0% |          0 |       0.0% |
| ...ure_core/src/ast/symbol_table.rs |          0 |       0.0% |          0 |       0.0% |
| ...es/conjure_core/src/ast/types.rs |          0 |       0.0% |          0 |       0.0% |
| ...onjure_core/src/ast/variables.rs |          1 |      50.0% |          0 |       0.0% |
| crates/conjure_core/src/bug.rs      |          1 |      50.0% |          1 |      50.0% |
| crates/conjure_core/src/context.rs  |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/error.rs    |          1 |      14.3% |          0 |       0.0% |
| crates/conjure_core/src/lib.rs      |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/metadata.rs |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/model.rs    |          3 |      17.6% |          0 |       0.0% |
| ...core/src/parse/example_models.rs |          2 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/parse/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...re_core/src/parse/parse_model.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/rule_engine/mod.rs |          5 |      71.4% |          5 |      71.4% |
| ...src/rule_engine/resolve_rules.rs |          3 |     100.0% |          0 |       0.0% |
| ..._core/src/rule_engine/rewrite.rs |          2 |      66.7% |          0 |       0.0% |
| ...ure_core/src/rule_engine/rule.rs |          3 |      25.0% |          1 |     100.0% |
| ...core/src/rule_engine/rule_set.rs |          4 |     100.0% |          0 |       0.0% |
| ...njure_core/src/rules/constant.rs |          1 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/rules/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/kissat.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/minion.rs |          1 |     100.0% |          0 |       0.0% |
| ..._core/src/solver/adaptors/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...s/conjure_core/src/solver/mod.rs |         14 |      33.3% |          1 |       4.2% |
| ...ore/src/solver/model_modifier.rs |          7 |      70.0% |          0 |       0.0% |
| ...onjure_core/src/solver/states.rs |          7 |      63.6% |          0 |       0.0% |
| ...es/conjure_core/src/stats/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...core/src/stats/rewriter_stats.rs |          1 |      20.0% |          0 |       0.0% |
| ...e_core/src/stats/solver_stats.rs |          3 |      37.5% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         91 |      42.1% |          8 |       9.8% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| conjure_oxide/src/defaults.rs       |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/find_conjure.rs   |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/lib.rs            |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/conjure.rs  |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/json.rs     |          2 |      66.7% |          0 |       0.0% |
| conjure_oxide/src/utils/misc.rs     |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/mod.rs      |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/testing.rs  |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          4 |      12.9% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/kissat/src/lib.rs           |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
Click to view documentation coverage for main 
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/conjure_macros/src/lib.rs    |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |      66.7% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| ...m_compatability_macro/src/lib.rs |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          2 |     100.0% |          1 |      50.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/tree_morph/src/commands.rs   |          1 |     100.0% |          0 |       0.0% |
| crates/tree_morph/src/helpers.rs    |          0 |       0.0% |          0 |       0.0% |
| crates/tree_morph/src/lib.rs        |          1 |     100.0% |          1 |     100.0% |
| crates/tree_morph/src/reduce.rs     |          2 |     100.0% |          0 |       0.0% |
| crates/tree_morph/src/reduction.rs  |          0 |       0.0% |          0 |       0.0% |
| crates/tree_morph/src/rule.rs       |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          4 |      40.0% |          1 |      33.3% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/kissat/src/lib.rs           |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| solvers/minion/src/ast.rs           |         11 |      11.0% |          0 |       0.0% |
| solvers/minion/src/error.rs         |          8 |     100.0% |          0 |       0.0% |
| solvers/minion/src/lib.rs           |          1 |     100.0% |          1 |     100.0% |
| solvers/minion/src/run.rs           |          2 |     100.0% |          1 |     100.0% |
| solvers/minion/src/wrappers.rs      |          1 |     100.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         23 |      20.5% |          2 |      11.8% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| crates/conjure_core/src/ast/atom.rs |          1 |      33.3% |          0 |       0.0% |
| .../conjure_core/src/ast/domains.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/ast/expressions.rs |         24 |      92.3% |          0 |       0.0% |
| ...conjure_core/src/ast/literals.rs |          1 |      33.3% |          0 |       0.0% |
| crates/conjure_core/src/ast/mod.rs  |          0 |       0.0% |          0 |       0.0% |
| ...ure_core/src/ast/symbol_table.rs |          0 |       0.0% |          0 |       0.0% |
| ...es/conjure_core/src/ast/types.rs |          0 |       0.0% |          0 |       0.0% |
| ...onjure_core/src/ast/variables.rs |          1 |      50.0% |          0 |       0.0% |
| crates/conjure_core/src/bug.rs      |          1 |      50.0% |          1 |      50.0% |
| crates/conjure_core/src/context.rs  |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/error.rs    |          1 |      14.3% |          0 |       0.0% |
| crates/conjure_core/src/lib.rs      |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/metadata.rs |          0 |       0.0% |          0 |       0.0% |
| crates/conjure_core/src/model.rs    |          3 |      17.6% |          0 |       0.0% |
| ...core/src/parse/example_models.rs |          2 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/parse/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...re_core/src/parse/parse_model.rs |          0 |       0.0% |          0 |       0.0% |
| ...jure_core/src/rule_engine/mod.rs |          5 |      71.4% |          5 |      71.4% |
| ...src/rule_engine/resolve_rules.rs |          3 |     100.0% |          0 |       0.0% |
| ..._core/src/rule_engine/rewrite.rs |          2 |      66.7% |          0 |       0.0% |
| ...ure_core/src/rule_engine/rule.rs |          3 |      25.0% |          1 |     100.0% |
| ...core/src/rule_engine/rule_set.rs |          4 |     100.0% |          0 |       0.0% |
| ...njure_core/src/rules/constant.rs |          1 |     100.0% |          0 |       0.0% |
| ...es/conjure_core/src/rules/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/kissat.rs |          1 |     100.0% |          0 |       0.0% |
| ...re/src/solver/adaptors/minion.rs |          1 |     100.0% |          0 |       0.0% |
| ..._core/src/solver/adaptors/mod.rs |          1 |     100.0% |          0 |       0.0% |
| ...s/conjure_core/src/solver/mod.rs |         14 |      33.3% |          1 |       4.2% |
| ...ore/src/solver/model_modifier.rs |          7 |      70.0% |          0 |       0.0% |
| ...onjure_core/src/solver/states.rs |          7 |      63.6% |          0 |       0.0% |
| ...es/conjure_core/src/stats/mod.rs |          0 |       0.0% |          0 |       0.0% |
| ...core/src/stats/rewriter_stats.rs |          1 |      20.0% |          0 |       0.0% |
| ...e_core/src/stats/solver_stats.rs |          3 |      37.5% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |         88 |      41.3% |          8 |       9.8% |
+-------------------------------------+------------+------------+------------+------------+
+-------------------------------------+------------+------------+------------+------------+
| File                                | Documented | Percentage |   Examples | Percentage |
+-------------------------------------+------------+------------+------------+------------+
| conjure_oxide/src/defaults.rs       |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/find_conjure.rs   |          1 |      50.0% |          0 |       0.0% |
| conjure_oxide/src/lib.rs            |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/conjure.rs  |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/json.rs     |          2 |      66.7% |          0 |       0.0% |
| conjure_oxide/src/utils/misc.rs     |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/mod.rs      |          0 |       0.0% |          0 |       0.0% |
| conjure_oxide/src/utils/testing.rs  |          0 |       0.0% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+
| Total                               |          4 |      12.9% |          0 |       0.0% |
+-------------------------------------+------------+------------+------------+------------+

Code Coverage Summary

This PR: Detailed Report

  lines......: 73.1% (3617 of 4948 lines)
  functions..: 59.2% (371 of 627 functions)
  branches...: no data found

Main: Detailed Report

  lines......: 72.8% (3517 of 4831 lines)
  functions..: 59.1% (367 of 621 functions)
  branches...: no data found

Coverage Main & PR Coverage Change

Lines coverage changed by 0.30% and covered lines changed by 100
Functions coverage changed by 0.10% and covered lines changed by 4
Branches... coverage: No comparison data available

@ozgurakgun ozgurakgun merged commit 81b2500 into conjure-cp:main Nov 17, 2024
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ozgurakgun ozgurakgun Awaiting requested review from ozgurakgun

Assignees

@niklasdewally niklasdewally

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

[eprime-minion] Implement modulo
2 participants
@niklasdewally @ozgurakgun