대수적 인 실수 : 꽤 인쇄 할 때 z3은 반올림합니까?

Question

내가 발행하는 경우 :

(set-option :pp-decimal true) 
(set-option :pp-decimal-precision 10) 

합니까 Z3는 실수의 10 자리 이후 반올림을합니까? 또는 반올림하지 않고 나머지 자릿수를 자르지 않습니까? Z3 4.0

Answer 1

는 대수적 번호 alpha은 변량 다항식 p 두 이진 유리수를 이용하여 표현된다 lower 및 upper. 이진 합리성은 a/2^k 형태의 유리한 수이고, a은 정수이며 k은 자연수입니다. 우리는 alpha이 (lower, upper) 간격의 p의 유일한 근원임을 알았습니다. 때 옵션

(설정 옵션을 : 사실 PP-진수)

(설정 옵션 : PP-소수점 정밀도를 N)

가 제공됩니다. 먼저, 간격을 좁히거나 좁히십시오 (lower, upper)upper - lower < 1/10^N까지. 그런 다음 상위 경계 (이진 합리성)를 엿보고 N 번째 자릿수를 잘라서 10 진수로 표시합니다. 더 정확하게 말하면, 정제는 실제로 upper - lower < 1/16^N까지 수행됩니다.

나는 이것이 이상적인 해결책이 아니라는 것을 알고 있지만, 대부분의 경우에 충분하다.