reset() vs new Solver

[ritam9495]

I am using the Z3 API for python for satisfiability check given a set of constrains. Suppose I have two set of constrains. Should I have two separate Solver() for the two or should I create one, check it, use the reset() and then add the constrains for the second one and check it!
Which one should be faster and why?

[nunoplopes]

That is a complicated topic. BTW there's more than just the solvers; there's also the global caches and symbol tables that Z3 preserves in across solvers. So you need to delete the context and reset the memory (Z3_reset_memory()) once in a while. How often? Depends on your application, if it creates many symbols with different names or not, does it create a lot of expressions that are discarded later? That's a bit of trial and error.
(FYI Z3 doesn't delete internalized strings, like function names. you need to reset memory to get rid of those)

A new Solver() vs reset? These are very similar. reset() should be slightly faster as some tactics know how to reuse previous memory allocations. The global memory reset has a much more noticeable impact.

[ritam9495]

I am observing almost 20% increase in the execution time when I use reset() compared to new Solver() every time. Can this be possible? or am I doing something wrong?

Also, using Z3_reset_memory() is giving me an exception Process finished with exit code 139 (interrupted by signal 11: SIGSEGV)

[NikolajBjorner]

There is overhead setting up a solver. If queries are small, this overhead dominates.

Resetting memory from managed interfaces, e.g., Python, Java, C#, Ocaml,
is not practical because of interactions with GC and global objects.
Resetting memory from plain C/C++ remains possible.

[ritam9495]

Is there a chance that the overhead for reset() dominates, given the queries are complex enough involving a large number of variables? How does this overhead compare to the one for setting up the solver?

[nunoplopes]

No, that can't be. Python has huge overheads in creating & deleting expressions, but not with resetting solvers.
Also, your formulas need to be super complicated before you can measure any time spent by Z3 as Python usually dominates 🤣

[nunoplopes]

If you really need speed, you can't use Python. Python is slow and Z3's Python API is super slow. You can't use it to create thousands of expressions.