我想知道是否有有效的方法来简化Microsoft Z3位向量上的算术公式表达式。但是，首先，我想解释一下这个问题。让我们从一个例子开始：

x + y == (x ^ y) + 2 * (x & y)

这两个x + y和(x ^ y) + 2 * (x & y)的，实际上，编码加入了位向量。当然，当在二进制程序中找到时，右手公式用于混淆逆向器。我尝试寻找工具和技术来简化混淆的公式并找到更简单的公式形式（左手）。

为此，我查看了 Z3 的 Python 界面，试图看看我能从中得到什么。因此，定义混淆公式是这样完成的：

>>> from z3 import *
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> fun1 = (x ^ y) + 2 * (x & y)

现在，让我们尝试借助内置函数简化此函数simplify：

>>> simplify((x ^ y) + 2 * (x & y))
(x ^ y) + 2*~(~x | ~y)

不是很令人信服......但是，让我们尝试证明与以下等价x + y：

>>> prove((x ^ y) + 2 * (x & y) == x + y)
proved
>>> prove((x ^ y) + 2 * (x & y) == x - y)
counterexample
[y = 2164268032, x = 2139094080]

我添加了一个否定结果以表明也可以取消公式的资格。

因此，如果该simplify函数不是真正令人信服，仍然可以尝试以蛮力的方式将未知公式与一系列更简单和常用的公式一个接一个地进行比较。但是，这种方式对我来说似乎效率极低。我想我缺少一些更智能的算法来简化公式。

我想知道是否有一些现有的工具或众所周知的技术可以比蛮力方法更有效地执行。因此，如果有人对此有一些提示或评论，那将是非常受欢迎的。