问题标签 [z3py]

It looks like Microsoft completely pooched their "rise4fun" website and the Z3 Python tutorial no longer loads.

How can I define define a matrix in Z3 for Python and impose some constraints on it?

我试图证明群论中的一些一般性质。

例如左取消属性： ( xy = xz ) => (y = z) 它使用以下代码证明

相应的输出是：

现在，当我尝试使用以下代码证明右取消属性时： ( yx = zx ) => (y = z)

我正在获得

请让我知道如何证明正确的取消属性或者使用 Z3 是不可能的？

我想解决的公式在 C 中如下所示：

我通过以下方式将其重写为 z3py：

有什么建议么 ？
PS：请注意，尝试以这种形式求解公式：
solve( (UDiv( (w*x*y+31), 8 )) * z == 0xffffffff)
是可能的，所以我不能相信按位运算会导致这个公式无法满足。

根据http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html如果我使用 .smt 文件，我可以从 z3 命令行设置 CC_NUM_THREADS=4。

如果我使用的是 z3py api，我该怎么做？

理想情况下，可以“或”表示为位向量的两个数字，但我做不到。请告诉代码中是否有错误或其他问题

给出的错误是

从这个错误中，我了解到 Or 只能用于 bool 变量。我的问题是如何或为 BitVectors

我正在尝试对矩阵执行一些符号计算（将符号作为矩阵的条目），之后我将有一些可能的解决方案。我的目标是根据约束选择解决方案/解决方案。

例如，M是一个矩阵，其中一个元素为symbol. 该矩阵将有 2 个特征值，一个是正的，一个是负的。使用 z3 我试图仅找出负值，但我无法这样做，因为 a 被定义为符号，除非我将其转换为实值，否则我无法将其写为约束。

我应该怎么办？有什么方法可以将（符号）转换为实数或整数，以便我可以将其用作约束s.add(a>0)

我一直在尝试解决一个小问题，其中包括某些术语的绝对值。在 z3 中不支持 abs() 函数。在python中有，但我最终必须将它传递给z3py。有什么方法可以将带有绝对运算符的术语从python传递给z3，或者有其他方法吗？以下是一个小示例的代码。

答案应该是 y=1，当你删除 abs() 时就是这种情况。有没有办法用绝对值函数解决这个问题？绝对（）。或者有什么方法可以在python中解决它，然后我可以将它传递给z3。我也试过 sympy 但它不起作用。

作为 Z3 的初学者，我想知道是否有办法让 Z3Py 使用预定义的 Python 函数。以下是一个解释我的问题的小例子。

f(x) 是在 python 中定义的函数。当 x <= 0 时，f(x) 返回 0。我添加了一个约束 s.insert(f(a) == 0)，希望 Z3 可以为变量“a”找到合适的值（例如 -3）。但是这些代码不能正常工作。我应该如何改变它？

（请注意，我需要在 Z3 之外定义 f(x)，然后被 Z3 调用。）

我想要做的是调用图形库提供的预定义函数而不将其转换为 Z3。我正在使用 NetworkX 库，一些代码如下：

我需要 Z3 来帮助我在 G2 中找到一个顶点，这样在删除该顶点后，G2 与 G1 同构。例如

The C API for z3 has functions such as Z3_mk_bvadd_no_overflow, but these do not seem to be available from the Python API. Before I start hacking to solve this I'd just like to verify that this is the case and also request that these be added to the official version.

I'm trying adding things like this to z3.py, but so far haven't managed to get the details right. Suggestions about where I'm going wrong would be appreciated. I'm working on the contrib branch.

嗨，我正在尝试通过非常基本的迭代过程找到具有一些约束的目标函数的最小值。问题是由于浮点问题程序永远不会终止。我需要精确到 15 位十进制数字，我不希望 z3 或 python 探索任何高于该精度的值。以下是代码：我通过Mathematica计算的准确结果是：a=1，b=2，c=3，d=4，e=5，f=6，目标函数对应的最小值是：2.06846* 10^-14。我可以计算出相同的结果吗？

以下是代码：（请复制粘贴运行，因为表达式很长）