niklasdewally commented 6 days ago

Ready to merge version of #450.

Add generic Minion flattening rules, and implement flattening for division.

These rules will be key to converting nested expressions to auxiliary variables for use with Minion. This PR only implements them for division, but they will apply trivially to any binary or vector operator.

Unlike previous attempts, flattening is now encoded in the type system (as enabled by f931a3d2b407c5f295e7eab181d53bd26a32c6aa). In this patch DivEq has the type DivEq(Metadata,Factor,Factor,Factor).

The following related bug-fixes were necessary to implement this:

Fix the rewriter not updating the next_var counter, breaking model.gensym().

Previously, we updated the model by extending the symbol table with the one returned by the rule application. This did not update the gensym() counter. This patch adds a method, model.extend_sym_table, to reconcile the gensym counter with machine names added by rules.
Make expressions bubble inside-out, and forbid making a bubble inside a bubble. This is a non-functional change, but the hope is that this will make execution order more predictable, and reduce the number of steps needed to rewrite bubbled expressions. See #450.
Fix domain of SafeDiv expressions to include 0. This is what I think the big bug was.
Do not allow putting an unsafe expression in an aux var. Unsafe expressions need to be bubbled up to the nearest boolean context. Putting them in an auxiliary variable moves them out of their boolean context to the top level of the model. I am unsure whether this was causing issues or not, but this seems like the right thing to do.

See #450.

Flattening approach

Flattening is the conversion between nested expressions to non nestedexpressions through the creation of auxiliary variables. For example:

(y/(x/z)) ~> y/a where a = x/z

Most solvers, including Minion, only support flattened constraints.

Unlike previous flattening code, here I choose to flatten expressions "inside out". This choice allows us to assume that diveq constraints are always flat.

Outside-in flattening looks like so:

y/(x/z) = a ~> diveq(y,(x/z),a) ~> diveq(y,b,a) , b = x/z

In the first line, diveq is non flat, which is a semantically invalid model. Flattening inside-out ensures that our model stays semantically valid after the application of every rule.

This means that we apply the rules that turn expressions into their "constraint" form when their arguments are flat.

This evaluation order also keeps things as solver independent arithmetic expressions (e.g. safediv) rather than lower-level constraints (e.g. diveq) for longer. This will allow solver-independent rules and optimisations, which use arithmetic expressions, to be applicable for longer.

I also, arbitrarily, choose to flatten after undefinedness and bubbles have been resolved: i.e. I flatten SafeDivs but not UnsafeDivs.

Flattening Rules

My rules for flattening are generic and will be applicable to all arithmetic binary operators (flatten_binop) and arithmetic vector operators (flatten_vecop).

To flatten an operator, it will need to be added to the above rules' allow lists and will need a rule to turn it into a lower-level flat constraint. In the case of division, this is introduce_diveq.

A special case is flattening equalities. We only need to flatten an equality if both sides are not flat. Note that this rule applies for equality only and we currently treat != as a standard binary operator.

``` +-------------------------------------+------------+------------+------------+------------+ | 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 | +-------------------------------------+------------+------------+------------+------------+ | .../conjure_core/src/ast/domains.rs | 0 | 0.0% | 0 | 0.0% | | ...jure_core/src/ast/expressions.rs | 24 | 92.3% | 0 | 0.0% | | ...s/conjure_core/src/ast/factor.rs | 1 | 33.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% | +-------------------------------------+------------+------------+------------+------------+ ```

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/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 | +-------------------------------------+------------+------------+------------+------------+ | .../conjure_core/src/ast/domains.rs | 0 | 0.0% | 0 | 0.0% | | ...jure_core/src/ast/expressions.rs | 24 | 92.3% | 0 | 0.0% | | ...s/conjure_core/src/ast/factor.rs | 1 | 33.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 | 2 | 12.5% | 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 | 87 | 41.0% | 8 | 9.9% | +-------------------------------------+------------+------------+------------+------------+ +-------------------------------------+------------+------------+------------+------------+ | 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% | +-------------------------------------+------------+------------+------------+------------+ ```

Code Coverage Summary

This PR: Detailed Report

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

Main: Detailed Report

  lines......: 72.5% (3455 of 4764 lines)
  functions..: 58.8% (359 of 611 functions)
  branches...: no data found

Coverage Main & PR Coverage Change

Lines coverage changed by 0.30% and covered lines changed by 67
Functions coverage changed by 0.30% and covered lines changed by 8
Branches... coverage: No comparison data available

niklasdewally commented 6 days ago

@ozgurakgun ok to merge?

conjure-cp / conjure-oxide

rules(minion): add flattening rules for division #454

Flattening approach

Flattening Rules

See also

450 for more details on changes to bubbling made in order to fix

Code and Documentation Coverage Report

Documentation Coverage

Code Coverage Summary

Coverage Main & PR Coverage Change