有没有一种方法可以在仅使用O（n）语句的Z3中生成全除例外约束？我知道XCSP3提供了此功能。
目前，可以使用O（n ^ 2）语句来做到这一点：
for i in range(len(G) - 1):
s.add( [ Or(G[i] == 0, G[i] != G[j]) for j in range(i + 1, len(G)) ] )
如果重要的话，我有兴趣比较位向量。
Z3确实带有Distinct确保所有元素都不同的谓词，但是据我所知，没有内置函数distinct-except。
为了对这种约束进行编码，我将使用数组来跟踪插入元素的基数。像这样：
from z3 import *
def distinct_except(G, ignored):
if len(G) < 2:
return BoolSort().cast(True)
A = K(G[0].sort(), 0);
for i in range(len(G)):
A = Store(A, G[i], If(G[i] == ignored, 0, 1 + Select(A, G[i])))
res = True
for i in range(len(G)):
res = And(res, Select(A, G[i]) <= 1)
return res
我们只需将元素插入数组中，如果不忽略该元素，则将计数增加1，否则输入0。这将避免线性构建数组的if-then-else节点。然后，我们再次遍历该列表，并确保从未存储大于1的内容。
这将保持表达式的大小res和A线性，并且z3应该能够相当有效地处理它。如果您发现其他情况，我想听听。
这是一些测试，以查看实际效果：
# Test: Create four variables, assert they are distinct in the above sense
a, b, c, d = BitVecs('a b c d', 32)
s = Solver()
s.add(distinct_except([a, b, c, d], 0))
# Clearly sat:
print s.check()
print s.model()
# Add a constraint that a and b are equal
# Still SAT, because we can make a and b 0
s.add(a == b)
print s.check()
print s.model()
# Force a to be non-zero
s.add(a != 0)
# Now we have unsat:
print s.check()
打印：
sat
[b = 1024, a = 16, c = 1, d = 536870912]
sat
[c = 33554432, a = 0, d = 32768, b = 0]
unsat
请注意，您始终可以print s.sexpr()在调用之前先查看所生成的表达式，s.check()以查看它们随着输入列表变大而如何增长。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句