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.

[filipeom]

I'm also having this issue when trying to run cvc5 in ECMA-SL. There seems to be few things cvc5 doesn't support (or maybe I haven't implemented yet). So this issue is not limited to smtzilla. I think smtml in general should have better support for this.

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?

I feel like we already know which ones aren't supported/implemented. We can just look at the bindings and see what has an assert false/failwith? Ideally, we would let the type system tell us this. I was thinking of a way to propagate this information even to the API (typed.ml). I feel it should be possible with phantom types/GADTs. I'll try to do a quick mvp