【发布时间】：2014-05-12 18:52:08
【问题描述】：
我正在使用 Z3 和它的 Python 模块为 Python 构建一个符号执行引擎。
我需要对字符串进行推理，但目前的API for Python似乎不支持它
我发现它可以通过某种方式完成：https://github.com/cs-au-dk/Artemis/tree/master/contrib/Z3-str
如何让 Z3 使用它的 python API 来推理字符串？ （也许可以扩展它？）
如果不可能，尽管我可能会尝试将它实现为整数数组（其中每个整数代表字符串中的一个字符）并编写一些帮助程序来推理它们。这行得通吗？
我用的是python3的4.3.2版本。
【问题讨论】：
-
z3 不支持字符串。也许您可以尝试其他字符串求解器，例如亨比或卡卢扎。它们都被用于符号执行工具中：Hampi 用于 Symbolic PathFinder，Kaluza 用于 Kudzu。
-
感谢 qsphan，但这个求解器的问题似乎是他们不考虑字符串和数字。