Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unexpected huge performance difference between solver using "default" tactic, Z3_mk_solver() and Z3_mk_simple_solver() #1035

Closed
delcypher opened this issue May 22, 2017 · 11 comments

Comments

@delcypher
Copy link
Contributor

commented May 22, 2017

I'm currently investigating queries that Z3 is taking a very long time to solve in my tool and I ran into one that Z3 is handling in a surprising way.

This is the query

(declare-fun f_ackermann!0 () (_ BitVec 64))
(assert
 (not (fp.isNaN ((_ to_fp 11 53) f_ackermann!0))))
(assert
 (let ((?x8 ((_ to_fp 11 53) f_ackermann!0)))
(let ((?x18 (fp.sqrt roundNearestTiesToEven (fp.mul roundNearestTiesToEven ?x8 ?x8))))
(let ((?x24 (fp.mul roundNearestTiesToEven ?x18 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))))
(let ((?x11 (fp.abs ?x8)))
(let (($x20 (or (fp.isNaN (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64)))) (fp.isNaN ?x18))))
(let (($x22 (or $x20 (fp.gt (fp.mul roundNearestTiesToEven ?x11 ((_ to_fp 11 53) (_ bv4607092346807469998 64))) ?x18))))
(not (or $x22 (or (or (fp.isNaN ?x11) (fp.isNaN ?x24)) (fp.lt ?x11 ?x24)))))))))))
(check-sat)

In my tool libz3 is taking ~1679 seconds to solve this. When I give this query to the Z3 binary it is solving the query in ~2 seconds.

I started digging into this and by making my tool increase libz3's verbosity it looks like the slow smt tactic is being used when my tool uses libz3.

(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 4)
(smt.searching)
(smt.simplifying-clause-set :num-deleted-clauses 30)
...

but when Z3 binary solves the query a different tactic is being used.

(sat.sat-solver)
(sat.simplify)
(sat-restart :conflicts 202 :decisions 677 :restarts 1 :clauses 185638 :learned 159 :gc-clause 0 :memory 46.75 :time 1.35)
(sat-restart :conflicts 303 :decisions 1100 :restarts 2 :clauses 185638 :learned 246 :gc-clause 0 :memory 46.75 :time 1.36)
...

In my tool I use the Z3_mk_simple_solver() to create the solver which I expected (maybe this is my mistake?) to have the same performance as the Z3 binary if no explicit tactic is requested and no logic is set. However it seems this is not the case at all.

To investigate some more I tried creating the Z3 solver instance in two different ways in my tool

  • replacing Z3_mk_simple_solver() with Z3_mk_solver()
  • Explicitly create the default tactic and make a solver from that, i.e. like this
    theTactic = Z3_mk_tactic(builder->ctx, "default");
    Z3_tactic_inc_ref(builder->ctx, theTactic);
    theSolver = Z3_mk_solver_from_tactic(builder->ctx, theTactic);

In both cases these changes to my tool caused performance to improve dramatically on these queries. Looking at the verbose output it seems when I instantiate Z3's solver this way it looks like the much faster sat.sat-solver tactic gets used.

So why is this happening? I would have expected Z3_mk_simple_solver() to behave like the Z3 binary does when no logic is provided and no tactic is supplied.

To help you reproduce this I'm attaching z3_interaction.zip (Z3 interaction log) and
solver-queries.core_solver.aa.smt2.txt (also a log of queries issued to Z3 in SMT-LIBv2.5 format).

Warning the interaction log has

  • Multiple contexts. One is used for solving, the other is just used for logging queries to a text file.
  • Sets verbosity to 0

CC: @ccadar @danielschemmel

@delcypher delcypher changed the title Unexpected huge performance different between solver using "default" tactic, Z3_mk_solver() and Z3_mk_simple_solver() Unexpected huge performance difference between solver using "default" tactic, Z3_mk_solver() and Z3_mk_simple_solver() May 22, 2017

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 22, 2017

I forgot to mention.

Z3 revision: b782ec3

@wintersteiger

This comment has been minimized.

Copy link
Member

commented May 22, 2017

Usually, Z3 will try to detect the logic (here) and then run a specialized tactic for the problem. This is what happens when the default tactic is used (declared here). If none of those logic checks succeed, it will call the smt tactic (here). On this particular problem, the fpa2bv and bit-blaster tactics are executed (among others) before handing the problem to the SAT solver. This is "eager", everything is translated into SAT and we use a SAT solver to decide the problem.

However, when the smt tactic is used the approach is "lazy": nothing is done up front and only during the search, when things become relevant, they are translated (for the case of the FP logic, see here) or otherwise instantiated. This is what the "simple" solver does; it provides a direct path to the SMT solver without any tactics being involved.

The solver obtained via mk_solver is a much more complicated one (here); it constructs a combined_solver that switches to the SMT solver if it sees incremental commands, otherwise it uses tactics (which may finally also result in running the SMT solver). Setting the verbosity to -v:15 should print lines beginning with (combined-solver ... to tell you which one of them is used.

Usually, we would expect that specialized tactics are better at solving their respective problems, but that's of course not always true.

In this particular case, you should also see that Z3 switches to the SMT solver when one of the FP operations requires uninterpreted functions (e.g., fp.to_ubv when hi_fp_unspecified=false, default setting may change depending on upcoming modifications to the SMT FP standard). In this case, the goal will still contain uninterpreted functions after fpa2bv and bit-blaster have translated everything they can translate, and so we can't use the SAT solver. (In this case, that check is here and there are similar ones in other tactics.)

A minor note: the "default" tactic tries to detect the logic after running the simplifier (see here). So, when it doesn't detect a matching logic, it will run the "smt" tactic on the simplified goal; so in these cases the actual tactic that gets executed is (then simplify smt) instead of just smt.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 23, 2017

@wintersteiger Thanks for the detailed response.

However, when the smt tactic is used the approach is "lazy": nothing is done up front and only during the search, when things become relevant, they are translated (for the case of the FP logic, see here) or otherwise instantiated. This is what the "simple" solver does; it provides a direct path to the SMT solver without any tactics being involved.

Is the smt tactic an implementation of what's described in "
Simplification by Cooperating Decision Procedures" by Nelson and Oppen? Sorry if this is a dumb question. I don't know that much about how SMT solvers are actually implemented.

I didn't realise this is what the "simple" solver did. I thought it was just like Z3_mk_solver() except that the simplifier tactic was applied first.

I think the doxygen documentation on Z3_mk_solver() and Z3_mk_simple_solver() could be greatly improved. Your description of what these functions actually do does not seem to match the current documentation.

Currently the docs say

/**
       \brief Create a new (incremental) solver. This solver also uses a
       set of builtin tactics for handling the first check-sat command, and
       check-sat commands that take more than a given number of milliseconds to be solved.

       \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
       Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.

       def_API('Z3_mk_solver', SOLVER, (_in(CONTEXT),))
    */
    Z3_solver Z3_API Z3_mk_solver(Z3_context c);

    /**
       \brief Create a new (incremental) solver.

       The function #Z3_solver_get_model retrieves a model if the
       assertions is satisfiable (i.e., the result is \c
       Z3_L_TRUE) and model construction is enabled.
       The function #Z3_solver_get_model can also be used even
       if the result is \c Z3_L_UNDEF, but the returned model
       is not guaranteed to satisfy quantified assertions.

       \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
       Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.

       def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
    */
    Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
  • The docs say that Z3_mk_solver() gives an incremental solver but this doesn't seem to always be the case.
  • The docs don't say what Z3_mk_simple_solver() does.

Fixing the descriptions here would hopefully prevent others from making my mistake.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 23, 2017

@wintersteiger
Based on your description it sounds like using either the default tactic or using Z3_mk_solver() would be suitable for my use case. I don't use Z3 in an incremental manner so it looks like Z3_mk_solver() would end up using the default tactic because it doesn't pass a logic to mk_smt_strategic_solver_factory().

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 23, 2017

@wintersteiger If you'd like me to have a go at rewriting the documentation for Z3_mk_solver() and Z3_mk_simple_solver() based on this discussion let me know and I'll have a go.

delcypher added a commit to delcypher/klee that referenced this issue May 24, 2017
[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses klee#653. We still need to try rolling our
own custom tactic.

[1] Z3Prover/z3#1035
delcypher added a commit to delcypher/klee that referenced this issue May 25, 2017
[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses klee#653. We still need to try rolling our
own custom tactic.

[1] Z3Prover/z3#1035
delcypher added a commit to delcypher/klee that referenced this issue May 26, 2017
[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses klee#653. We still need to try rolling our
own custom tactic.

[1] Z3Prover/z3#1035
@wintersteiger

This comment has been minimized.

Copy link
Member

commented May 26, 2017

Sure! We should definitely add a better definition of "simple" :-)

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented May 29, 2017

@wintersteiger Okay. I'm pretty busy right now but when I have some free time I'll tackle this.

delcypher added a commit to klee/klee that referenced this issue Jun 1, 2017
[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses #653. We still need to try rolling our
own custom tactic.

[1] Z3Prover/z3#1035
ddcc added a commit to ddcc/clang that referenced this issue Jun 5, 2017
[analyzer] Change default solver used by z3
Use combined tactic/SMT solver instead of simple SMT-only solver. Improved performance, see Z3Prover/z3#1035.
delcypher added a commit to delcypher/z3 that referenced this issue Jun 11, 2017
[Doxygen] Rewrite documentation of `Z3_mk_solver()` and
`Z3_mk_simple_solver()` to try to make it clearer what the differences
are between these APIs.

This an attempt to address issues noted in Z3Prover#1035.
@rainoftime

This comment has been minimized.

Copy link

commented Jun 15, 2017

@delcypher From my own experience, the qfbv_tactic(eager encoding to sat, see z3/src/tactic/smtlogics/qfbv_tactic.cpp) based solver(what Z3_mk_solver() returns in your case) is usually faster than the smt_tactic(DPLL(T)-style lazy approach) based solver.

@rainoftime

This comment has been minimized.

Copy link

commented Jun 15, 2017

@delcypher Another tactic z3 uses to solver QF_BV constraints is called inc_sat_solver(see z3\src\sat\sat_solver\inc_sat_solver.cpp), which is same as qfbv_tactic, but has simpler preprocessings.

@wintersteiger

This comment has been minimized.

Copy link
Member

commented Sep 15, 2017

Can we close this issue or is there still something remaining to do?

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Sep 18, 2017

There's nothing else to do. Closing.

@delcypher delcypher closed this Sep 18, 2017

ccadar added a commit to ccadar/klee that referenced this issue Oct 4, 2018
[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses klee#653. We still need to try rolling our
own custom tactic.

[1] Z3Prover/z3#1035
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.