a potential new normalization

[redianthus]

Hi @filipeom!

While working with Codex, I noticed they are only exposing one of {lt,le,gt,ge}.

Currently we are exposing two of them :

smtml/src/smtml/ty.mli

Lines 184 to 187 in 03d8b4c

	| Lt (** Less than. *)
	| LtU (** Unsigned less than. *)
	| Le (** Less than or equal. *)
	| LeU (** Unsigned less than or equal. *)

Maybe we could remove lt and encode lt x1 x2 as not (ge x1 x2) which is not (le x2 x1).
It might help with cache-hit and normalization-related stuff, but on the other hand, it might not be that good for the SMT, I'm not really sure.

WDYT?

[filipeom]

I think it does indeed simplify the AST and it might improve caching. However, I not sure if that normalization is sound for floating point arithmetic. We have to be careful because both lt and le evaluate to false if the relop has a NaN in either argument. For that reason if you do not (le x2 x1) and either x2 or x1 is a NaN this operation would return true when the result is false.

[redianthus]

Ah yes sure, I was thinking about bitvectors and such !