search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
449 stars 149 forks source link

`/Int` is not equivalent to `div` of SMT-LIB #238

Closed daejunpark closed 3 years ago

daejunpark commented 5 years ago

Currently, /Int and %Int have the attribute smtlib(div) and smtlib(mod), respectively: https://github.com/kframework/k/blob/6bc147f6097afd3aa3c6a6c6d472201614ff7ef5/k-distribution/include/builtin/domains.k#L359-L360

According to the SMT-LIB integer theory, however, they do not agree on negative numbers. For example, -4 /Int 3 is -1, while (div -4 3) is -2.

dwightguth commented 5 years ago

This is quite unfortunate. If (div -4 3) is -2, that means that Z3 division is rounding to negative infinity, whereas /Int and %Int round to zero, and divInt and modInt are euclidean division (ie the remainder is always positive). it should be possible to change the smtlib attribute to an if-then-else expression that computes the correct value for negative numbers, but this does mean that divInt and modInt also have incorrect smtlib expressions and also need to be corrected. Take a look at powmod for the syntax of using an expression in the smtlib attribute.

dwightguth commented 5 years ago

Since this is a problem in the K prelude, I can take care of it at some point if you don't want to work on it, but it will have to wait until I get the llvm backend delivered to IOHK, so since it's a simple change, you might want to do it yourself.

daejunpark commented 5 years ago

Just for a reference: https://github.com/kframework/k/pull/240#issuecomment-453702596

ehildenb commented 3 years ago

@daejunpark is this still a problem?

daejunpark commented 3 years ago

Close this for now: https://github.com/kframework/k/pull/240#issuecomment-469931127