x + y和(x ^ y) + 2 * (x & y)都在位向量上编码加法。当然，在二进制程序中找到时，右手公式会用来混淆反向器。我尝试找到简化混淆的公式的工具和技术，并找到公式的更简单形式（左手）。为此，我看了Z3的Python接口，试图看看我可以摆脱它。因此，定义混淆的公式是这样完成的：x + y == (x ^ y) + 2 * (x & y)
simplify简化此函数：>>> from z3 import *
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> fun1 = (x ^ y) + 2 * (x & y)
不是很令人信服...但是，让我们尝试证明与
x + y的等效性：>>> simplify((x ^ y) + 2 * (x & y))
(x ^ y) + 2*~(~x | ~y)
我添加了如果结果为负数，则表明还可以取消公式的资格。未知公式，其中包含一系列简单而又常用的公式。但是，这种方式对我而言似乎效率极低。我想我缺少一些更智能的算法来简化公式。
我想知道是否已经存在一些比蛮力方法更有效的工具或知名技术。因此，如果有人对此有任何提示或评论，那将是非常受欢迎的。
#1 楼
Z3是SMT求解器。它的工作是确定用户传递的公式的可满足性，其中公式可以混合Z3支持的各种理论中的术语。巧合的是，为了通过产生比用户传递的公式更简单的公式使自己的工作更容易，它实现了一种简化器，该简化器在技术上不是很复杂，并且主要由术语重写规则组成。 />尽管用户可以对两个表达式的等价性提出疑问，但Z3唯一涉及的就是求解公式。即Z3不会为您生成候选人。提供用户并查询SMT求解器的可满足性是您的用户职责。一般来说，合成函数是程序合成中的一项艰巨任务。这些查询自然是在二阶逻辑中提出的，但是现代的SMT求解器仅支持一阶逻辑的限制。为了避免这个问题，一些已发表的工作采取了将大多数候选对象排除在外的途径，从而使等价查询的数量保持较小。例如，参见本文或本论文。另一种方法是指定一个模板，描述允许候选函数看起来像什么。本文是一个简单的例子。这些方法可以使公式保持一阶逻辑，甚至不需要量词。
通常，您应该研究程序合成。
评论
尝试help_simplify（）-一些选项可能会满足您的需求。我已经尝试了其中几种策略（simplify（fun1，som = True）），但均未成功。也许我错过了正确的使用策略。如果您有这样的清单，很高兴知道您的建议！
问题不是很清楚。 “有效”是什么意思，什么使“无效”简化？
你是对的。我的意思是要比蛮力方法更有效，在蛮力方法中，您将所有公式与要调查的公式进行比较。