feat: implement predicate and assumption solving in python wrapper

[maartenflippo]

Assumption solving in the Rust layer currently performs semantic minimisation of the core. E.g. if the assumptions contain [y <= 1] and [y != 0], and the domain of y starts at 0, then the core may contain [y == 1] rather than the original predicates in the assumptions.

[EmirDe]

I am wondering if this may be unexpected from the user side. They may expect that the core is just a subset of the assumptions.

Related to this, if we would do core lifting somehow, that also might be unexpected from the user.

I suppose this means that the definition of a core as the subset of assumption is not proper?

Could be useful to check with Ignace for instance?

[ImkoMarijnissen]

I think it would be better if we simply do not perform semantic minimisation when extracting cores

[maartenflippo]

After some exploration, I found that disabling semantic minimisation of the core is more tricky than anticipated. This is because the solver splits up equality literals, and we rely on semantic minimisation to merge those.

We should create a separate PR that fixes the issues with core extraction and minimisation, rather than shoe-horn it into this one.

dissenting opinion