问题标签 [z3py]

我的问题与： Z3：将 Z3py 表达式转换为 SMT-LIB2？

我正在尝试将 z3py 表达式从 smtlib2 格式转换。使用以下脚本，但在将结果提供给 z3 或任何其他 SMT 时转换后，我得到：

“语法错误，意外让”

有什么方法可以使用 z3py 将它带入 smtlib2 格式，这样我就不必再次编写长表达式。

以下是我用于转换的代码：

这是输出：

我试图将python的数学库与z3python一起使用，我所做的是

它返回的错误消息是 AttributeError: ArithRef instance has no attribute ' float '。

我的目的并不是真正使用 Z3 中的阶乘函数，而是我很好奇数学库中的函数是否可以与 Z3 一起使用。任何建议表示赞赏。

如何使用 z3 以多项式形式打印 (x) 的复杂函数？该simplify函数打印一些讨厌的东西：

返回 sat，并给出解决方案

不满足约束。如果我删除最后一个约束，它会返回一个满足前两个（平凡）约束的合理对。这是怎么回事？

在线尝试的永久链接：http ://rise4fun.com/Z3Py/fk4

编辑：我是 z3 的新手，所以我有可能做错了什么，请告诉我。

我试图用 Z3 证明在一般拓扑中给出的定理

TPTP-拓扑

我正在使用以下 Z3-SMT-LIB 代码翻译那里给出的代码

对应的输出是

请在此处在线运行此示例

第一个sat是正确的；但第二个sat是错误的，它必须是unsat。换句话说，Z3 是说定理及其否定同时为真。

请让我知道在这种情况下会发生什么。非常感谢。一切顺利。

我正在尝试将 2 个 2*2 顺序的矩阵相乘。其中一个矩阵包含未知参数“k1”。我想检查一个令人满意的解决方案，即 k1 的值。两个矩阵的乘积将等于第三个矩阵。注意：我不想将乘法转换为线性关系或方程组，我想将其作为矩阵进行操作。

这是我卡住的地方。

有什么出路吗？

我正在尝试使用以下代码证明群论中的右取消属性

但我得到

请让我知道会发生什么。非常感谢。

我想知道是否可以在 Z3Py 中创建依赖于另一种代数数据类型的代数数据类型。

例如，假设我定义了自己的 Bool 数据类型，并且我想自己定义一个 Bool 列表：

这工作正常，然后：

这失败并显示以下消息：

原因是使用 Bool() 作为对早期定义的数据类型的引用。使用 Z3 布尔排序就像一个魅力：

依赖于另一个代数数据类型的代数数据类型的定义是不可能的，还是我需要通过 s.th。除了 Bool() 吗？

提前致谢！卡斯滕

作为逆向工程练习的一部分，我正在尝试编写 Z3 求解器来查找满足以下程序的用户名和密码。这特别难，因为大家参考的 z3py 教程（rise4fun）已经挂了。

我从二进制程序集中获得了该代码，虽然它可能是错误的，但我想专注于编写求解器。我从第一部分开始，只是计算r1，这就是我所拥有的：

我要断言的是数组中没有小于“A”的字母，所以我希望得到一个数字大于 65 的任意大小的数组。

显然这是完全错误的，主要是因为它无限循环。另外，我不确定我是否正确计算总和，因为我不知道它是否已初始化为 0。有人可以帮助弄清楚如何让第一个循环工作吗？

编辑：我能够得到一个接近上面显示的 C++ 代码的 z3 脚本：

此代码能够为我提供正确的用户名和密码。但是，我硬编码了用户名的长度为 1，密码的长度为 5。我将如何更改脚本，这样我就不必对长度进行硬编码？每次运行程序时如何生成不同的解决方案？

随后在不同的变量和公式上调用 Z3py 的 Exists 函数时，我得到完全相同的结果。这是某种Python问题还是Z3在这里坏了？怎么修？以下最小示例说明了该问题：

输出：