smtzilla: make sur we don't dispatch unsupported operations to some solvers?

[redianthus]

Hi,

Let's take the example of ext_rotate. I think only Z3 supports it.
Thus, when a query contains such an operator, we should only send it to Z3.
Maybe we should have such a list somewhere and use it in SMTzilla to make sure we don't send unsupported queries to some solvers?

cc @hra687261, I'm curious to hear your thoughts about it.
I'm also thinking the work of @amenahh could help us making such a list?
Moreover, we could start by only making the list for QF_BVFP which is what is needed in Owi, that could be a good first step! :)

[hra687261]

Oh definitely, even more generally, we don't want to dispatch to a solver queries containing logics it does not support.
Most SMT solvers support a defined set of logics +- some specific symbols, so we could imagine storing that information in the solver's module, then having a function that takes a query and returns of list of solvers that support it.