Z3Python:字符串排序支持

Question

我正在使用Z3及其Python模块为Python构建一个符号执行引擎。你知道吗

我需要对字符串进行推理，但在当前的API for Python中似乎不支持它

我发现这是可以做到的：https://github.com/cs-au-dk/Artemis/tree/master/contrib/Z3-str

如何让Z3使用其pythonapi对字符串进行推理？（可能会扩展吗？）你知道吗

如果不可能，我可以尝试将其实现为int数组（其中每个int表示字符串中的一个字符），并编写一些帮助程序来解释它们。这样行吗？你知道吗

我正在使用python3的4.3.2版本。你知道吗

Answer 1

你找到的链接是z3str，它是Z3上的一个理论插件。z3str是使用Z3旧版本的外部理论插件API（用于C）实现的。Z34.3.2中不推荐使用这些插件API。你知道吗