Consistent speed-up of incremental solver (2) used in non-incremental way

[sreeshmaheshwar]

TL;DR: I've observed consistent and substantial speed-ups of Z3's (4.8.12, QF_ABV) incremental solver (that is, solver2) on a set of 12 non-incremental benchmark SMT-LIB2 outputs (each containing several independent queries - see sample files at bottom) produced by a symbolic execution engine, that seem to indicate that, oddly, solver2 should be preferred entirely for our use case despite the non-incremental setting.

I'm working on a symbolic execution engine and noticed unexpected speed-ups using a single push before a query and a single pop after - to confirm the result from the solver's perspective, I extracted the .smt2 interaction from our benchmarks and manually compared the performance of the original with the file transformed in this way to enable solver2. For example, I compared the performance of

(declare-fun n_args_0 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select n_args_0 #x00000003)
                   (concat (select n_args_0 #x00000002)
                           (concat (select n_args_0 #x00000001)
                                   (select n_args_0 #x00000000))))))
  (not (not (bvult a!1 #x00000002)))))
(check-sat)
(reset)

(declare-fun n_args_0 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select n_args_0 #x00000003)
                   (concat (select n_args_0 #x00000002)
                           (concat (select n_args_0 #x00000001)
                                   (select n_args_0 #x00000000))))))
  (bvult a!1 #x00000002)))
(assert (let ((a!1 (concat (select n_args_0 #x00000003)
                   (concat (select n_args_0 #x00000002)
                           (concat (select n_args_0 #x00000001)
                                   (select n_args_0 #x00000000))))))
  (not (bvslt #x00000000 a!1))))
(check-sat)
(reset)

...

with

(push)
(declare-fun n_args_0 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select n_args_0 #x00000003)
                   (concat (select n_args_0 #x00000002)
                           (concat (select n_args_0 #x00000001)
                                   (select n_args_0 #x00000000))))))
  (not (not (bvult a!1 #x00000002)))))
(check-sat)
(pop)

(push)
(declare-fun n_args_0 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select n_args_0 #x00000003)
                   (concat (select n_args_0 #x00000002)
                           (concat (select n_args_0 #x00000001)
                                   (select n_args_0 #x00000000))))))
  (bvult a!1 #x00000002)))
(assert (let ((a!1 (concat (select n_args_0 #x00000003)
                   (concat (select n_args_0 #x00000002)
                           (concat (select n_args_0 #x00000001)
                                   (select n_args_0 #x00000000))))))
  (not (bvslt #x00000000 a!1))))
(check-sat)
(pop)

...

If my high-level understanding of Z3's incremental behaviour is correct, the pops here should cause the solver to "forget" what it has learnt since the corresponding push, meaning it should not benefit from incrementality over these queries. Indeed, simply comparing combined_solver.ignore_solver1 being false vs true (with the original) yields similar results (a 2x speed-up on average), though not as dramatic.

Results: the push/pop run outperformed the original on every .smt2 benchmark, taking 37% of the time that solver1 did on average (exact results here). This was very (pleasantly!) surprising - I'd expect either similar performance or the opposite given the discussions in #1141 and #501. Moreover, I am yet to find smt.random_seeds (as suggested in #1143) that cause solver2 to outperform solver1 (though I haven't investigated this thoroughly given that conclusiveness of these results make me doubt that this is the cause - maybe I should?).

A couple of questions:

1. Can anyone shed light on (or point me to code that concerns) differences between the two solvers that could cause such results? I've heard about preprocessing/inprocessing differences between the two, for example. EDIT: I tried running a couple of the more costly individual queries verbosely - it seems that the time overhead of solver1's preprocessing is not the underlying cause.
2. Has anyone else observed similar results (or perhaps switched to solver2 either entirely or with a timeout in light of similar observations) / identified the nature of queries that would cause solver2 to outperform solver1 in this way?
3. Am I correct in thinking that surrounding independent queries with push/pop in this way disallows profiting from incrementality between them, or is the incremental solver's learning unaffected by these APIs?

Examples (shortened): basic-smt2.txt, push-pop-smt2.txt.

I'd be very grateful for any help - thank you!

[sreeshmaheshwar]

I was wrong about (3) in the general case - https://stackoverflow.com/a/40427658. Unsure how relevant that is here though, given these aren't "pure bit-vector problems"; I don't see delegation to a SAT solver when running a handful of the queries verbosely. An incremental engine that doesn't garbage collect lemmas would explain the speed-up of surrounding queries with push/pop over running the original queries with combined_solver.ignore_solver1=true though (but that the latter outperforms solver1 would still be unexplained).

[NikolajBjorner]

If we profile the slow version, we see that it spends quite some overhead in setting up a fresh state.
The effect of "reset" is to clear all state that was associated with the previous commands.
There is also different behavior with respect to pre-processing. check-sat from scratch uses a richer set of pre-processing simplifications that can have their own overhead. This is not directly visible in the stack below, but may in general play a role (some of the queries do take notable time, for reasons that are not visible from the global analysis).

Function Name	Total CPU [unit, %]	Self CPU [unit, %]	Module
| - main	208648 (99.97%)	0 (0.00%)	z3
| - read_smtlib2_commands	208648 (99.97%)	0 (0.00%)	z3
| - parse_smt2_commands	208646 (99.97%)	0 (0.00%)	z3
| - smt2::parser::operator()	208644 (99.97%)	8 (0.00%)	z3
| - smt2::parser::parse_cmd	208636 (99.96%)	32 (0.02%)	z3
| - cmd_context::check_sat	101804 (48.78%)	2 (0.00%)	z3
| - solver::check_sat	101173 (48.47%)	3 (0.00%)	z3
| - solver_na2as::check_sat_core	101152 (48.46%)	1 (0.00%)	z3
| - `anonymous namespace'::tactic2solver::check_sat_core2	101147 (48.46%)	11 (0.01%)	z3
| - smt2::parser::parse_declare_fun	80467 (38.55%)	2 (0.00%)	z3
| - smt2::parser::sort_stack	80311 (38.48%)	9 (0.00%)	z3
| - binary_tactical::cleanup	57878 (27.73%)	471 (0.23%)	z3
| - check_sat	52828 (25.31%)	12 (0.01%)	z3
| - exec	52509 (25.16%)	2 (0.00%)	z3
| - cmd_context::init_manager_core	46731 (22.39%)	3 (0.00%)	z3
| - th_rewriter::imp::imp	44523 (21.33%)	31 (0.01%)	z3
| - cmd_context::mk_solver	44521 (21.33%)	7 (0.00%)	z3
| - smt_strategic_solver_factory::operator()	44513 (21.33%)	10 (0.00%)	z3

[dong-yf]

Excuse me, by the way, how to generate a table like this?

[NikolajBjorner]

open visual studio, run profiling.

If you don't have VS, there is perf and gperf.