TryFor在Z3不会停止给定的时限后检查 [英] TryFor in Z3 does not stop checking after the given timelimit

问题描述

我使用Z3的.NET API。当我实例化一个求解器调用：

I am using the .NET API of Z3. When I instantiate a solver by calling:

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

和给它60秒（60000毫秒）的一些车型时限声明

and give it a TimeLimit of 60 seconds (60000 milliseconds) for some models the statement

s.Check()

60秒后没有返回。对于某些型号后来返回了几秒钟，这在我的情况就不会是一个问题，但对于某些机型，它不返回在所有（我取消后3天的过程）。

does not return after 60 seconds. For some models it returns a few seconds later, which in my case would not be a problem, but for some models it doesn't return at all (I cancelled the process after 3 days).

我怎么能强迫Z3停止给定的时限后检查？

How can I force Z3 to stop checking after a given timelimit?

推荐答案

在 TryFor 组合子使用的是取消的标志来实现。新的战术是非常敏感，并终止速度非常快的时候，取消标志设置。不幸的是，通用战术 SMT 是一个包装在一个通用的解决者。这种通用求解器是不是很敏感。在几个关键的地方，它可以得到丢失：量词实例，单等。 qflia 战术是建立在 SMT 和许多其他的战术。因为，你正在试图解决量词无问题。我假设 SMT 的策略是在单模块的内部循环。在 SMT的单模块战术是利用任意precision有理数实现。因此，它可能是耗费非平凡线性实/整数问题非常时间

The TryFor combinator is implemented using a "cancellation" flag. The new tactics are very responsive, and terminate very quickly when the "cancellation" flag is set. Unfortunately, the general purpose tactic smt is a wrapper over a general purpose solver. This general purpose solver is not very responsive. It can get "lost" in several key places: quantifier instantiation, Simplex, etc. The qflia tactic is built on top of the smt and many other tactics. Since, you are trying to solve quantifier-free problems. I'm assuming that the smt tactic is in a loop inside of the Simplex module. The Simplex module in the smt tactic is implemented using arbitrary precision rational numbers. Thus, it may be very time consuming for non-trivial linear real/integer problems.

没有太多可以做，以解决此问题。如果你真的需要在运行时间了有力的保障，我看到的唯一解决方案是创建运行Z3一个单独的进程，并杀死它，只要它需要更多的 K 秒来解决一个问题。

There is not much you can do to workaround this issue. If you really need a strong guarantee in running time, the only solution I see is to create a separate process running Z3, and kill it whenever it takes more the k seconds to solve a problem.

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

That being said, future versions of Z3 will have a complete new arithmetic module. This new module (like the new tactics) will terminate quickly when the cancellation flag is set.

这篇关于TryFor在Z3不会停止给定的时限后检查的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！