Imperative API

[Stevendeo]

Tackles #899 by making both Sat API imperative.

• The imperative is made... well, imperative; it still relies on Satml_frontend for properly wrapping calls to Satml. We should be able to merge them, but I choosed not to in this PR to avoid spaghettification.
• The functional sat now has an imperative frontend upadting a reference to the environment.

[Stevendeo]

There is a test that does not pass on the CI, but it works on my side...

[Stevendeo]

The test does not seem to be executed with make runtest, when I play it manually it does not pass on my side as well.

[bclement-ocp]

This looks reasonable except for the change in step limit which is a bit worrying. Maybe we should run benches on ae-format just to check that everything is A-OK before merging?

[bclement-ocp]

Hm, that is surprising… This may indicate that the change is not as innocuous as we thought — unless this is the weak table somehow?

[bclement-ocp]

Can you explain why this is moved here and why it is correct? Is it related to the test failure you observed?

[Stevendeo]

In the old version, if acc is empty, the objective update will not be taken into account because an I_dont_know exception is raised. It only is otherwise that the objectives must be updated.

[bclement-ocp]

In the old version, env.objectives is a reference that is shared across all versions of env (including the one in unknown_exn), so in fact the objectives should still get updated even though that is confusing control flow. Is this the change that fixes the test failure?

[Stevendeo]

Oh you're right I forgot it was a reference; and no, it is not what fixes the test failure.

[Halbaroth]

Actually the goal of this reference isn't to be able to retrieve objectives (currently, objectives are stored in a struct from Models.ml and the reference last_saved_model gives us access to them) but to keep in mind we're exploring branches beyond SAT because we're looking for a better model during the optimization. If we got an unsat answer in this context, it means the last attempt to improve the model failed but the previous one is correct and we have to return unknown for the frontend. The critical code is here:

   | IUnsat (env, _) as e ->
     if !(env.objectives) == None then raise e;
     (* TODO: put the correct objectives *)
     raise (I_dont_know env)

[bclement-ocp]

Oh you're right I forgot it was a reference; and no, it is not what fixes the test failure.

Well don't leave us hanging — what did, then?

[Halbaroth]

Probably the worst way to write for loops now :) but I agree that getting ride of this heresy is out of the scope of this PR.

[Stevendeo]

Well don't leave us hanging — what did, then?

Just a let env = that I forgot to replace by its proper side effect; the heuristic mechanism that forces the Normal strategy depends on a counter (last_forced_normal) that is reinitialized every time it triggers. The counter was not reinitialized, and the force normal behavior was looping. I am not sure of the details regarding the raised exception though, maybe there is a subtle bug hiding behind this. All I managed to find is that the culprit was the first assertion of Satml.update_lazy_cnf, which triggers when trying to add twice the same formula in the environment (also, there is a generic exception catcher in satml_frontend that breaks my callstack and I really want to remove it).

[bclement-ocp]

Ah, you must have changed it in a force push then, which is why I didn't see it. The question was mostly to know if it was a simple omission or if there was some trickery involved, looks like it is the first case if there was a let env = { env with xxx } in lying around. Please run ae-format benches then we should be good to merge!

there is a generic exception catcher in satml_frontend that breaks my callstack and I really want to remove it

Yeah, this assert false is regularly annoying, we should just re-raise the exception there instead I guess, would be happy to accept a PR that does this.

[Stevendeo]

Yeah, this assert false is regularly annoying, we should just re-raise the exception there instead I guess, would be happy to accept a PR that does this.

Wouldn't that break the callstack as well? I would rather remove this catch (or replace it with the actual exception that are raised by the wrapped function).

[bclement-ocp]

Wouldn't that break the callstack as well? I would rather remove this catch (or replace it with the actual exception that are raised by the wrapped function).

No, OCaml should properly preserves the call stack when re-raising exceptions.

[Stevendeo]

Now I'm thinking of it, maybe the exception was changed to an assert false is due to the fact that it may raise other exception (I_dont_know, Sat) that could be catched at a higher level. If we are sure it is not the case, why not just removing this code?

[bclement-ocp]

Now I'm thinking of it, maybe the exception was changed to an assert false is due to the fact that it may raise other exception (I_dont_know, Sat) that could be catched at a higher level. If we are sure it is not the case, why not just removing this code?

As a matter of fact I don't think we are sure that is not the case (it shouldn't be the case but… bugs exist I guess). In this case, the proper thing to do would be to raise an error (from the Errors module) instead (raising from within an exception handler, rather than asserting, should also preserve the call stack).

Or we could keep the assert false but add the backtrace to the debug message (using Printexc.get_backtrace ()), which maybe is the better solution.

[bclement-ocp]

Benches look good — let's merge. Thanks!