意外的行为与Z3 GADTs，得到的值等于每一个整数

Question

这将是有人在其怪癖z3或利益的更深层次的理解正确的问题。

还有嗨，我运行下面的测试来了解GADTs在z3蟒蛇是如何工作的。这似乎是价值unfoo(bar(foo(b)))等于任意整数？这是正确的吗？

以下是一个有效的测试 - 你可以帮助解释为什么它的工作原理？

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

def test_stackoverflow():
    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-库。 （你叫print solver.sepxr()前添加check）我得到：

(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东西。

，这其中就有问题：你有“破坏”与用别的东西建立一个术语。

典型的“SMTLib”答案这样的场景是“得以确认。”也就是说，逻辑是没有什么持有，因此，求解器允许它想要的任何方式来实例化的承诺。所以，你得到的模型是正确的;虽然那种混乱。

看到这更好的，想象一下你将如何在象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使这个“令人满意”。

从本质上讲，Z3做同样的事情。由于适用于具有unfoo构建东西bar析构函数是尚未，它只是挑选一个解释，使问题满足的。概括起来，当你定义像unfoo析构函数，你要说的是：

• 如果您收到foo值，然后给我里面有什么
• 如果您收到一个非foo值，然后给我不管你请;只要它是正确的类型，并满足我的其他限制。

而这恰恰是Z3为你做。我希望是十分明显的。酷例子，但！