具有非线性算术的 Z3 性能 [英] Z3 Performance with Non-Linear Arithmetic

问题描述

我们遇到了性能问题，我认为是 Z3 处理非线性算术的部分.这是一个简单的具体 Boogie 示例，当使用 Z3(版本 4.1)进行验证时，需要很长时间(大约 3 分钟)才能完成.

We are running into performance problems with what I believe is the part of Z3 that treats non-linear arithmetic. Here is a simple concrete Boogie example, that when verified with Z3 (version 4.1) takes a long time (on the order of 3 minutes) to complete.

const D: int;
function f(n: int) returns (int) { n * D }

procedure test() returns ()
{
  var a, b, c: int;
  var M: [int]int;
  var t: int;

  assume 0 < a && 1000 * a < f(1);
  assume 0 < c && 1000 * c < f(1);
  assume f(100) * b == a * c;

  assert M[t] > 0;
}

问题似乎是由函数的相互作用、整数变量的范围假设以及(未知)整数值的乘法引起的.最后的断言不应该是可证明的.Z3 似乎并没有很快失败，而是有办法以某种方式实例化大量项，因为它的内存消耗相当快地增长到大约 300 MB，此时它放弃了.

It seems that the problem is caused by an interaction of functions, range assumption on integer variables as well as multiplications of (unknown) integer values. The assertion in the end should not be provable. Instead of failing quickly, it seems that Z3 has ways to instantiate lots of terms somehow, as its memory consumptions grows fairly quickly to about 300 MB, at which point it gives up.

我想知道这是否是一个错误，或者是否有可能改进 Z3 何时应该停止在它当前试图解决问题的特定方向上的搜索的启发式方法.

I'm wondering if this is a bug, or whether it is possible to improve the heuristics on when Z3 should stop the search in the particular direction it is currently trying to solve the problem.

一个有趣的事情是通过使用内联函数

One interesting thing is that inlining the function by using

function {:inline} f(n: int) returns (int) { n * D }

使验证很快终止.

背景:这是我们在验证器 Chalice 中看到的问题的最小测试用例.在那里，Boogie 程序变得更长，可能有多个类似的假设.通常，验证似乎根本没有终止.

Background: This is a minimal test case for a problem that we see in our verifier Chalice. There, the Boogie programs get much longer, potentially with multiple assumptions of a similar kind. Often, the verification does not appear to be terminating at all.

有什么想法吗?

推荐答案

是的，非终止是由于非线性整数运算.Z3 有一个新的非线性求解器，但它用于非线性实数算术"，并且只能用于仅使用算术的无量词问题(即，没有像您的示例中那样的未解释函数).因此，您的示例中使用了旧的算术求解器.该求解器对整数算术的支持非常有限.你对问题的分析是正确的.Z3 很难找到非线性整数约束块的解.请注意，如果我们将 f(100) * b == a * c 替换为 f(100) * b <= a * c，则 Z3 立即返回未知"的答案.

Yes, the non-termination is due to nonlinear integer arithmetic. Z3 has a new nonlinear solver, but it is for "nonlinear real arithmetic", and can only be used in quantifier free problems that only use arithmetic (i.e., no uninterpreted functions like in your example). Thus, the old arithmetic solver is used in your example. This solver has very limited support for integer arithmetic. Your analysis of the problem is correct. Z3 has trouble finding a solution for the block of nonlinear integer constraints. Note that if we replace f(100) * b == a * c with f(100) * b <= a * c, then Z3 returns immediately with an "unknown" answer.

我们可以通过限制 Z3 中非线性算术推理的次数来避免非终止.选项 NL_ARITH_ROUNDS=100 将为每个 Z3 查询最多使用 100 次非线性模块.这不是一个理想的解决方案，但至少，我们避免了非终止.

We can avoid the non-termination by limiting the number of nonlinear arithmetic reasoning in Z3. The option NL_ARITH_ROUNDS=100 will use the nonlinear module at most 100 times for each Z3 query. This is not an ideal solution, but at least, we avoid the non-termination.

这篇关于具有非线性算术的 Z3 性能的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！