Z3Python:字符串排序支持 [英] Z3Python: StringSort support

问题描述

我正在使用 Z3 及其 Python 模块为 Python 构建一个符号执行引擎.

I'm building a symbolic execution engine for Python using Z3 with it's Python module.

我需要对字符串进行推理，但当前 Python API

I need to reason about strings, but it doesn't appear to be supported in the current API for Python

我发现它可以以某种方式完成:https://github.com/cs-au-dk/Artemis/tree/master/contrib/Z3-str

I found it can be done somehow: https://github.com/cs-au-dk/Artemis/tree/master/contrib/Z3-str

我怎样才能让 Z3 使用它的 Python API 来推理字符串?(也许会延长它?)

How can I get Z3 to reason about strings using it's python API? (maybe extend it?)

如果不可能，尽管我可能会尝试将其实现为整数数组(其中每个整数代表字符串中的一个字符)并编写一些帮助程序来推理它们.那行得通吗?

If not possible, though I may try to implement it as arrays of ints (where each int represents a char in the string) and write some helpers to reason about them. Would that work?

我在 python3 中使用 4.3.2 版本.

I'm using the 4.3.2 version with python3.

推荐答案

你找到的链接是Z3-str，Z3上的一个理论插件.Z3-str 是使用旧版本 Z3 的外部理论插件 API(用于 C)实现的.这些插件 API 在 Z3 4.3.2 中已弃用.

The link you found is Z3-str, which is a theory plug-in on Z3. Z3-str was implemented using the External Theory Plugins API (for C) of an old version of Z3. These plugin APIs are deprecated in Z3 4.3.2.

这篇关于Z3Python:字符串排序支持的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！