Add assertion levels in SatML

[Halbaroth]

Satml_frontend assumes that assume and check_sat are always called on a SatML environment with no prior decisions. It works in the current codebase because, in the presence of pop/push, we always restart from a fresh environment.

This PR is a preparation for #1288.

The assertion:

assert (SAT.decision_level env.satml == 0)

is replaced with:

assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml)

Notice that we cannot enforce the assertion:

assert (SAT.decision_level env.satml = SAT.assertion_level env.satml)

Consider for instance:

let env = SAT.env () in
SAT.push env 1;
SAT.assume env f; (* <--- HERE *)
...

Internally, SAT.assume env f adds the formula g => f into the environment of SatML where g is a guard formula introduced in SAT.push. But SatML.assume does not decide the guard formula g, so the decision level is 0 but the assertion level is 1. Guards are decided (with the highest priority) in SatML.solve, and is called by SAT.unsat.

I didn't add the new assertion into SAT.assume_th_elt because this function is only used for handling the theory concept in native language and we always invoke it at the assertion level 0.