Z3中的精确n编码

Question

我试图在Z3中的UOD (此处列表)中编码“精确N”。我在CBMC (C有界模型检查器)中实现的方法是将列表定义为_Bool，并使用一个无符号的int，只使用状态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”替换为(Not)“至少N+1”。而对于N >= 5，L=6 0 0。内存不足的代码在我的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

你想要伪布尔函数吗？最多/至少/准确地说N件事是真的？可能是系数？

如果是这样的话，Z3可以通过SMT和各种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