4
votes

I'm currently using the Z3 C++ API for solving queries over bitvectors. Some queries may contain an existential quantifier at the top level.

Often times the quantifier elimination is simple and can be performed by Z3 quickly. However, in those cases where the quantifier elimination falls back to enumerating thousands of feasible solutions I'd like to abort this tactic and handle the query myself in some other way.

I've tried wrapping the 'qe'-tactic with a 'try-for'-tactic, hoping that if quantifier elimination fails (in say 100ms) I'd know that I'd better handle the query in some other way. Unfortunately, the 'try-for'-tactic fails to cancel the quantifier elimination (for any time bound).

In an old post a similar issue is discussed and the 'smt' tactic is being blamed for being not responsive. Does the same reasoning apply to the 'qe' tactic? The same post indicates that 'future' versions should be more responsive though. Is there any way or heuristic to determine whether quantifier elimination would take long (besides running the solver in a separate thread and killing it on timeout)?

I've attached a minimal example so you can try it yourselves:

z3::context ctx;

z3::expr bv1 = ctx.bv_const("bv1", 10);
z3::expr bv2 = ctx.bv_const("bv2", 10);
z3::goal goal(ctx);
goal.add(z3::exists(bv1, bv1 != bv2));

z3::tactic t = z3::try_for(z3::tactic(ctx,"qe"), 100);    
auto res = t.apply(goal);
std::cout << res << std::endl;

Thanks!

1

1 Answers

1
votes

The timeout cancellations have to be checked periodically by the tactic that is running. We basically have to ensure that the code checks for cancellations and does not descend into a long running loop without checking. You can probably identify the code segment that fails to check for cancellation by running your code in a debugger, break and then determine which procedures it is in. Then file a bug on GitHub to have cancellation flag checked in the place that will help. Overall, the quantifier elimination tactic is currently fairly simplistic when it comes to bit-vectors so it would be better to avoid qe for all but simple cases.