Ty.RoundFpToDynBv Bug

[jkwoods]

Code that casts from a double/float, like this:

int main(void) {
   int r = (int) 4.2;
   return(r);
}

is "checked" correctly, and will pass tests, but will not compile to constraints.

Error here: "Cannot translate RoundFpToDynBv <expression...>'

[jkwoods]

I fixed this by implementing RoundFpToDynBv in ToPf.hs. I don't know if you guys want my fix or have a plan in mind for that stuff in the future?

[alex-ozdemir]

Interesting. Certainly the code would go in ToPf.hs.

However, I have to ask first: it seems that before one embeds RoundFpToDynBv in R1CS, one must be able to embed floating point terms in R1CS. Have you already done that? If so, that's really cool and I'd love to hear more about it.

[jkwoods]

I don't have floating points in the general case. Basically just Fp64Lits, Fp32Lits, RoundFpToDynBv - just what you would need for casting doubles/floats to the fixed point implementation. (So the user can write fixed point terms as decimals/"floating points".) I used the asBits method from TySMT.

I was under the impression we wanted to make fixed point work first/instead. This just allows the user to write fixed point stuff in a natural way. I'd be willing to do the rest of floating point at some point.

[alex-ozdemir]

I was under the impression we wanted to make fixed point work first/instead. This just allows the user to write fixed point stuff in a natural way. I'd be willing to do the rest of floating point at some point.

This is certainly the right approach!

Basically just Fp64Lits, Fp32Lits, RoundFpToDynBv - just what you would need for casting doubles/floats to the fixed point implementation.

I see. Okay, now I think I understand better.

I fixed this by implementing RoundFpToDynBv in ToPf.hs. I don't know if you guys want my fix or have a plan in mind for that stuff in the future?

I think the right strategy here would be to merge the entire fix-point implementation (when it's ready), rather than merging the changes one at a time. I'm happy to talk about doing that whenever you feel the implementation is ready.

[jkwoods]

Ok, cool. Ready very soon. I think it will need some revamping in line with your most recent pull request.