Z3中整数集合加法归约问题：首个示例未返回预期unsat

我最近在尝试用Z3对固定大小的集合执行加法归约操作，以此证明相关性质，但碰到了两个棘手的问题：第一个测试用例里，按逻辑应该返回*unsat*，但实际结果不符；第二个用例能正常工作，但必须通过循环不断获取模型、添加约束，这种增量调整的方式太繁琐，我想找到更简洁的声明式方法。

第一个未达预期的测试代码 #

这个例子中，我定义了一个包含0到4（共5个元素）的集合，然后声明了10个变量，尝试对这些变量对应的集合元素求和。按道理，断言求和等于1应该是不可能的，但Z3并没有返回预期的*unsat*：

def test_reduce():
    LIM = 5
    VARS = 10
    poss = [Int('i%d'%x) for x in range(VARS)]
    i = Int('i')
    s = Solver()
    arr = Array('arr', IntSort(), BoolSort())
    s.add(arr == Lambda(i, And(i < LIM, i >= 0)))
    a = arr
    for x in range(len(poss)):
        s.add(Implies(a != EmptySet(IntSort()), arr[poss[x]]))
        a = SetDel(a, poss[x])

    def final_stmt(l):
        if len(l) == 0:
            return 0
        return If(Not(arr[l[0]]), 0, l[0] + (0 if len(l) == 1 else final_stmt(l[1:])))

    sm = final_stmt(poss)
    s.push()
    s.add(sm == 1)
    assert s.check() == unsat

第二个可行但繁琐的测试代码 #

下面这个例子能正确验证求和的性质，但它需要循环迭代：每次从模型中获取一个集合元素，累加到总和后，再添加约束排除这个元素，直到集合被遍历完。这种方式虽然有效，但不够优雅，我希望避免：

import uuid

def test_reduce_with_loop_model():
    s = Solver()
    i = Int('i')
    arr = Array('arr', IntSort(), BoolSort())
    LIM = 1000
    s.add(arr == Lambda(i, And(i < LIM, i >= 0)))
    sm = 0
    f = Int(str(uuid4()))
    while True:
        s.push()
        s.add(arr[f])
        chk = s.check()
        if chk == unsat:
            s.pop()
            break
        tmp = s.model()[f]
        sm = sm + tmp
        s.pop()
        s.add(f != tmp)

    s.push()
    s.add(sm == sum(range(LIM)))
    assert s.check() == sat
    s.pop()
    s.push()
    s.add(sm == 11)
    assert s.check() == unsat

我的核心疑问 #

• 为什么第一个测试用例无法返回预期的*unsat*？是不是我的约束或者归约逻辑存在疏漏？
• 有没有不用这种增量模型调整的方式，直接用声明式方法来完成固定大小集合的归约性质证明？

内容的提问来源于stack exchange，提问作者Mike