Help wanted: flattening negated nested divisions

[niklasdewally]

The purpose of this PR is to get feedback on my ongoing work on flattening nested divs and to debug a failing testcase.

The test case in question is div_undefzero-05-nested-noteq, which is defined as:

find x : int(5..20)
find y : int(0..5)
find z : int(0..6)

such that !(x / (y/z) = 10)

This PR is completed in #454

[niklasdewally]

@ozgurakgun what are the undefinedness semantics of (a/y !=z)?

The existing div_to_bubble rule seems to be trying to do

Not(Neq(UnsafeDiv(x,y),z)) 
~> Not(And[Neq(SafeDiv(x,y),z), Neq(y,0)]) 
~> And[Eq(SafeDiv(x,y),z),Eq(y,0)]

which might be wrong?

This is causing div_undefzero-05-nested-noteq to fail.

[niklasdewally]

I have made to_aux_var fail when it has an undefined thing inside it so that we don't bring something to the top that should've been bubbled; but this doesn't make a difference...

[niklasdewally]

div-05, which does (a!= b/c), works as expected, so it might be more to do with double negations?

I know that its probably not my flattening rules doing it, so I'm a bit stuck...

[niklasdewally]

Rule applicable: negated_neq_to_eq ([("Base", 8800)]), to expression: Not((SafeDiv(y, z) != 0)), resulting in: (SafeDiv(y, z) = 0) new_top=And([])

This is weird....

(for context, this safediv is the b/c in a/(b/c))

[niklasdewally]

bubbling up the auxvar instead of posting it to the top level is also very wrong...

for

!(x/(y/z) = 10) 

it just makes z=0 and gets solutions that way, which conjure does not seem to do.

[niklasdewally]

Heres the rule trace: https://gist.github.com/niklasdewally/39a3a938e477f4b109202850e33e3b66

[ozgurakgun]

(a/y !=z)

~~> parsed as:
Neq(Div(a,y), z)

~~> make safe
Eq(Bubble(SafeDiv(a,y), Neq(y,0)), z)

~~> bubble-up
Bubble(Eq(SafeDiv(a,y), z), Neq(y, 0))

~~> bubble-to-and since first arg is bool
And(Eq(SafeDiv(a,y), z), Neq(y, 0))

[ozgurakgun]

the nested case is interesting

!(x/(y/z) = 10)

~~> parsed as
Not(Eq(Div(x, Div(y,z)), 10))

~~> make-safe the inside div
Not(Eq(Div(x, Bubble(SafeDiv(y,z), Neq(z,0)), 10))

~~> (*)
Not(Eq(SafeDiv(x, Bubble(SafeDiv(y,z), Neq(z,0)), Neq(Bubble(SafeDiv(y,z), Neq(z,0), 0), 10))

(*) if we allow make-safe the outside div without bubbling up first, we would get. not wrong, but if we bubbled-up first and then converted the outside Div to SafeDiv we probably won't repeat work?

So rule_Div_to_SafeDiv should refuse to apply i fthe second arg is a Bubble.

Happy for you to try both options (both should be correct) and see the rule application trace before we commit to one.

[ozgurakgun]

here

x/(y/z) != 10

!(x/(y/z) = 10) 

both !=0 bubbles should stay in the !() for the second one, end up at the top level for the first one.

Did you test x/y != 10 and !(x/y=10) as well? Do they work as expected?

[niklasdewally]

here

x/(y/z) != 10

!(x/(y/z) = 10) 

both !=0 bubbles should stay in the !() for the second one, end up at the top level for the first one.

Did you test x/y != 10 and !(x/y=10) as well? Do they work as expected?

We already had a test case for the first; just tried the second and that passes too.

[niklasdewally]

(*) if we allow make-safe the outside div without bubbling up first, we would get. not wrong, but if we bubbled-up first and then converted the outside Div to SafeDiv we probably won't repeat work?

So rule_Div_to_SafeDiv should refuse to apply i fthe second arg is a Bubble.

Do you mean that we should not create a bubble if we have a bubble as a child?

I tried bottom up vs top-down bubbling previously, and that didn't have an affect on the result, although not with the above condition.

[ozgurakgun]

as rule traces if you could produce something of the style I used above that would be the easiest for me to follow/debug

something like

expr1

~~> rulename
expr2

~~> rulename
expr3

[ozgurakgun]

I think both (created nested bubbles and waiting untill they bubble up) should work correctly actually, but one will be fewer steps - I suspect the latter will be fewer steps.

[niklasdewally]

I'm not sure if this is what you meant, but it still doesn't work.

[niklasdewally]

Makes smaller models though :)

[niklasdewally]

This made the rule ordering a lot shorter... By process of elimination, could we be missing something in distribute_not_over_and? This runs after each bubble while there are still some UnsafeDivs left in the tree. not(eq) to neq , flattening etc wait until we only have SafeDivs

[lixitrixi]

I remember having an issue with != ~> !(=). Are the semantics we use in that case correct? This is for the final step after bubbling etc.

[niklasdewally]

This made the rule ordering a lot shorter... By process of elimination, could we be missing something in distribute_not_over_and? This runs after each bubble while there are still some UnsafeDivs left in the tree. not(eq) to neq , flattening etc wait until we only have SafeDivs

I made distribute_not_over_and not applicable if its universe contains a bubble or unsafe div, forcing it to not apply until all bubbling is done (similarly to !=). This did not change anything :(

[niklasdewally]

I remember having an issue with != ~> !(=). Are the semantics we use in that case correct? This is for the final step after bubbling etc.

We do this when everything is fully defined. This seems to work, as the non-nested !(=) and != tests work.

[niklasdewally]

An updated gist with better spacing for @lixitrixi

https://gist.github.com/niklasdewally/968d67b7b569c9f74df2aa33c01128a0

[niklasdewally]

@lixitrixi and I wrote this on paper and theres nothing in the rewritten model that says that z cannot equal zero...

Yet, those are the solutions that we are missing?

[niklasdewally]

Infact, it says z=0 as one of the or cases!

[niklasdewally]

conjure gives us the following minion, which seems the same as what we get as output:

[niklasdewally]

Its a domain evaluation issue!!!!

In our model,__1 has domain {1..20}, but Conjure gives it domain {0..20}!

[ozgurakgun]

Yep, it needs to have 0 in its domain. Good debug!

[niklasdewally]

@ozgurakgun if this is all good, I will write a commit message and clean this up to merge tomorrow.

[github-actions[bot]]

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/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 4840 lines)
  functions..: 59.2% (367 of 620 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.40% and covered lines changed by 8
Branches... coverage: No comparison data available

[ozgurakgun]

oh also there are a few extra files (2, a*txt) but I assume you know about these.

[niklasdewally]

Completed by #454