TryFor in Z3 does not stop checking after the given timelimit

Question

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));

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

s.Check()

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).

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

Answer 1

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.

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.

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.