z3 python solver copying

[bannsec]

Another question regarding my use of z3 in the python script symbolic execution engine. In longer examples of the engine, the script spends much of it's time re-creating the z3 solver when it state splits. My current implementation simply instantiates a new solver, and then copies over all the solver.assertions(). The obvious slowdown here is that I'm asking z3 the solve something it has already solved. This becomes a more serious problem (exponential in some cases) when it gets deeper into execution.

Is there any way to copy the solver without having this overhead?

[wintersteiger]

No there isn't, but you can use the incremental solving facilities for this purpose, i.e., solve with assumptions or push/pop parts of your problem.

For examples, see here (they are in C++, but the function names are the same/very similar in Python).

[NikolajBjorner]

There is also the translate method (Z3_solver_translate or Solver.translate) that lets you clone a solver. This may work for your scenario.

[bannsec]

Nikolaj,

I think what you're talking about is what I'm trying to do. However, when I attempt that I get an error that I don't understand "translation of contexts is only supported at base level".

[NikolajBjorner]

This would mean that you did a push. You have to pop back everything.