feat: exporting alt-ergo FPA built-in primitives

[Stevendeo]

Issue #873

[bclement-ocp]

I don't think we should change the datatype constructor names depending on the input format, that is somewhat brittle (e.g. now reasoning depends on the input format, which it wasn't before and they should really be independent) and the benefits (strict backward compatibility) don't seem worth the cost.

We do need to use the SMT-LIB names for models, but I don't think we really need the "native" names for anything beyond parsing. Can we just change the names to the SMT-LIB ones ("RNE", etc.) for the ADT constructor names (so they are used for printing) and otherwise define the AE names (NearestTiesToEven etc.) and the SMT constants (roundNearestTiesToEven etc.) as aliases in the parser?

[bclement-ocp]

Why nested caches, and why is the rounding mode argument not cached? For multiple arguments it is better to cache a tuple:

with_cache ~cache:(Hashtbl.create 13) (fun (n, m, rm) -> ...)

[bclement-ocp]

It is somewhat confusing that ae.round becomes SMTFloat, would probably deserve an explanatory comment here.

[bclement-ocp]

Maybe IndexedFloat would be a better name here (SMTFloat seems to imply that this is related to SMT-LIB somehow where it's not)

[Stevendeo]

I can use AERound to be sure

[bclement-ocp]

Please don't blanket open DT — it shouldn't be needed here, and Dolmen has many functions with the same names in different modules, using qualified names help (if only a bit) follow what we are doing.

[Stevendeo]

I just refactored some code and this let open was copied from below (or above).

[bclement-ocp]

Ah, you are right — but before it was scoped to the inside of a let fpa_builtins statement, while now it "leaks" into the whole function :)

[Stevendeo]

I don't think we should change the datatype constructor names depending on the input format, that is somewhat brittle (e.g. now reasoning depends on the input format, which it wasn't before and they should really be independent) and the benefits (strict backward compatibility) don't seem worth the cost.
We do need to use the SMT-LIB names for models, but I don't think we really need the "native" names for anything beyond parsing. Can we just change the names to the SMT-LIB ones ("RNE", etc.) for the ADT constructor names (so they are used for printing) and otherwise define the AE names (NearestTiesToEven etc.) and the SMT constants (roundNearestTiesToEven etc.) as aliases in the parser?

I would agree to break the backward compatibility if I was sure Why3 did not have drivers for these problems. I would rather not have aliases in the parser though, as we don't want conflicts between identifiers.

I am not sure why you find this solution brittle though, the input format specifies straightforwardly the constructor names. If there are multiple input formats, it sounds consistent to have multiple manners to handle built-in values.

[bclement-ocp]

I would agree to break the backward compatibility if I was sure Why3 did not have drivers for these problems. I would rather not have aliases in the parser though, as we don't want conflicts between identifiers.

Sorry, i said "parser" but meant "typer" (i.e. D_cnf here). I meant adding aliases in the same way you already do in the PR with the RoundNearestToEven etc. builtins from Dolmen (you can think of it as defining transparent constants for each of the constructor names; this is already the case for the SMT-LIB format in Dolmen -- see here).

Can you clarify what you mean by "Why3 did not have drivers for these problems"? I am not suggesting we change the syntax of the native format in any way, if that was not clear, and adding extra builtins will not break Why3 because we now allow user-defined functions to shadow builtins.

I am not sure why you find this solution brittle though, the input format specifies straightforwardly the constructor names. If there are multiple input formats, it sounds consistent to have multiple manners to handle built-in values.

We have support for problems that combine input files in different formats using preludes (and we use preludes for FPA). Now we need to think very hard about where we call get_input_format and whether that might or might not have changed since parsing. In fact, I thought that your implementation was doing the right thing in this case due to dispatching on Options.get_input_format (which, for the record, I think we should avoid as much as possible, since, again, reasoning should not depend on the input format), but in fact in D_cnf there is no dispatching on Options.get_input_format, and so using a .ae prelude with a .smt2 file will break.

All of this is only an issue because fpa_rounding_mode is a term-level ADT for historical reasons, and unfortunately we do depend on this for reasoning. If it was properly designed, there would only be the fpa_rounding_mode ADT at the OCaml level, and the only distinction would be in the printers — but alas, we do currently depend on the term-level names for printing, which is unfortunate.

[bclement-ocp]

I would agree to break the backward compatibility if I was sure Why3 did not have drivers for these problems. I would rather not have aliases in the parser though, as we don't want conflicts between identifiers.

To be clear: as far as I know, the only backwards compatibility we would be breaking is that we would have different debug messages.

[bclement-ocp]

I was focused on the cache earlier, but: ae.round should only have two indexed identifiers; the rounding mode argument should be an actual term-level argument (in the same way that in the FloatingPoints SMT-LIB theory only the bit widths are indexed).

[Stevendeo]

Okay, I did not understood your remark ; I thought you were asking to alias the Smtlib2 & the legacy identifiers. In any case, we have to test which identifier to use given the input language at some point to select which constructor is valid. Take const_view in expr.ml for example : from a hstring, we need to know which rounding mode to use.

using a .ae prelude with a .smt2 file will break.

I tested the new feature with the .ae preludes and it worked just fine.

[bclement-ocp]

Okay, I did not understood your remark ; I thought you were asking to alias the Smtlib2 & the legacy identifiers. In any case, we have to test which identifier to use given the input language at some point to select which constructor is valid. Take const_view in expr.ml for example : from a hstring, we need to know which rounding mode to use.

I am saying that we should have a single hstring per identifier so that we do not have to do that dispatch. And yes, I am saying we should alias the SMT-LIB and legacy identifiers, in the sense that I am saying Alt-Ergo should behave in the native format as if we had:

type RoundingMode = RNE | RTZ | ...
type fpa_rounding_mode = RoundingMode
logic ToEven : fpa_roundingMode = RNE
...

Well, to be fair, we don't actually have to expose RoundingMode and RNE etc. constructors to the user, we could just expose the constants. I don't really like this, either, but it allows a correct solution without introducing too much complexity at the cost of slightly worse debug messages.

using a .ae prelude with a .smt2 file will break.

I tested the new feature with the .ae preludes and it worked just fine.

Maybe I should have been more precise what I meant by "break", so let me clarify. Here is the same file in both formats, float.smt2 and float.ae, that Alt-Ergo should be able to prove unsat (or Valid) in both cases (this is an instantiation of an axiom in the fpa prelude):

The SMT2 version:

; float.smt2
(set-logic ALL)
(declare-const x Real)
(assert (<= 1.0 x))
(assert (not (<= ((_ ae.round 4 4) RNE 1.0) ((_ ae.round 4 4) RNE x))))
(check-sat)

The native version:

(* float.ae *)
logic x : real
axiom ax : 1.0 <= x
goal g : float(4, 4, NearestTiesToEven, 1.0) <= float(4, 4, NearestTiesToEven, x)

Running next on float.smt2 does not make sense because the ae.round identifier does not exist there. But running float.smt2 or float.ae with the FPA preludes on your branch should do the same thing, and it should be unsat (this is an instantiation of one of the prelude axioms). Here is what I observe on next:

$ alt-ergo --enable-theories fpa float.ae
File "float.ae", line 4, characters 1-82: Valid (0.7564) (13 steps) (goal g)

However here is what I observe on your branch:

$ alt-ergo --enable-theories fpa  float.ae
[Debug][Satml_frontend][unsat]         
Failure("unsupported constant: NearestTiesToEven")
Fatal error: exception File "src/lib/reasoners/satml_frontend.ml", line 1207, characters 6-12: Assertion failed
$ alt-ergo --enable-theories fpa -i native float.ae
File "float.ae", line 4, characters 1-82: Valid (0.4636) (13 steps) (goal g)
$ alt-ergo --enable-theories fpa float.smt2
                                       
; File "float.smt2", line 5, characters 1-12: I don't know (0.4565) (4 steps) (goal g_1)

unknown

I was actually surprised by the first one, I expected it to work, but it didn't, because when Options.get_input_format is specifically the input format that was requested by the user on the command line, never the input format that we inferred from the file name.

Anyways, this is the sort of things I had in mind when saying that the implementation is brittle. While we could fix these specific issues, we would always risk introducing new ones by mistake when changing the parsers and/or option handling, and it would be highly preferable to use a solution that is by design immune to this sort of shenanigans.

(It also shows that we don't nearly have enough FPA tests in the test suite ;) )

[Stevendeo]

I am saying that we should have a single hstring per identifier so that we do not have to do that dispatch. And yes, I am saying we should alias the SMT-LIB and legacy identifiers, in the sense that I am saying Alt-Ergo should behave in the native format as if we had:

type RoundingMode = RNE | RTZ | ...
type fpa_rounding_mode = RoundingMode
logic ToEven : fpa_roundingMode = RNE
...

I was thinking the other way round : we don't want the fpa_rounding_mode to be accessible in SMT2.

Well, to be fair, we don't actually have to expose RoundingMode and RNE etc. constructors to the user, we could just expose the constants. I don't really like this, either, but it allows a correct solution without introducing too much complexity at the cost of slightly worse debug messages.

I am not sure to understand your point here... Why not exposing them? Do you want to change how these constants are handled (i.e. not as constructors, but as constants) ?

The input file issue is troubling though, you're right.

[bclement-ocp]

I am saying that we should have a single hstring per identifier so that we do not have to do that dispatch. And yes, I am saying we should alias the SMT-LIB and legacy identifiers, in the sense that I am saying Alt-Ergo should behave in the native format as if we had:

type RoundingMode = RNE | RTZ | ...
type fpa_rounding_mode = RoundingMode
logic ToEven : fpa_roundingMode = RNE
...

I was thinking the other way round : we don't want the fpa_rounding_mode to be accessible in SMT2.

We don't have to, and we have a lot of flexibility here: the definition of the ADT and the identifiers we expose to the user for each language are all completely distinct. In fact, we could define the ADT internally using arbitrary constructor names and the user would be none the wiser — except that the constructor names for the ADT end up in debug messages and in models, which is why I was saying that we had to use SMT2 names for it (because models are always using the SMT2 syntax).

Well, to be fair, we don't actually have to expose RoundingMode and RNE etc. constructors to the user, we could just expose the constants. I don't really like this, either, but it allows a correct solution without introducing too much complexity at the cost of slightly worse debug messages.

I am not sure to understand your point here... Why not exposing them? Do you want to change how these constants are handled (i.e. not as constructors, but as constants) ?

As I state above: the constructors as objects and the environment binding them to names are completely separate. So we could have RNE, etc. as constructors, but only expose them in the user environment as NearestTiesToEven. It will behave exactly the same (think exception NearestTiesToEven = RNE or type t += NearestTiesToEven = RNE in OCaml), because this is about name binding, not variable binding. What I am not sure is if we want to only expose the name NearestTiesToEven, or to also allow users to use RNE as a name to refer to the same constructor.

The reason to allow RNE in the AE format is that now debug messages and models would use RNE instead of NearestTiesToEven, and it would be somewhat confusing that those name don't work in the input problem. The reason to not allow RNE in the AE format is so that we don't change the initial environment for AE files (the goal is to add support for round in the SMT-LIB format, no reason it should change things for the AE format). I don't have a strong opinion either way, but my preference would go to not changing the environment (so only exposing the NearestTiesToEven name in AE format, not RNE) because while it is easy to add stuff to the initial environment, it is harder to remove from it once people start using the stuff that was added.

[Stevendeo]

We don't have to, and we have a lot of flexibility here: the definition of the ADT and the identifiers we expose to the user for each language are all completely distinct. In fact, we could define the ADT internally using arbitrary constructor names and the user would be none the wiser — except that the constructor names for the ADT end up in debug messages and in models, which is why I was saying that we had to use SMT2 names for it (because models are always using the SMT2 syntax).

Okay, so what you propose is to change the fpa_rounding_type to not be an alt-ergo enum, but a special type defining 5 constants? If we build them at parsing, we forbid the user to overload this type (which can be a good thing actually) or we must be careful to match the cases in the right order ; if we do it at typechecking, we lose the file format we were working on.

I'm sorry if I make you repeat, I have a hard time understanding your answers here.

[bclement-ocp]

Okay, so what you propose is to change the fpa_rounding_type to not be an alt-ergo enum, but a special type defining 5 constants? If we build them at parsing, we forbid the user to overload this type (which can be a good thing actually) or we must be careful to match the cases in the right order ; if we do it at typechecking, we lose the file format we were working on.

Here is what I propose:

• In Fpa_rounding, we define the fpa_rounding_mode semantically. There is only one ADT definition in Fpa_rounding. What I mean by semantically is that this behaves as the following ADT::

  type _fpa_rounding_mode = _RNE | _RNA | _RTP | _RTN | _RTZ
  

  except that it doesn't add any identifiers to the context. I use underscores to indicate that these identifiers are never in scope, but I do need to refer to them in the following. This is already what we do: we just build the enum as Ty.t in code, semantically. In fact, this is necessary so that Alt-Ergo reasons properly with this type at the moment.
• At the syntax level, in an AE file, we add the name bindings: NearestTiesToEven → _RNE, ToZero → _RTZ, Up → _RTP, Down → _RTN and NearestTiesToAway → _RTA. These names, when occuring in an AE file, will behave as the constructors for the _fpa_rounding_mode type. We also add the binding fpa_rounding_mode → _fpa_rounding_mode.
• At the syntax level again, in a SMT-LIB file, we add the name bindings: RNE → _RNE, RTZ → _RTZ, RTP → _RTP, RTN → _RTN and RTA → _RTA, as well as RoundingMode → _fpa_rounding_mode.

Note that we can do this at typechecking because we use different builtin environments depending on the file format. Order of matches does not matter, because user-defined names and builtins live in two separate environments (in fact this is a reason to do this at typing time rather than at parsing time, because at parsing time we cannot know if the constructor has been shadowed or not).

The actual names are not important, except that they will be used when printing values of type _fpa_rounding_mode, which is why we have to use the SMT-LIB names so that the appear correctly in models, so there should be almost no changes to the Fpa_rounding module except to change the name of the constructors.

This way, there is a single "semantic" ADT (so that the reasoners don't know about the input format and that is very good), but we give different names to the constructors in the different input format, making it by construction compatible with preludes written in a different language.

I'm sorry if I make you repeat, I have a hard time understanding your answers here.

Yes, sorry, the difference between "OCaml enum" vs "Alt-Ergo enum" plus the distinction between syntax and semantics make all this very confusing. Hopefully this is clearer now, otherwise we can discuss in person tomorrow as I will be in Paris, might be easier :)

[Stevendeo]

I think we forgot to talk about it when you were in Paris ! I chose it inject the fpa_rounding_mode of alt-ergo into the SMT Rounding Mode type instead of having a _fpa_rounding_mode in which the two types are injected.

[bclement-ocp]

Indeed we forgot — but we did have a lot of other things to cover. I think we are mostly on the same page tho; translating everything into RoundingMode is the right way forward I think.

There are still a few minor changes I'd like you to make (notably a couple unused stuff to remove) and we should be good to go :)

[bclement-ocp]

I think with mk_rounding now the following is shorter and clearer:

Suggested change

	| (B.RoundNearestTiesToEven
	| B.RoundNearestTiesToAway
	| B.RoundTowardPositive
	| B.RoundTowardNegative
	| B.RoundTowardZero as b), _ ->
	let fpa_rounding = match b with
	B.RoundNearestTiesToEven -> Fpa_rounding.NearestTiesToEven
	| B.RoundNearestTiesToAway -> NearestTiesToAway
	| B.RoundTowardPositive -> Up
	| B.RoundTowardNegative -> Down
	| B.RoundTowardZero -> ToZero
	| _ -> assert false
	in
	mk_rounding fpa_rounding
	| B.RoundNearestTiesToEven, _ -> mk_rounding NearestTiesToEven
	| B.RoundNearestTiesToAway, _ -> mk_rounding NearestTiesToAway
	| B.RoundTowardPositive, _ -> mk_rounding Up
	| B.RoundTowardNegative, _ -> mk_rounding Down
	| B.RoundTowardZero, _ -> mk_rounding ToZero

[bclement-ocp]

Nit: while this is correct, I feel like having the generic add_builtin_enum available is useful.

We could do add_builtin_enum ?(rename = Fun.id) map with an optional rename argument that is fun c -> Option.get (Fpa_rounding.translate_smt_rounding_mode c) for the rounding mode. On the other hand we can also do this when (if) we ever have more builtin enums to add before removing the legacy typechecker entirely, so eh.

[Stevendeo]

IIRC there was a more generic version of this function, which I specialized because it was used only once and I did not expect we would add new enums to the legacy syntax. I can revert it, but I already changed it to simplify the reading.

[bclement-ocp]

The generic version did not handle renaming so you were right to specialize it. This is a nit, feel free to ignore it :)

[bclement-ocp]

Remove this

[bclement-ocp]

Can you also add the smt2 version of this test to make sure the preludes work with smt2 input?

[Stevendeo]

Good point: I tested the 'simple' identifier parsing but not the 'indexed' one, which does not work.

EDIT: just an error in my test, ignore this comment

[bclement-ocp]

I believe this function is unused.

[bclement-ocp]

Since we use the SMT-LIB type as the "basis", this should be rounding_mode_of_hs (also for symmetry with string_of_rounding_mode).

[Stevendeo]

This name is to have symmetry and disambiguation with rounding_mode_of_ae_hs, which also is exported.

[bclement-ocp]

I that is the choice we make please update the documentation.

[bclement-ocp]

Nothing wrong with using 'a option in general, but if we are going to raise an exception anyways, it would be better to call Hashtbl.find and catch Not_found to avoid the extra allocation.

[bclement-ocp]

The documentation comment is useful but calling this something explicit like inject_ae_to_smt2 would be clearer than inject_identifier which sounds generic.

[bclement-ocp]

Sorry, I somehow missed that this one was ready — let's merge.