I understand that Z3 has some supports for nonlinear arith but wondering to what extends ? Is it possible to specify what classes of nonlinear arithmetics are supported and are not (or likely to give time out) ? Know these in advances will help me abort my task early.
Seems like power related stuff is not supported as shown below
def pow2(x):
k=Int('k')
return Exists(k, And(k>=0,2**k==x))
prove(pow2(7))
failed to prove
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.
