如何使z3中的GADTs上的操作符过载？

Question

目标

我的目标是在一个理论中工作，在这个理论中，我可以接触到整数，也可以对整数进行推理，而且还有一个已知的函数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

问题是bar最终是可计算的，但不能用整数算术编码，所以我试图将它映射到一个“未知”函数。你知道吗

特定示例

在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

我是否可以重载+运算符以跨foo值工作，如下所示：

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

有没有不牺牲可判定性的方法？你知道吗

Answer 1

从纯z3/SMTLib的角度来看：您不能用SMTLib或通常的SMT-Lib来做这件事。如果要添加FooBar，必须为此定义一个自定义函数。你知道吗

从“Python”的角度来看：我确信有一些Python魔法咒语可以为FooBar重载+（您可能必须先将它隐藏在某个类后面），所以它看起来像是常规加法。但请记住，这与Z3或SMTLib无关，这只是Python的把戏。你知道吗

即使这是可能的，我也强烈建议不要这样做：虽然重载很可爱，但它几乎总是会导致更多的麻烦，而SMTLib对多态性的工作方式相当挑剔：它只为+/-等符号提供了“烘焙”多态性。；特别是它明确禁止用户定义的多态性。你知道吗