z3 求解器中的存在限定符产生违反直觉的结果

Question

我正在使用 Z3 求解器来尝试证明某些集合的域的质量。在这个例子中，我构造了两组整数。在伪代码中，它会是......

a0 = x such that x < 5
a1 = x such that x < 6

我想构造来自a0 的元素和来自a1 的元素的所有可能和的集合。直觉上，我认为这是：

a2 = x such that x < 10

我不确定在 Z3 中表达a2 的最佳方式，但下面的代码显然不是其中之一。该测试失败，但按照我的逻辑，它应该通过。 Exists([v], And(a1[v], Not(a2[v]))) 应该会产生不令人满意的结果，因为a1 中没有不在a2 中的数字。了解为什么下面的代码会产生令人满意的结果以及结果会是什么会很有帮助。

def test_set_inclusion_under_addition():
    a0 = Array('a0', IntSort(), BoolSort())
    a1 = Array('a1', IntSort(), BoolSort())
    a2 = Array('a2', IntSort(), BoolSort())
    x, y, a, m, n, v = Ints('x y a m n v')
    false, true = Bools('false true')
    s = Solver()
    s.add(false == False)
    s.add(true == True)
    s.add(a0 == Lambda([m], If(m < 5, true, false)))
    s.add(a1 == Lambda([n], If(n < 6, true, false)))
    s.add(a2 ==
        Lambda([x],
            If(Exists([a],
                And(a0[a],
                a1[x - a])),
            true,
            false)))
    s.add(Exists([v], And(a1[v], Not(a2[v]))))
    assert s.check() == unsat

Answer 1

我不确定你为什么说你的测试失败了。当我运行它时，它成功地为check 调用生成了unsat。

也许您使用的是旧版本的 z3？最近对 Lambda 构造的处理方式进行了一些更改。您可以尝试使用https://github.com/Z3Prover/z3/releases/tag/Nightly 的新版本吗？或者更好的是，直接从源代码构建它。