При расчете появляется ошибка, как ее исправить?

Question

[artshelom]

Использую библиотеку для расчета z3.
Вот код:

constants =[
        ((y - y2) / (x - x2)) ==(
            ((f - 2 * p) * math.sqrt(1 - q * q) +
             2 * math.sqrt(f * f * q * q * (1 - q * q) + p * (p - f))) /
            (2 * f * q * q + (2 * p - f) * q - f)
        ),
        ((y - y1) / (x - x1)) == (
                ((f - 2 * p) * math.sqrt(1 - q * q) -
                 2 * math.sqrt(f * f * q * q * (1 - q * q) + p * (p - f))) /
                (2 * f * q * q + (2 * p - f) * q - f)
        ),
        4 * 1 / f * (p - p1) == **
        #
        4 * 1 / f * (p - p1) == **
    ]
    for i in constants:
        solver.add(i)
    while solver.check() == z3.sat:
        print(solver.model()[x], solver.model()[y])
        solver.add(x != solver.model()[x],
                   y != solver.model()[y])

А вот ошибка:

2 * math.sqrt(f * f * q * q * (1 - q * q) + p * (p - f))) /
TypeError: must be real number, not BitVecRef

Answer 1

[dmshar]

Функция sqrt из пакета math требует, что-бы на ее вход подавались действительные числа. А что вы ей на ход пытаетесь подать - всякие f,q,p. - так нам сие не ведомо.
Проверяйте.

Comments

[artshelom]

А какую тогда функцию использовать для вычисления корня? то z3 не видел sqrt

[artshelom]

Нашел спасибо