使用Z3求解正则表达式填字游戏

作者在产假期间对Z3和SMT求解器产生了兴趣，开发了基于Z3的正则表达式填字游戏求解器。

正则表达式填字游戏由一个未知字符的网格组成，这些字符由给定的正则表达式约束。

为了解决这个问题，需要将正则表达式编码为确定性有限自动机（DFA），并在Z3中表达正则匹配。

使用qntm的greenery库将正则表达式转换为DFA，并在项目中使用numpy处理状态转换表。

在Z3中定义状态和字符的整数表示，并添加适当的约束以确保字符符合正则表达式。

初始求解器性能较慢，解决3x3的填字游戏需要十分钟，作者进行了性能调试和优化。

通过域特定分析生成额外约束来修剪状态，从而提高求解器性能。

将状态转换函数显式表示为条件表达式，而不是使用未解释的函数，以提高性能。

使用Z3的lambda表达式和宏查找器来优化求解器性能，避免重复构建表达式。

尝试使用Z3的枚举类型来表示状态和字符，发现其性能不如整数表示。

Z3支持正则表达式理论，可以直接将正则表达式线索编码为Z3正则表达式，简化求解过程。

作者总结了使用Z3的经验，包括Z3支持的多种数据类型和理论，以及性能的不稳定性。