使用非线性算术的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似乎有办法实例化许多术语，而不是很快失败，因为它的内存消耗相当快地增长到大约300MB，在这一点上它放弃了。

我想知道这是不是一个bug，或者是否有可能改进启发式方法，以确定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中非线性算术推理的次数来避免不可终止性。对于每个Z3查询，选项NL_ARITH_ROUNDS=100最多使用非线性模块100次。这不是一个理想的解决方案，但至少，我们避免了非终止性。