Further refactoring of set defaults for incompatibility methods (#7072)

Further refactoring of set defaults for incompatibility methods (#7072)

This introduces standard methods for checking incompatible with models, unsat-cores, incremental, proofs.

There is one minor change in behavior in this PR.When bitblast=eager and models were enabled in combined logics, then the set defaults would change the bitblast mode to lazy. However, it would then in the same block complain that eager cannot be used in combination with incremental. After this PR, we won't complain in this case since we've already decided to change the bitblast mode to lazy.