Z3 support for exponentials

Question

I'm new to Z3 and I'm trying to understand how it works, and what it can and cannot do. I know that Z3 has at least some support for exponentials through the power (^) operator (see Z3py returns unknown for equation using pow() function, How to represent logarithmic formula in z3py, and Use Z3 and SMT-LIB to define sqrt function with a real number). What I'm unclear on is how extensive this support is, and what kind of inferences z3 can make about exponentials.

Here's a simple example involving exponentials which z3 can analyze. We define an exponential function, and then ask it to verify that exp(0) == 1:

(define-fun exp ((x Real)) Real
  (^ 2.718281828459045 x))
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(assert (= y1 (exp x1)))
(assert (not (=> (= x1 0.0) (= y1 1.0))))
(check-sat)
(exit)

Z3 returns unsat, as expected. On the other hand, here's a simple example which Z3 can't analyze:

(define-fun exp ((x Real)) Real
  (^ 2.718281828459045 x))
(declare-fun x1 () Real)
(declare-fun y1 () Real)
(assert (= y1 (exp x1)))
(assert (not (< y1 0.0)))
(check-sat)
(exit)

This should be satisfiable, since literally any value for x1 would give y1 > 0. However, Z3 returns unknown. Naively I might have expected that Z3 would be able to analyze this, given that it could analyze the first example.

I realize this question is a bit broad, but: can anyone give me any insight into how Z3 handles exponentials, and (more specifically) why it can solve the first example I gave but not the second?

Sometimes (check-sat-using (or-else default qfnra-nlsat)) gives better results, using the non-linear sat engine. (Though it doesn't work for your second example.) In my experience, it's really hard to say when something works and when it doesn't once you have non-linear terms. — alias

pavpanchekha pavpanchekha · Accepted Answer · 2018-05-17T22:46:45

It is hard to say in general, since non-linear solving is challenging, but the case you presented is actually not so mysterious. You wrote:

(assert (= y (exp x)))
(assert (not (=> (= x 0) (= y 1))))

Z3 is going to simplify the second assertion, yielding:

(assert (= y (exp x)))
(assert (= x 0))
(assert (not (= y 1)))

Then it will propagate the first equality, yielding:

(assert (= y (exp 0)))
(assert (not (= y 1)))

Now when exp is expanded, you have a case of constant^constant, which Z3 can handle (for integer exponents, etc).

For the second case, you are asking it a very very basic question about variable exponents, and Z3 immediately barfs. That's not too odd, since so many questions about variable exponents are either known uncomputable or unknown but hard.

Z3 support for exponentials

1 Answers