Как перегрузить операторы через GADT в z3? - PullRequest
Новая
       13

Как перегрузить операторы через GADT в z3?

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

Цель

Моя цель - работать в теории, в которой у меня есть доступ и я могу рассуждать о целых числах, а также есть известная функция bar.

Я хочу иметь возможность решать уравнения, подобные этим: 

bar(bar(x)) == bar(y)  Solution: y = bar(x), bar is unknown
2 + bar(2) == bar(x)   Solution: x is unknown, bar is unknown

Проблема в том, что строка в конечном итоге вычислима, но не может быть закодирована в целочисленной арифметике, поэтому я пытаюсь сопоставить ее с «неизвестной» функцией.

Конкретный пример

В z3 я работаю со следующим пользовательским типом данных. 

import pytest
from z3 import Datatype, IntSort

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

Можно ли перегрузить *Оператор 1021 * для работы с foo значениями, такими как:

Forall([x, y], foo(x) + foo(y) == foo(x + y))

Есть ли способ сделать это, не жертвуя разрешимостью?

1 Ответ

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

С точки зрения чистого z3 / SMTLib: Вы не можете сделать это в SMTLib или на обычном языке SMT-Lib.Если вы хотите добавить FooBar, вам нужно определить для этого пользовательскую функцию.

С точки зрения "Python": я уверен, что есть какое-то магическое заклинание Python для перегрузки + для FooBar (возможно, вам придется сначала спрятать его за каким-то классом), так что это выглядит как обычное добавление.Но имейте в виду, что это не имеет ничего общего с Z3 или SMTLib, и это будет простой трюк с Python.

Даже если это возможно, я настоятельно рекомендую против этого: хотя перегрузка хороша, онапочти всегда в конечном итоге вызывает больше проблем, чем оно того стоит;и SMTLib довольно требователен к тому, как работают полиморфные вещи: он имеет только «запеченный» полиморфизм для таких символов, как + / - и т. д .;и, в частности, он явно запрещает определяемый пользователем полиморфизм.

...