在位向量算术决策过程中使用术语重写
我正在开展一个项目，其重点是使用术语重写来解决/简化固定大小的位向量算术问题，这对于某些决策过程（例如基于位爆破的决策过程）的前一步很有用。术语重写可能会根本解决问题，或者以其他方式产生更简单的等效问题，因此两者的结合可以带来相当大的加速。
我知道许多 SMT 求解器都实现了这种策略（例如 Boolector、Beaver、Alt-Ergo 或 Z3），但很难找到详细描述这些重写步骤的论文/技术报告/等。一般来说，我只找到作者在几段中描述此类简化步骤的论文。我想找到一些详细解释术语重写的使用的文档：提供规则示例，讨论AC重写和/或其他方程公理的便利性，重写策略的使用等。
目前，我刚刚找到了技术报告固定宽度位向量的决策过程，其中描述CVC Lite 执行的规范化/简化步骤，我想找到更多像这样的技术报告！我还找到了一张关于STP 中的术语重写的海报，但这只是一个简短的摘要。
我已经访问过这些 SMT 求解器的网站，并且在他们的出版物页面中进行了搜索...
我将不胜感激任何参考资料，或者任何关于如何在当前版本的 Well- 中使用术语重写的解释。已知的 SMT 求解器。我对 Z3 特别感兴趣，因为它看起来拥有最智能的简化阶段之一。例如，Z3 3.* 引入了一种新的位向量决策过程，但不幸的是，我找不到任何描述它的论文。
I am working on a project whose focus is the use of term rewriting to solve/simplify fixed-size bit-vector arithmetic problems, which is something useful to do as a prior step to some decision procedure such as those based on bit-blasting. The term rewriting may solve the problem at all, or otherwise produce a much simpler equivalent problem, so the combination of both can result in a considerable speed-up.
I am aware that many SMT solvers implement this strategy (e.g. Boolector, Beaver, Alt-Ergo or Z3), but it is being hard to find papers/tech-reports/etc in which these rewriting steps are described in detail. In general, I only found papers in which the authors describe such simplification steps in a few paragraphs. I would like to find some document explaining in detail the use of term rewriting: providing examples of rules, discussing the convenience of AC rewriting and/or other equational axioms, use of rewriting strategies, etc.
For now, I just have found the technical report A Decision Procedure for Fixed-Width Bit-Vectors which describes normalization/simplification steps performed by CVC Lite, and I would like to find more technical reports like this one! I have also found a poster about Term rewriting in STP but it is just a brief summary.
I have already visited the websites of those SMT solvers and I have searched in their Publications pages...
I would appreciate any reference, or any explanation of how term rewriting is being used in current versions of well-known SMT solvers. I am specially interested in Z3 because it looks to have one of the smartest simplification phases. For instance, Z3 3.* introduced a new bit-vector decision procedure but, unfortunately, I was not able to find any paper describing it.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
我同意你的看法。很难找到描述现代 SMT 求解器中使用的预处理步骤的论文。
大多数 SMT 求解器开发人员都认为这些预处理步骤对于位向量理论非常重要。
我相信这些技术没有发表有几个原因：它们中的大多数都是一些小技巧，它们本身并不是重大的科学贡献；大多数技术仅在特定系统的上下文中起作用；似乎在求解器
A上效果很好的技术，在求解器B上不起作用。我相信拥有开源 SMT 求解器是解决这个问题的唯一方法。即使我们发布特定求解器 A 中使用的技术，在不查看其源代码的情况下也很难重现求解器 A 的实际行为。
不管怎样，这里是 Z3 执行的预处理的总结，以及重要的细节。
几个简化规则，可能会局部减小此大小，但会全局增加它。简化者必须避免这种简化导致的内存爆炸。您可以在以下位置找到示例： http://research.microsoft.com /en-us/um/people/leonardo/mit2011.pdf
第一个简化步骤仅执行保留等价性的局部简化。
示例：
t = v，其中v是一个值。它将所有地方的t替换为v。接下来，它对位向量执行高斯消除。但是，仅消除算术表达式中最多出现两次的变量。
此限制用于防止公式中加法器和乘法器的数量增加。
例如，假设我们有
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 万）。
局部上下文简化包含诸如
之类的规则。
然后，它尝试通过应用结合性和交换性来最小化加法器和乘法器的数量。
假设公式包含项
a + (b + c)和a + (b + d)。然后，Z3会将它们重写为：(a+b)+c和(a+b)+d。在转换之前，Z3 必须对 4 个加法器进行编码。之后，由于 Z3 使用完全共享的表达式，因此只需要对三个加法器进行编码。
如果公式仅包含相等、串联、提取和类似运算符。然后，Z3 使用基于并查和同余闭包的专用求解器。
否则，它会对所有内容进行位爆炸，使用 AIG 来最小化布尔公式，并调用其 SAT 求解器。
I agree with you. It is hard to find papers describing the preprocessing steps used in modern SMT solvers.
Most SMT solver developers agree that these preprocessing steps are very important for the Bit-Vector theory.
I believe these techniques are not published for several reasons: most of them a little tricks that by themselves are not a significant scientific contribution; most of the techniques only work in the context of a particular system; a technique that may seem to work very well on solver
A, does not work on solverB.I believe that having open source SMT solvers is the only way to address this issue. Even if we publish the techniques used in a particular solver
A, it would be very hard to reproduce the actual behavior of solver A without seeing its source code.Anyway, here is a summary of the preprocessing performed by Z3, and important details.
Several simplification rules, may reduce this size locally, but increase it globally. A simplifier must avoid the memory blowup caused by this kind of simplification. You can find examples at: http://research.microsoft.com/en-us/um/people/leonardo/mit2011.pdf
The first simplification step only performs local simplifications that preserve equivalence.
Examples:
t = vwherevis a value. It replacesteverywhere withv.Next, it performs Gaussian elimination for Bit-Vectors. However, only variables that occur at most twice in arithmetical expressions are eliminated.
This restriction is used to prevent an increase of the number of adders and multipliers in your formula.
For example, suppose we have
x = y+z+wandxoccurs atp(x+z),p(x+2*z),p(x+3*z)andp(x+4*z). Then, after eliminatingx, we would havep(y+2*z+w),p(y+3*z+w),p(y+4*z+w)andp(y+5*z+w). Although we eliminatedx, we have more adders than the original formula.Next, it eliminates unconstrained variables. This approach is described by in the PhD thesis of Robert Brummayer and Roberto Brutomesso.
Then, another round of simplification is performed. This time, local contextual simplifications are performed.
These simplifications are potentially very expensive. So, a threshold on the maximal number of nodes to be visited is used (the default value is 10million).
Local context simplification contain rules such as
Then, it tries to minimize the number of adders and multipliers by applying associativity and commutativity.
Suppose the formula contains the terms
a + (b + c)anda + (b + d). Then, Z3 will rewrite them to:(a+b)+cand(a+b)+d.Before the transformation, Z3 would have to encode 4 adders. After, only three adders need to be encode since Z3 uses fully shared expressions.
If the formula contains only equality, concatenation, extraction and similar operators. Then, Z3 uses a specialized solver based on the union-find and congruence closure.
Otherwise, it bit-blasts everything, uses AIGs to minimize the Boolean formula, and invokes its SAT solver.
Z3 使用重写来进行预处理期间执行的许多简化。以下论文详细描述了用于 UFBV 策略（带有量词）的许多重写规则：
Wintersteiger、Hamadi、de Moura：有效求解量化位向量公式， FMCAD，2010
Z3 uses rewriting for many the simplification performed during pre-processing. Many of the rewrite rules used for the UFBV strategy (with quantifiers) are described to some detail in the following paper:
Wintersteiger, Hamadi, de Moura: Efficiently Solving Quantified Bit-Vector Formulas, FMCAD, 2010