非线性算法的Z3性能

我认为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程序的使用时间更长了，可能有多种类似的假设。通常，验证似乎根本没有终止。

有任何想法吗？

最佳答案

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

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

关于非线性算法的Z3性能，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/12511503/