Optimize model generation in CVC5 and Bitwuzla

[daniel-raffler]

Hello,

this PR tries to optimize model generation in CVC5 and Bitwuzla. Both solvers are somewhat special in that they have no way to get the model directly. Instead, we have to build the model ourselves by first collecting all defined symbols, and then having those symbols evaluated by the solver to get the assignments for the model. Currently we're using mgr.extractVariablesAndUFs() to get the symbols for the model from the asserted formulas. Benchmarking has shown this operation to be surprisingly expensive, with the call to mgr.extractVariablesAndUFs() making up 3/4 of the time spent on model generation. On closer inspection there appear to be two reasons for this:

• First of all, mgr.extractVariablesAndUFs() uses a Visitor, which adds some additional overhead, such as getting the Sort for a term, that isn't needed when only looking for defined symbols
• Second, these additional operations are particularly expensive on CVC5/Bitwuzla, due to the way these solvers manager their objects. As an example, when returning the 2nd child of a Term, CVC5 will first wrap the corresponding Node of the child in a new Term object, which then has to be wrapped by a Java proxy, which is then added to the abstractPointer queue for garbage collection at the end of the program. Since the initial C++ proxy is always new, this has to be done every time, even if the Term/Sort is already known to us

In this PR we avoid the problem by collecting the symbols for the model directly in the solver API, without resorting to a Visitor. In microbenchmarks this leads to a speedup of 4 for CVC5 and 2 for Bitwuzla, while memory usage was reduced by 50% and 30% respectively. Numbers were less impressive when looking at svcomp results for unreach-call, but the number of correct results on CVC5 increased from 8031 to 8115, while saying mostly flat for Bitwuzla. (I believe the reason the difference is less clear for Bitwuzla, is that it does not support interpolation, which may rule out many runs that require a lot of model generation)

On CVC5 the difference is large enough to show up in the plots:

However, overall the effect is still smaller than expected

[kfriedberger]

The code for model generation in CVC5 (and other solvers) was simplified and optimized in the last year (for example in PRs like #539 and #551) from a potentiallly exponential runtime to near-linear runtime in size of the asserted formulas. This PR seems to go one step further and bring some more optimizations here, including both, memory and cpu usage.

Even an evaluation is provided in the PR. 👍
I have not evaluated by myself, but the PR looks promising. ✅

Could you also take a look at CVC4? It works quite similar to CVC5 and we might want to keep the code similar.

[daniel-raffler]

Could you also take a look at CVC4? It works quite similar to CVC5 and we might want to keep the code similar.

Thanks for the hint! I've included CVC4 now