z3 - 术语重写在位向量算术的决策程序中的使用

Question

我正在从事一个项目，该项目的重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对某些决策程序(例如基于位爆破的决策程序)的先行步骤很有用。重写一词可能根本解决了这个问题，或者产生了一个简单得多的等效问题，因此，两者的结合可以大大提高速度。

我知道许多SMT求解器都采用这种策略(例如Boolector，Beaver，Alt-Ergo或Z3)，但是很难找到详细描述这些重写步骤的论文/技术报告/等。总的来说，我只发现了几篇文章中作者描述了这种简化步骤的论文。我想找到一些文档详细解释术语重写的用法:提供规则示例，讨论AC重写和/或其他方程式公理的便利性，重写策略的使用等。

现在，我只是找到了技术报告A Decision Procedure for Fixed-Width Bit-Vectors，其中描述了CVC Lite执行的标准化/简化步骤，我想找到更多类似的技术报告!我还找到了有关Term rewriting in STP的海报，但这只是一个简短的摘要。

我已经访问了那些SMT求解器的网站，并在他们的出版物页面中进行了搜索...

我将不胜感激，或者对当前版本的著名SMT求解器中如何使用术语重写的任何引用或任何解释。我对Z3特别感兴趣，因为Z3似乎是最聪明的简化阶段之一。例如，Z3 3. *引入了新的位向量决策过程，但是不幸的是，我找不到任何描述它的论文。

Answer 1

我同意你的看法。很难找到描述现代SMT求解器中使用的预处理步骤的论文。
大多数SMT求解器开发人员都同意，这些预处理步骤对于位矢量理论非常重要。
我认为这些技术之所以未发布，有几个原因:大多数是一些小技巧，它们本身并不是重大的科学贡献；大多数技术仅在特定系统的上下文中起作用；在求解器A上似乎很好用的一种技术，在求解器B上无效。
我相信拥有开源SMT解决方案是解决此问题的唯一方法。即使我们发布了特定求解器A中使用的技术，也很难在没有看到其源代码的情况下重现求解器A的实际行为。

无论如何，这是Z3执行的预处理的摘要，以及重要的细节。

几个简化规则可以在本地减小此大小，但在全局范围内增大它。简化器必须避免这种简化引起的内存消耗。您可以在以下位置找到示例:http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf

简化的第一步仅执行保留等效性的局部简化。
示例:

2*x - x ->  x 
x and x -> x

接下来，Z3执行恒定传播。给定相等的t = v，其中v是一个值。它将t替换为v。

t = 0 and F[t]  -> t = 0 and F[0]

接下来，它对位向量执行高斯消除。但是，仅消除在算术表达式中最多出现两次的变量。
此限制用于防止公式中加法器和乘法器数量的增加。
例如，假设我们有x = y+z+w，并且x出现在p(x+z)，p(x+2*z)，p(x+3*z)和p(x+4*z)处。然后，在消除了x之后，我们将得到p(y+2*z+w)，p(y+3*z+w)，p(y+4*z+w)和p(y+5*z+w)。尽管我们删除了x，但比原始公式有更多的加法器。

接下来，它消除了不受约束的变量。 Robert Brummayer和Roberto Brutomesso的博士学位论文描述了这种方法。

然后，执行另一轮简化。这次，执行局部上下文简化。
这些简化可能非常昂贵。因此，使用了要访问的最大节点数阈值(默认值为1000万)。
本地上下文简化包含诸如

之类的规则

(x != 0 or  y = x+1) ->  (x != 0 or y = 1)

接下来，它尝试使用分布性来最小化乘法器的数量。示例:

ab + ac -> (b+c)*a

然后，它尝试通过应用关联性和可交换性来最小化加法器和乘法器的数量。
假设公式包含术语a + (b + c)和a + (b + d)。然后，Z3将它们重写为:(a+b)+c和(a+b)+d。
转换之前，Z3必须编码4个加法器。之后，由于Z3使用完全共享的表达式，因此仅需要编码三个加法器。

如果公式仅包含等于，串联，提取和类似运算符。然后，Z3使用基于联合查找和同余闭合的专用求解器。

否则，它将对所有内容进行位爆炸，使用AIG最小化 bool 公式，然后调用其SAT求解器。