Search code examples
z3smt

Z3 support for exponentials

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?

Solution

  • 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.