Проблемы с Z3 (версия 4.3): Результат реального значения не округляется автоматически

Question

Пожалуйста, помогите мне решить эту проблему, я пробовал различные способы, но не удалось.

На сайте: http://rise4fun.com/Z3

при решении этой формулы:

 
(declare-const a Real) 
(assert (= a (/ 5 2))) 
(check-sat) 
(get-model) 

результатом является

 
sat 
(model 
    (define-fun a() Real 
    (/ 5.0 2.0)) 
) 

Ответ (/ 5,0 2,0), которое не является круглым стоимость. (Нужно 2.5)

В старой версии Z3 (версия 3.2), с той же вышеприведенной формуле: ответ 2,5 (то есть то, что мне нужно)

Есть ли кто-нибудь знает, как config Z3 (версия 4.3), чтобы получить тот же ответ, что и его старая версия?

Спасибо.

Answer 1

Пожалуйста, используйте следующий код

(declare-const a Real) 
(assert (= a (/ 5 2))) 
(check-sat) 
(set-option :pp-decimal true) 
(get-model) 

и выход

sat 
(model 
    (define-fun a() Real 
    2.5) 
)