Split abduction solver from SmtEngine (#4733)

Split abduction solver from SmtEngine (#4733)

This splits everything related to abducts into its own standalone module, AbductionSolver.

It furthermore converts some of the interfaces of SmtEngine to make them take Node instead of Expr (this will be done for every method eventually).

The code for interpolation should follow a similar pattern, e.g. InterpolantSolver.