[cvoss]

> Z3 SMT theorem prover to validate

Well that's awesome. Do you know, is the theory decidable? My guess would be yes, due to quantification over only bounded integers, but I'm not sure what the full complexity of the rule language is.

[Scaevolus]

The rules you create are in the form of venn diagrams of up to 4 overlapping regions (see shagie's top-level comment), where you can specify rules for each region to match and the sizes of the different overlaps, and then the output is a decision-- marking specific regions as clear/bomb, creating new regions (!), or even changing region visibility-- marking them as hidden or removing them from further rule evaluations.

Those rules can include terms like "5", "x", "x+2", and "x+y+3", so you can express most variants in a signle rule.

The closest to "undecidable" under this rule system is that you can hide a region and prevent further deductions from it, making some board states impossible to resolve. Other than that, all the rules are decidable.