如何使用 Z3Py 在变量中设置模式答案

【问题标题】：how to set a pattern in a variable using Z3Py如何使用 Z3Py 在变量中设置模式
【发布时间】：2015-10-17 22:28:39
【问题描述】：

我是 Z3 的新手，但我的问题可以用它解决。我有两个变量 A 和 B 以及两个这样的模式：图案_1：1010x11x 模式_2：x0x01111 其中 1 和 0 是位 0 和 1，x（不关心）cold 是位 0 或 1。我想使用 Z3Py 来检查带有 pattern_1 的 A 和带有 pattern_2 的 B 是否可以同时为真。在这种情况下，如果 A = 10101111 和 B = 10101111，则 A 和 B 冷吃的时间相同。谁能帮我这个？？可以用 Z3Py 解决这个问题

【问题讨论】：

标签： z3 z3py

【解决方案1】：

澄清后修改答案

这是表示这些约束的一种方式。有一个称为Extract 的操作可以应用于位向量项。定义如下：

def Extract(high, low, a): """Create a Z3 bit-vector extraction expression."""

其中high是要提取的高位，low是要提取的低位，a是位向量。该函数表示a在high和low之间的位，包括。

使用Extract 函数，您可以约束要检查的任何术语的每一位，使其与模式匹配。例如，如果D 的第七位必须是 1，那么可以写成s.add(Extract(7, 7, D) == 1)。对不是x 的模式中的每个位重复此操作。

【讨论】：

非常感谢。我还有一个问题。你知道我怎么能代表这个向量吗？因为使用 BitVec 我不能输入一个值，而使用 BitVecVal 我必须输入一个常数。如何表示具有高、低和不关心（未定义）值的向量？非常感谢您的帮助。
对于 BitVec，仅使用单个变量是不可能的。 Z3 的类型系统将您可以放入 BitVec 的唯一合法值定义为 0 和 1。您必须将其编码为单独的约束，正如我解释的那样，或者作为两个单独的 BitVec 变量 - 一个表示一个位是否是"don't care" 和一个表示设置了哪个值（0 或 1）的值（假定该位不是“don't care”）。