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

Question

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

你好，我正在运行下面的测试来了解GADTs如何在z3python中工作。似乎值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做同样的事情。由于应用于用bar构造的东西的unfoo析构函数没有被指定，所以它只选择一个使问题可满足的解释。总而言之，当您定义一个像unfoo这样的析构函数时，您要说的是：

• 如果你收到一个foo值，那么告诉我里面是什么
• 如果您收到一个非foo值，那么请给我您想要的任何东西；只要它的类型正确并且满足我的其他约束条件

而这正是Z3为你所做的。我希望这是清楚的。很酷的例子