Support for Casting

[Greg4cr]

Yices does not support typecasting. However, other solvers - such as Z3 - do support casting from integer -> real and real -> integer.

If possible, could JKind be upgraded to support the Lustre cast(var, type) operation when using an appropriate solver?

As usual, thanks for your hard work.

[agacek]

I would hate to support a feature like this for just one solver. That said, it appears SMT-LIB2, the standard language we use to communicate with z3 and cvc4, supports casting:

From: http://smtlib.cs.uiowa.edu/theories/Reals_Ints.smt2

• to_real as the standard injection of the integers into the reals,
• to_int as the function that maps each real number r to its integer part, that is, to the largest integer n that satisfies (<= (to_real n) r)

In addition we can create those same functions in Yices:

From: http://mls.csl.sri.com/pipermail/yices-help/2009-February/000154.html

(define to_int::(-> x::real (subtype (y::int) (and (<= y x) (< x (+ y 1)))))) (define to_real::(-> x::int (subtype (y::real) (= y x))))

This seems to work and the semantics agree between the solvers.

Really the only controversial part of the semantics is what to do when converting a negative real to a integer. For example:

to_int -1.5

Our solvers say the answer is -2. Most programming languages (e.g. Java) would give back -1. I believe solvers have the identity:

to_int x <= x < 1 + to_int x

Whereas most programming languages have the identity:

to_int -x = - to_int x

Both are reasonable, so this just becomes another sharp edge where people need to be aware the our semantics for Lustre might not accurately model the semantics of the language they are encoding. This is essentially the same issue as in integer division with negative numerators (see issue #16).

Any way, the next step is to figure out syntax. I'm research Lustre syntax for this now.

On Thu, Mar 27, 2014 at 4:32 PM, Gregory Gay notifications@github.com wrote:

Yices does not support typecasting. However, other solvers - such as Z3 - do support casting from integer -> real and real -> integer.

If possible, could JKind be upgraded to support the Lustre cast(var, type) operation when using an appropriate solver?

As usual, thanks for your hard work.

Reply to this email directly or view it on GitHub.

[agacek]

Gryphon uses the syntax

cast(x, int) cast(x, real)

According to http://www.di.ens.fr/~pouzet/cours/mpri/manual_lustre.ps it seems Lustre might use the syntax

int(x) real(x)

Both of these options are nicer than Java/C style syntax since they avoid any issues with figuring out precedence. Personally, I prefer the latter style since it is less verbose while still being quite clear.

On Fri, Mar 28, 2014 at 10:51 AM, Andrew Gacek andrew.gacek@gmail.com wrote:

I would hate to support a feature like this for just one solver. That said, it appears SMT-LIB2, the standard language we use to communicate with z3 and cvc4, supports casting:

From: http://smtlib.cs.uiowa.edu/theories/Reals_Ints.smt2

• to_real as the standard injection of the integers into the reals,
• to_int as the function that maps each real number r to its integer part, that is, to the largest integer n that satisfies (<= (to_real n) r)

In addition we can create those same functions in Yices:

From: http://mls.csl.sri.com/pipermail/yices-help/2009-February/000154.html

(define to_int::(-> x::real (subtype (y::int) (and (<= y x) (< x (+ y 1)))))) (define to_real::(-> x::int (subtype (y::real) (= y x))))

This seems to work and the semantics agree between the solvers.

Really the only controversial part of the semantics is what to do when converting a negative real to a integer. For example:

to_int -1.5

Our solvers say the answer is -2. Most programming languages (e.g. Java) would give back -1. I believe solvers have the identity:

to_int x <= x < 1 + to_int x

Whereas most programming languages have the identity:

to_int -x = - to_int x

Both are reasonable, so this just becomes another sharp edge where people need to be aware the our semantics for Lustre might not accurately model the semantics of the language they are encoding. This is essentially the same issue as in integer division with negative numerators (see issue #16).

Any way, the next step is to figure out syntax. I'm research Lustre syntax for this now.

On Thu, Mar 27, 2014 at 4:32 PM, Gregory Gay notifications@github.com wrote:

Yices does not support typecasting. However, other solvers - such as Z3 - do support casting from integer -> real and real -> integer.

If possible, could JKind be upgraded to support the Lustre cast(var, type) operation when using an appropriate solver?

As usual, thanks for your hard work.

Reply to this email directly or view it on GitHub.

[Greg4cr]

I also prefer the latter syntax. I'm working with Gryphon's Simulink -> Lustre translation, but I can filter the Gryphon format to the preferred Lustre format.

Thanks for looking at this!

(and the other requests I've made - if I ask for anything unreasonable, go ahead and say no - Mike just suggested I make requests on here as others might want to do these things too)

[agacek]

Casting came up once before in my own project. Actually it was checking if a real was an integer which wasn't possible before, but with casting one could check real(int(x)) = x.

On Fri, Mar 28, 2014 at 11:06 AM, Gregory Gay notifications@github.comwrote:

I also prefer the latter syntax. I'm working with Gryphon's Simulink -> Lustre translation, but I can filter the Gryphon format to the preferred Lustre format.

Thanks for looking at this!

(and the other requests I've made - if I ask for anything unreasonable, go ahead and say no - Mike just suggested I make requests on here as others might want to do these things too)

Reply to this email directly or view it on GitHubhttps://github.com/agacek/jkind/issues/17#issuecomment-38936354 .

[agacek]

After discussing this with Mike, I now like the syntax real(x) and floor(x). This makes is clear what the behavior of the real to int conversion is. Then people can defined their own towardsZero(x) or ceil(x) or whatever else they want using the clearly named floor primitive.

On Fri, Mar 28, 2014 at 11:14 AM, Andrew Gacek andrew.gacek@gmail.comwrote:

Casting came up once before in my own project. Actually it was checking if a real was an integer which wasn't possible before, but with casting one could check real(int(x)) = x.

On Fri, Mar 28, 2014 at 11:06 AM, Gregory Gay notifications@github.comwrote:

I also prefer the latter syntax. I'm working with Gryphon's Simulink -> Lustre translation, but I can filter the Gryphon format to the preferred Lustre format.

Thanks for looking at this!

(and the other requests I've made - if I ask for anything unreasonable, go ahead and say no - Mike just suggested I make requests on here as others might want to do these things too)

Reply to this email directly or view it on GitHubhttps://github.com/agacek/jkind/issues/17#issuecomment-38936354 .

[Greg4cr]

I like it.

[agacek]

I've added support for this. It works with Yices and Z3. CVC4 still has some strange behavior, but I've contacted the developers about it.