具有非线性算术的Z3性能

Question

我们遇到了性能问题,我认为是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程序可以使用更长的时间,可能有类似的多种假设.通常,验证似乎根本没有终止.

有任何想法吗？

Answer 1

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

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