z3 中 GADT 的意外行为，得到的值等于每个整数

Question

对于对 z3 有更深入了解或对其怪癖感兴趣的人来说，这将是一个正确的问题。

您好，我运行进行以下测试以了解 GADT 在 z3 python 中的工作原理。值 unfoo(bar(foo(b))) 似乎等于任何整数？这样对吗？

下面是一个有效的测试 - 你能帮忙解释一下它为什么有效吗？

import pytest
from z3 import Datatype, Solver, IntSort, Int

def test_Whosebug():
    FooBar = Datatype('FooBar')
    FooBar.declare('foo', ('unfoo', IntSort()))
    FooBar.declare('bar', ('unbar', FooBar))
    FooBar = FooBar.create()

    foo = FooBar.foo
    unfoo = FooBar.unfoo
    bar = FooBar.bar
    unbar = FooBar.unbar

    solver = Solver()
    solver.push()
    a = Int('a')
    b = Int('b')
    solver.add(a == unfoo(bar(foo(b))))
    assert str(solver.check()) == "sat"
    model = solver.model()
    assert model.evaluate(a).as_long() == 1
    assert model.evaluate(b).as_long() == 0
    solver.pop()

Answer 1

这确实令人困惑，但我认为 z3 做的是正确的。

如果我们转储生成的 SMT-Lib，就更容易看到发生了什么。（在调用 check 之前添加 print solver.sepxr()。）我得到：

(declare-datatypes ((FooBar 0)) (((foo (unfoo Int)) (bar (unbar FooBar)))))
(declare-fun b () Int)
(declare-fun a () Int)
(assert (= a (unfoo (bar (foo b)))))

需要多看几眼，但涉及的类型如下：

b 是 Int
(foo b) 是一个 FooBar，但特别是它具有构造函数 foo.
(bar (foo b)) 是一个 FooBar，但特别是它具有构造函数 bar.
(unfoo (bar (foo b)) 是一个 Int，但它将 unfoo 选择器应用于使用 bar.

这就是问题所在：你有一个术语 "destructed" 一个术语是用其他东西构建的。

此类场景的典型 'SMTLib' 答案是 "underspecified." 也就是说，逻辑不保证什么成立，因此允许求解器以任何它想要的方式实例化。所以，你得到的模型是正确的；虽然有点混乱。

为了更好地理解这一点，想象一下您将如何使用 Haskell:

这样的语言编写代码

data FooBar = Foo {unfoo :: Int} | Bar {unbar :: FooBar}
check a b = a == unfoo (Bar (Foo b))

让我们试试：（ghci 是 Haskell 解释器）：

ghci> check 1 0
*** Exception: No match in record selector unfoo

啊！它告诉我们，我们搞砸了。我们可以修复它吗？我们开始吧：

data FooBar = Foo Int | Bar {unbar :: FooBar}

unfoo :: FooBar -> Int
unfoo (Foo i) = i
unfoo (Bar _) = 1  -- Conveniently pick the result here!

check a b = a == unfoo (Bar (Foo b))

我们得到：

ghci> check 1 0
True

瞧！请注意我是如何定义 unfoo 自己来制作这个 "satisfiable".

本质上，z3 做同样的事情。由于 unfoo 应用于用 bar 构造的东西的析构函数是未指定的，它只是选择一个使问题可满足的解释。总结一下，当你定义一个像unfoo这样的析构函数时，你说的是：

如果你收到一个foo值，请告诉我里面是什么
如果你收到一个非foo的值，请给我任何你想要的；只要它是正确的类型并满足我的其他限制。

这正是 Z3 为您所做的。我希望这很清楚。不过很酷的例子！

z3 中 GADT 的意外行为，得到的值等于每个整数

Unexpected behavior with GADTs in z3, got value that is equal to every integer

python

z3

z3py