Неожиданное поведение с GADT в z3, полученное значение, равное каждому целому числу - PullRequest
Новая
       10

Неожиданное поведение с GADT в z3, полученное значение, равное каждому целому числу

0 голосов
/ 07 февраля 2019

Это будет правильный вопрос для кого-то с более глубоким пониманием z3 или интересом к его причудам.

Привет! Я запускаю следующий тест, чтобы понять, как работают GADT в 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()

1 Ответ

0 голосов
/ 08 февраля 2019

Это действительно сбивает с толку, но я думаю, что z3 делает правильные вещи.

Проще увидеть, что происходит, если мы сбросим сгенерированный SMT-Lib.(Добавьте 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 сделал для вас.Надеюсь, это понятно.Классный пример!

...