search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
429 stars 40 forks source link

[BUG] Fix integer division in the model checker #331

Open konnov opened 3 years ago

konnov commented 3 years ago

According to the definition in Specifying Systems:

Integer division \div and modulus (%) are defined so that the following two conditions hold, for any integer a and positive integer b:

a % b \in 0..(b-1) a = b * (a \div b) + (a % b)

This definition is incompatible with the definition of div in SMTLIB and integer division in programming languages. However, we have to be compatible with the book and TLC.

konnov commented 3 years ago

This is a summary of tests that show how integer division is implemented in different languages. The current version of TLC seems to be compatible with // in python and incompatible with div in SMTLIB. I am not even sure about possible fixes, as the book is only giving us the definition for the positive dividers.

  C (clang 12) Scala 2.13 Rust Python 3.8.6 TLA+ (TLC) SMT (z3 4.8.8)
100 div 3 100 / 3 == 33 100 / 3 == 33 100 / 3 == 33 100 // 3 == 33 (100 \div 3) = 33 (assert (= 33 (div 100 3)))
(-100) div 3 -100 / 3 == -33 -100 / 3 == -33 -100 / 3 == -33 -100 // 3 == -34 ((-100) \div 3) = -34 (assert (= (- 0 34) (div (- 0 100) 3)))
100 div (-3) 100 / (-3) == -33 100 / (-3) == -33 100 / (-3) == -33 100 // (-3) == -34 (100 \div (-3)) = -34 (assert (= (- 0 33) (div 100 (- 0 3))))
(-100) div (-3) -100 / (-3) == 33 -100 / (-3) == 33 -100 / (-3) == 33 -100 // (-3) == 33 ((-100) \div (-3)) = 33 (assert (= 34 (div (- 0 100) (- 0 3))))
konnov commented 3 years ago

Although it is a bug, it seems to be of low priority

konnov commented 2 years ago

It's even worse, our preprocessing uses Scala division, which makes it inconsistent

thpani commented 2 years ago

The problem is that Python and TLC allow a negative remainder, whereas SMT-LIB does not. In contrast, the PLs+TLC leave the remainder unconstrained and just favor a rounding direction for /, either towards -\infty or towards 0.

konnov commented 2 years ago

It looks like we have to express integer division via (if ...) in SMT, if we want to support the TLC definition.

thpani commented 2 years ago

The SMT-LIB definition actually nicely lines up with the one from Specifying Systems (modulo accounting for a negative divisor in the definition of mod)