Performance problem with Solver.translate()

[CanCebeci]

I've been experimenting with incrementalism in the context of symbolic execution using z3 (Python API). When forking a state, I use Solver.translate() to clone the solver instead of creating a new solver instance and copying all the constraints, as suggested in #556. I've surprisingly observed that Solver.translate() is much slower than the latter approach. Could you help me understand why that is?

[NikolajBjorner]

Solver.translate does not copy the original constraints, it copies constraints after pre-processing. It also copies learned lemmas with high glue levels and it copies model reconstruction instructions. These three elements can each contribute to overhead beyond the original set of constraints but they should not outright lead to drastic slow-downs.
The main way the reconstruction stack can grow to something larger than the original constraints if the solver applies variants of blocked clause elimination or variable elimination that involves several clauses.
The mundane reasons for slowdowns are typically performance bugs (code bugs) that apply naive algorithms for copying state. It is easier to get an idea of what is going on with something concrete.

[NikolajBjorner]

Do you have any repro or were you able to gain insights based on the above comment?

[CanCebeci]

Sorry for the delayed reply. You can find here 12 instances I've come upon where translate is significantly slower.

Unzipping and running reproduce_clone.py should suffice. Hope this helps.

[NikolajBjorner]

Thanks, the repro is useful. It uses the files in an essential way. I pushed an update that addresses a main perf bottleneck.