z3 low performance

[apach301]

We have a QF_BV formula from symbolic execution tool which solved in z3 much slower than other formulas. Average time of solving of path_predicate.txt is 11-12min (checked z3 versions 4.8.6, 4.8.7 and 4.8.9). There are a 3 conjuncts that cause such performance regression: path_predicate_sliced.txt. Solving these conjuncts separately or in combinations of 2 is relatively fast (<5s).

What can be the reason of such performance regression? Is it a z3 issue, improper symbolic interpretation or just complex formula? Other solvers (yices, stp) process this formula quite fast.

[rainoftime]

When I change the last line of https://github.com/Z3Prover/z3/files/5194831/path_predicate.txt to

(check-sat-using (then simplify solve-eqs bit-blast sat))

Z3 can also solve the instance quickly.

@NikolajBjorner I noticed that the qfbv tactic uses solve-eqs a bit conservatively, but many other tactics do not.

    // conservative gaussian elimination.
    solve_eq_p.set_uint("solve_eqs_max_occs", 2);
    ...
    using_params(mk_solve_eqs_tactic(m), solve_eq_p),

Perhaps it could be performance detrimental for some instances?

[NikolajBjorner]

thanks for taking a closer look at chiming in.

We could of course, try with different settings of this particular configuration parameter across SMT benchmarks and see. It seems indeed to become truly trivial after proper pre-processing. For example, this one also works for me; z3 path_predicate_sliced.txt tactic.default_tactic="(and-then simplify propagate-values solve-eqs propagate-values bit-blast smt)" and some variants.

Yet, overall, solve_eqs needs to be much more systematic than it is right now in order to support better common heuristics. So the current best way is to force users into low level tweaking. Perhaps there is some general lesson about pre-processing at the AIG level here, but I don't have bandwidth to look closer right now. It's very good to have perf discrepancies reported, but time to analysis is arbitrary long.

[rainoftime]

Interestingly, after bit-blasting, the tactic solve-eqs also works fine. After the modification below, z3 can solve the instance quickly.

                when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
                              // try not seting local_ctx_p for solve_eqs 
                              //and_then(using_params(and_then(mk_simplify_tactic(m),
                              //                               mk_solve_eqs_tactic(m)),
                              //                      local_ctx_p),
                                     and_then(using_params(mk_simplify_tactic(m),
                                              local_ctx_p), mk_solve_eqs_tactic(m),

[apach301]

Thank you for the replies.

Seems like using simplify and bit-blast tactics improves performance of solving. Also tried solve-eqs, aig, propagate-values but can't say about their impact on performance. Can you suggest what other z3 tactics we should use for solving such QF-BV formulas, generated from symbolic execution? And is qfbv tactic (mentioned by @rainoftime) applied automatically for the QF-BV formula or it should be specified separately?

Also i am wondering why it takes so long to process this particular formula - is it bvmul/bvlshr operations or something else?

[rainoftime]

qfbv tactic is applied automatically for non-incremental QF-BV formulas (no push/pop operations; one check-sat, one formula). It is already a combination of several small tactics (e.g., propagate-values, conservative solve-eqs, bit-blast, aig, sat, etc)

If your queries are all non-incremental, I guess qfbv should work well for most cases. Other tactics such as (check-sat-using (then simplify solve-eqs bit-blast sat)) or other SMT solvers may also have some "shortcomings" (an example of CVC4 https://github.com/CVC4/CVC4/issues/4936)

[apach301]

Yes, all queries are non-incremental and almost all solved by default z3 solver quite fast. But on some rare formulas like this solver gets stuck (despite it applies qfbf tactics by default). Even with patch https://github.com/Z3Prover/z3/issues/4683#issuecomment-690142571 z3 can't solve it at acceptable time.

Guess I will use manually configured tactics as it works good and fast on formulas.