Z3 supports nonlinear polynomial Real arithmetic. So, there is no support for transcendental functions (e.g., sine and cosine), and exponential (e.g., 2^x
). Actually, for the exponential, Z3 can handle exponents that can be simplified to numerals. Here is an example,
x = Real('x')
y = Real('y')
solve(y == 3, x**y == 2)
In this example, the y
in x**y
is rewritten to 3
during a preprocessing step. After preprocessing, the nlsat solver for nonlinear polynomial real arithmetic is invoked.
Regarding nonlinear integer arithmetic, see this related post.
与恶龙缠斗过久,自身亦成为恶龙;凝视深渊过久,深渊将回以凝视…