Support a dynamic approach to FP bitvector rounding modes

[Tony Sloane]

Currently rounding modes are provided to operations via implicit arguments of type Sort. E.g., we can have an implicit in scope that is set to RNE() and that will be used for operation terms we create in that scope. Unfortunately, this means we need to know the rounding mode we want to use at the time we create the terms.

To support the C library functions fegetround and fesetround I think a more dynamic approach is needed. fegetround is used to store the rounding mode in an integer variable via its return value. fesetround is used to set the rounding mode from an integer argument. In neither case can we guarantee to know statically what the rounding modes will be.

As a related issue, it seems strange that RNE etc are Sorts. smtlib has a RoundingMode sort which has values RNE, etc. This would seem to suggest that Scala SMT should support the RoundingMode sort and that RNE etc should be terms not sorts.

It seems that a viable approach to encoding dynamic rounding modes is to have an smtlib variable _fprmode of sort RoundingMode and use it to keep track of the (dynamic) rounding mode (using indexes to distinguish between the different values of _fprmode). We would then just need to encode the conversion from RNE etc to C library function rounding modes, and vice versa.

So then we would need to be able to somehow specify the rounding mode when we create fp operation terms to be something like _fprmode@3 rather than one of RNE, etc. At the moment I am hacking this in by encoding the RoundingMode sort directly by name and pretending that _fprmode is a Sort (since the implicit is a sort).

[Franck Cassez]

@inkytonik The new 2.1.1-SNAPSHOT has RoundingMode variables. They can be created as follows:

    val rm = RMs( "rm" )

and then used in FPBV operators e.g.

(x.+(y)(rm)) fpeq Reals(2.219).toFPBV(5,11)

Get-value also works for RoundingModeSort variables.

[Tony Sloane]

Looks good, thanks! I've just pushed a Skink fpbv branch commit that replaces my hacks with the new RM support.

One possible addition: Skink currently has this method:

def fpToSignedInt(op1 : TypedTerm[FPBVTerm, Term], bits : Int)(implicit rm : TypedTerm[RMFPBVTerm, Term]) : TypedTerm[BVTerm, FPBVToSBV] =
    TypedTerm[BVTerm, FPBVToSBV](
        op1.typeDefs,
        FPBVToSBV(bits.toString, rm.termDef, op1.termDef)
    )

since I couldn't see a builder for this kind of term in Scala SMT. Did I miss it? Or should we add something like this?

[Franck Cassez]

@inkytonik Yes I'll add it later (this is issue #10: conversion to other sorts).

[Tony Sloane]

Ah yes, of course. It seems like this issue can be closed then.

[Franck Cassez]

RoundingModes fixed, closing this issue.