Поддерживает ли Z3 преобразование Real-to-Int?

В Z3 вы должны to_real получить реальный эквивалент Int. Есть ли какая-то поддержка обратных преобразований, то есть усечения, округления и т.п.? В отрицательном случае, каким может быть наиболее удобный для Z3 способ их определения, если таковой имеется? Всем большое спасибо ответите.


z3
person Pietro Braione    schedule 15.10.2012    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Да, в Z3 есть функция to_int, которая преобразует вещественное число в целое число. Семантика to_int определена в стандарте SMT 2.0. Вот пример: http://rise4fun.com/Z3/uJ3J

(declare-fun x () Real)

(assert (= (to_int x) 2))
(assert (not (= x 2.0)))

(check-sat)
(get-model)
person Leonardo de Moura    schedule 15.10.2012
comment
Спасибо большое; поскольку мне нужно округление до нуля, я буду использовать (define-fun round_to_zero ((x Real)) Int (if (›= x 0.0) (to_int x) (- (to_int (- x))))). Еще раз спасибо и продолжайте в том же духе с Z3. - person Pietro Braione; 16.10.2012