Project

General

Profile

Bug #4992

[calculator] В StandardOperationsInt операции MOD и REM реализованы одинаково

Added by Alexander Kamkin over 6 years ago. Updated about 6 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Andrei Tatarnikov
Category:
-
Target version:
Start date:
06/16/2014
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
140915

Description

Следует уточнить в SMT-LIB.

History

#1

Updated by Sergey Smolov over 6 years ago

  • Target version changed from 0.1 to 0.3
#2

Updated by Andrei Tatarnikov about 6 years ago

Про это подробно не пишут (во всяком случае я пока не нашёл). Но разница есть (возникает при работе с отрицательными числами) и следующий пример её демонстрирует:

(declare-const a Int)
(declare-const b Int)
(declare-const r1 Int)
(declare-const r2 Int)
(declare-const r3 Int)
(declare-const r4 Int)
(assert (= a 10))
(assert (= b 4))

(assert (= r1 (mod a b))) ; mod
(assert (= r2 (rem a b))) ; remainder
(assert (= r3 (mod a (- b)))) ; mod
(assert (= r4 (rem a (- b)))) ; remainder

(check-sat)
(get-value (a b r1 r2 r3 r4))

sat
((a 10)
 (b 4)
 (r1 2)
 (r2 2)
 (r3 2)
 (r4 (- 2)))

#3

Updated by Andrei Tatarnikov about 6 years ago

Z3 реализует следующее поведение (выяснено методом тыка):

  1. MOD всегда дает положительный результат независимо от знака операндов;
  2. REM даёт отрицательный результат только если второй операнд отрицателен, знак первого не влияет на результат.

В Java сделано следующим образом (выяснено методом тыка):

  1. MOD знак результата зависит от знака второго операнда, знак первого игнорируется
  2. REM такого оператора нет
#4

Updated by Andrei Tatarnikov about 6 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

Изменил реализацию так, чтобы поведение было как в Z3 (см. мою заметку выше). r527.

Есть возражения?

#5

Updated by Andrei Tatarnikov about 6 years ago

  • Status changed from Resolved to Closed
  • Published in build set to 140915

Also available in: Atom PDF