Add conversions between Int and Real

Issue #29 new
Tony Sloane created an issue

I was looking to support conversion operations such as fptosi and sitofp (plus their unsigned versions) in math mode. (They are fine in bit mode.)

However, it seems that the Ints and Reals theories don't support these conversions. According to the smtlib site, we needs the Ints_Reals theory which provides to_real and to_int, etc.

Is there another way to encode this kind of conversion with what ScalaSMT already has, or do we need to add support for Ints_Reals to ScalaSMT?

Comments (0)

  1. Log in to comment