https://regexcrossword.com/ solver using Z3py
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
crossword
.gitignore
LICENSE.txt
Makefile
README.md
bbc.py BBC Radio puzzle demo Jun 30, 2018
grammar.md

README.md

regex-crossword-solver

Regex Crossword solver written in Python. Runs in both Python 2 and 3.

It solves a puzzle by converting the puzzle into equivalent SMT problem. Detailed method is described here.

Demo

5 x 14 regex crossword posted in BBC Radio 4 Puzzle for Today.

$ python bbc.py

Requirements

You can install them by

pip install ply
pip install angr-only-z3-custom

Make sure you have /usr/local/lib/ and $HOME/.local/lib in LD_LIBRARY_PATH environment variable.

Usage

Solve Regex Crossword puzzle directly.

>>> from crossword import solve_crossword
>>> solve_crossword(["HE|LL|O+","[PLEASE]+"], ["[^SPEAK]+","EP|IP|EF"])
[['H', 'E'], ['L', 'P']]
>>> solve_crossword(["[A-GN-Z]+"], ["[D-HJ-M]","[^A-RU-Z]"], ["[^A-DI-S]+"], ["[^F-KM-Z]","[A-KS-V]"])
[['E', 'T']]

You can also manually find a solution to each regex.

>>> from crossword import solve_regex
>>> solve_regex("(U|O|I)*T[FRO]+", 5)
'IIITF'

Run tests

nosetests