Z3 中的 TryFor 在给定的时间限制后不会停止检查答案

【问题标题】：TryFor in Z3 does not stop checking after the given timelimitZ3 中的 TryFor 在给定的时间限制后不会停止检查
【发布时间】：2012-08-09 01:43:09
【问题描述】：

我正在使用 Z3 的 .NET API。当我通过调用实例化求解器时：

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit));

并为某些型号的语句设置一个 60 秒（60000 毫秒）的 TimeLimit

s.Check()

60 秒后不返回。对于某些型号，它会在几秒钟后返回，在我的情况下这不是问题，但对于某些型号，它根本不会返回（我在 3 天后取消了该过程）。

如何强制 Z3 在给定时间限制后停止检查？

【问题讨论】：

标签： .net z3

【解决方案1】：

TryFor 组合器是使用“取消”标志实现的。新战术反应迅速，并在设置“取消”标志时很快终止。不幸的是，通用策略smt 是通用求解器的封装。这个通用求解器反应不灵敏。它可能在几个关键地方“丢失”：量词实例化、Simplex 等。qflia 策略建立在 smt 和许多其他策略之上。因为，您正在尝试解决无量词问题。我假设smt 策略在 Simplex 模块内部的循环中。 smt 策略中的 Simplex 模块是使用任意精度有理数实现的。因此，对于非平凡的线性实数/整数问题，它可能非常耗时。

您无法解决此问题。如果你真的需要一个强有力的运行时间保证，我看到的唯一解决方案是创建一个运行 Z3 的单独进程，并在需要更多 k 秒来解决问题时终止它。

话虽如此，Z3 的未来版本将拥有一个全新的算术模块。当取消标志设置时，这个新模块（如新战术）将迅速终止。

【讨论】：