Implement Default Case Rule Check

[jadeandtea]

Description

As #777 lays out, case rules should be tested. However, it is tricky to make sure that they will work in all cases. Case rules may generate anywhere between 1 and 10 cases, depending on what the rules describe, and not all case rules have a logical way of verifying that the rule was applied correctly.

Consider the finish room case rule in Nurikabe. What metrics could be used to verify that the cases are correct? The number of branches (what if we have duplicate branches)? The number of modified cells (what about different-sized rooms)? The rooms created being complete (what if we have duplicate branches (again))? There might not be a logically sound way to verify that this rule was applied correctly.

Instead of coming up with the correct logic for every case rule for every puzzle, we can generalize a way to guarantee that a case rule is applied correctly simply by matching the created branches to the boards generated by the case rule. This involves checking every possible matching of boards to the cases generated; when n <= 10, this is manageable. If the limit of the number of branches allowed for a given node increases, then this may become a problem and will need to be optimized.

A big assumption this makes is that the getCases function returns the right cases when applying the case rule. There really is no good way of programmatically testing that the getCases function is correct, but generally it is easier to convince oneself that the generated cases are as expected. The getCases function will need to be monitored in the future to make sure that this assumption holds.

Closes #777, #638, #643

Type of change

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• Enhancement (improvement to an already existing feature)
• Breaking change (fix or feature that would cause existing functionality to not work as expected)

How Has This Been Tested?

On smaller puzzles, I have messed around with standard proof creation and applying case rules and direct rules in various situations. All case rules seem to check out when manually creating cases, as well as shifting the order of cases or changing the type of rule to a direct rule.

In larger puzzles, generating all cases in certain situations seems to massively slow down the program. I believe that the issue is due to the specific getCases function not terminating early.

Checklist:

• I have performed a self-review of my code
• I have commented my code, particularly in hard-to-understand areas
• I have made corresponding changes to the documentation (if applicable)
• My changes generate no new warnings
• I have added tests that prove my fix is effective or that my feature works
• New and existing unit tests pass locally with my changes

[jadeandtea]

There is an issue related to when a user wants to create their own cases. Some case rules in LEGUP are "smart" in that they won't generate cases where the next step leads to a contradiction. Consider the Nurikabe Finish Room case rule. If the generated case causes multiple white regions to merge into one, the case isn't generated, as the resulting board would have a Multiple Numbers contradiction. However, if a user wanted to generate all possible ways a room could be finished manually, they might merge two white regions. In this situation, the case rule would not check out, as the user-created cases do not match the cases generated by the program.

There are three solutions Bram brought up:

1. Add a flag that determines how "smart" the auto-generated case rules are. There is already a flag for allowing the auto-generated case rules in the first place, so it shouldn't be too bad to add another flag. The more annoying part is reimplementing the getCases functions for all the "smart" case rules. However, this doesn't really fix the issue; if the user doesn't know which mode the program is in, they still have to guess how to generate the cases.
2. Compare the cases in the transition to two sets of cases: one "smart" set and one "dumb" set. The worry is the amount of time it takes to generate and match the two sets. This shouldn't be too bad to implement, as the recursive code should just have a check somewhere that removes cases. The main concern with this approach is runtime, which is already a problem with some larger puzzles.
3. Add documentation for each of the case rules such that a user can follow them to generate the "smart" cases. This makes it less straightforward for the user, but it would be the easiest to implement (as in nothing to implement at all).

It is probably best to implement option 2, but I need to figure out how to match the possible cases in a reasonable amount of time.