Dolmen named formulae

[Stevendeo]

Updates the handling of named formulas with the latest Dolmen update

[Gbury]

If I read the code correctly, you currently treat all implicit definitions as named definitions, which happens to be the case currently, but may change in the future. It would be better to lookup the named tag on the id being defined to determine whether it comes from a :named annotation.

[bclement-ocp]

Looks good; please just update the code with @Gbury's remark

[bclement-ocp]

Suggested change

	| _ -> assert false (* Implicit definitions are epected to be definitions *)
	| _ -> assert false (* Implicit definitions are expected to be definitions *)

[bclement-ocp]

Actually it looks like there are still issues with the assignments/models that need to be investigated.

[Stevendeo]

It would be better to lookup the named tag on the id being defined to determine whether it comes from a :named annotation.

Okay I get it, thanks! Why does the string attached to the :named tag does not hold the term name? Or in other words, why does DStd.Expr.Id.get_tag id DStd.Expr.Tags.named returns Some "" for named formulae?

[Gbury]

Okay I get it, thanks! Why does the string attached to the :named tag does not hold the term name? Or in other words, why does DStd.Expr.Id.get_tag id DStd.Expr.Tags.named returns Some "" for named formulae?

Well, because the term name is already in the name of the constant. Part of the reason/problem is that other languages (ae's native iirc) have a slightly different notion of named which attach a string to an expression, which is why historically, the named tag uses a string. However, in the case of smtlib, the named annotation creates a new constant, and it seemed better to use an empty string to prevent people from wrongly assuming that they should use the string payload, where instead they should use the constant's name.

That begin said, this is admittedly not ideal, and it could be changed.

[Stevendeo]

Actually it looks like there are still issues with the assignments/models that need to be investigated.

Fixed, but it required some changes on how get_value is called.

[bclement-ocp]

We should check implicit rather than depend on the fact that all statements but the last are implicit (or at the very least, if we do depend on that, there should be a comment explaining this).

Also it looks like there are weird things happening with get_value — shouldn't we always be able to get the value of the assignments now that there are actual terms associated with them? But it looks like we still reply unknown all the time, which is not very useful — can you investigate? This might get out of scope for this PR, so feel free to open an issue instead.

[Stevendeo]

But it looks like we still reply unknown all the time, which is not very useful — can you investigate?

I already did actually, and my conclusion is that these assignments are not always put in the gamma map as is, which is the actual data get_value works with. @Halbaroth is working on some stuff about the model's API and I wanted to wait for his work before further investigation.

[bclement-ocp]

I already did actually, and my conclusion is that these assignments are not always put in the gamma map as is, which is the actual data get_value works with. @Halbaroth is working on some stuff about the model's API and I wanted to wait for his work before further investigation.

This should be unrelated to the model API stuff. I just looked at the code; it should be correct for the Fun_sat solver, but looking in gamma for Satml_frontend is not correct (the two solvers are structured very differently), we need to call SAT.boolean_model and extract the assignment from there. So really this is just #937 and unrelated to this PR then.

[bclement-ocp]

Please rebase to fix the merge conflicts and then we should be ready to merge.

[Stevendeo]

This should be unrelated to the model API stuff.

The function get_value is not named get_assignments because I had in mind this function would handle the get-value instruction which requires the models.