Поддержка Z3 для нелинейной арифметики

Question

Я понимаю, что Z3 имеет некоторую поддержку нелинейного арифметического, но интересно, что распространяется? Можно ли указать, какие классы нелинейной арифметики поддерживаются и не поддерживаются (или могут дать время ожидания)? Знать это заранее поможет мне прервать мою задачу рано.

Похоже, что питание не поддерживается, как показано ниже

def pow2(x): 
    k=Int('k')
    return Exists(k, And(k>=0,2**k==x))


prove(pow2(7))
failed to prove

Answer 1

Z3 поддерживает нелинейную полиномиальную вещественную арифметику. Таким образом, нет поддержки трансцендентных функций (например, синуса и косинуса) и экспоненциальных (например, 2^x). На самом деле, для экспоненты, Z3 может обрабатывать показатели, которые можно упростить до цифр. Вот пример,

x = Real('x')
y = Real('y')
solve(y == 3, x**y == 2)

В этом примере y в x**y переписан 3 на этапе предварительной обработки. После предварительной обработки запускается решатель nlsat для нелинейной полиномиальной вещественной арифметики. Что касается нелинейной целочисленной арифметики, см. Этот пост.