I am currently using the Z3 C ++ API to solve requests on bitvectors. Some queries may contain an existential quantifier at the top level.
Often eliminating the quantifier is simple and can be done quickly by the Z3. However, in cases where the elimination of the quantifier returns to listing thousands of possible solutions, I would like to stop this tactic and process the request myself in a different way.
I tried wrapping the qe tactic with try-for tactics, hoping that if the quantifier exception failed (say 100 ms), I would know that it would be better to process the request in a different way. Unfortunately, the “try-for” tactic does not cancel the elimination of the quantifier (for any time reference).
An old post discusses a similar issue, and the smt tactics are accused of not responding. Does the same reasoning apply to qe tactics? The same post indicates that future versions should be more responsive. Is there any way or heuristic to determine if the elimination of the quantifier will be long (in addition to launching the solver in a separate thread and killing it during a timeout)?
I have attached a minimal example so you can try:
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!
source
share