Если я выдаю:алгебраические значения: делает z3 делать округление, когда довольно печатает?
(set-option :pp-decimal true)
(set-option :pp-decimal-precision 10)
ли Z3 сделать любое закругление после 10 разряда действительного числа? Или он просто рубит оставшиеся цифры без округления?
В Z3 4.0, алгебраическое число alpha представляется с использованием одномерного полиномом p и два бинарных рациональными: lower и upper. Бинарным рациональным является рациональное число вида a/2^k, где a - целое число и k - натуральное число. У нас есть то, что alpha является единственным корнем p в интервале (lower, upper). Когда опции
(вариант установленная: PP-десятичный истинный)
(вариант установленные: PP-десятичные точности N)
предусмотрены. Во-первых, я сжимаю/уточняю интервал (lower, upper) до upper - lower < 1/10^N. Затем я просматриваю верхнюю границу (которая является двоичной рациональной) и отображает ее в десятичной форме путем измельчения после N-й цифры. Точнее, уточнение фактически выполняется до upper - lower < 1/16^N.
Я понимаю, что это не идеальное решение, но оно достаточно для большинства целей.