The current implementation of `maximize` and `minimize` isn't satisfying in
the native language. As this feature have never been released and MERCE prefers
using the SMT-LIB format, we remove the support of optimization in the native
language.

This PR refactors the way we manage optimization constraints in
Alt-Ergo.

- Optimization constraints aren't tag on subformulas anymore. Instead
  we use the MaxSMT syntaxes.
- We don't support optimization in Alt-Ergo native format. As this
  feature haven't been published, we don't need to deprecated it.
- We support `maximize`, `minimize` and `get-objectives`. There is no
  support for `assert-soft`. I think it's out of the scope of this PR.
- The SAT solver API exposes two new functions: `optimize` and
  `get_objectives` which, respectively, register objective function and
  return the current objective model.
- The objective values are expressions.

The optimization constraint is wrong if we use it in incremental
mode but it's safe if we use `maximize` and `minimize` at the top level
only.

The value produced by `middle_value` in `intervalCalculus` wasn't
propagate to the CC(X) module in `look_for_sat`. We propagate it now.

I also modify the test `arith7.optimize.smt2` as we cannot use both
incremental mode and optimization constraints.

We don't support yet impure terms or formulae in `maximize` and
`minimize` statements. Let's print a warning message and ignoring
invalid objective functions.

Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com>

Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com>

Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com>