python - Z3 中恰好 n 编码

Question

我正在尝试在 Z3 的 UOD(此处为列表)中对“EXACTLY N”进行编码。我以前在 CBMC(C 有界模型检查器)中实现的方法是我将 List 定义为 _Bool 并使用一个无符号整数并且只是状态 B1 == N。

// L is the length of the List b1.
unsigned int B1 = 0
for i in range(L):
      B1 = b[i] + B1 
....
__CPROVER_assume (B1 == N);

这在 Z3 中不是直截了当的，因为变量是表达式，而不是类型值本身。所以我最初的尝试是对“至少 N”和“最多 N”进行编码，并将它们结合起来以获得“ExACTLY N”。改进最初的想法并使用我的逻辑类，我将“最多 N”替换为(不)“至少 N+1”。但是对于 N >= 5 且 L =~ 600。我的 4 Gb RAM 机器上的代码内存不足。

# b1 is the List
X_list = []
for i in range(L-3):
  for j in range(i+1,L-2):
    l = And ( b1[j], b1[i])
    for k in range(j+1,L-1):
        l1 = And ( l, b1[k])
        for l in range(k+1,L):
            X_list.append( And (b1[l], l1))
B1 = Or(X_list) 

File "file1.py", line 49, in <module>
X_list.append( And (b1[l], l1))
File "/usr/lib/python2.7/dist-packages/z3/z3.py", line 1611, in And
return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
File "/usr/lib/python2.7/dist-packages/z3/z3core.py", line 1653, in
Z3_mk_and
raise Z3Exception(lib().Z3_get_error_msg(a0, err))
z3.z3types.Z3Exception: out of memory

有没有更好的方法在 Z3 中对此进行编码。也许经验丰富的 Z3 用户有一些很好的编码方法。谢谢。

Answer 1

你似乎想要伪 bool 函数？最多/至少/恰好 N 件事是真的？可能还有系数？

如果是这样，Z3 将通过 SMT-Lib 和各种 API 直接支持此功能。对于 Python，请参见此处:https://github.com/Z3Prover/z3/blob/b27a4a3593fd15c003d3e30da20b35ac96b7218e/src/api/python/z3/z3.py#L7718-L7793

对于 SMTLib，请参阅此处的讨论:K-out-of-N constraint in Z3Py