5

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

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，此时它放弃了。

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

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

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

使验证很快终止。

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

有任何想法吗？

4

1 回答 1

3

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

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

于 2012-09-21T15:33:24.507 回答