Search for a command to run...
Articles tagged with #z3
In previous post, I showed how to break Caesar cipher with Z3. This wasn't really all that exciting as Caesar cipher has only 26 possibilities, so it's triival to break with brute force, and you can even just display all possible answers and choose t...
Z3 is usually given a list of hard constraints, and told to solve them, but it can do quite a few more things. Let's use it unconventionally and break Caesar cipher. The Challenge The following plaintext from Wikipedia: In cryptography, a Caesar cip...
This is the final episode with Crystal Z3 solvers, at least for now. In previous episode I showed how to solve Lights Up puzzle with math, now it's time to write a Crystal Z3 solver. Light Up (Akari) is a simple puzzle with following rules: there's ...
Light Up (Akari) is a simple puzzle with following rules: there's a grid of cells some cells are wall cells your task is to place light bulbs in some of the cells light spreads horizontally and vertically from light bulbs, but it doesn't pass throug...
Dominosa is a puzzle with simple rules: there's a grid filled with numbers you need to pair those numbers into dominos each domino needs to be different As usual, I recommend playing the puzzle a few times to get a good feel for it. It will make it...
While writing various puzzle game solvers in Crystal Z3 I discovered two big issues: I frequently needed .reduce chains of +/*/and/or with special case for empty arrays Model#[] returned untyped result (Expr) even though its exact type is statically...