Z3 支持指数 [英] Z3 support for exponentials

问题描述

我是 Z3 的新手，我正在尝试了解它是如何工作的，以及它可以做什么和不能做什么.我知道 Z3 通过幂 (^) 运算符至少一些支持指数(参见 Z3py 使用 pow() 函数返回未知的方程，如何在 z3py 中表示对数公式 和 使用 Z3 和 SMT-LIB 定义带有实数的 sqrt 函数).我不清楚这种支持有多广泛，以及 z3 可以对指数做出什么样的推断.

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.

这是一个简单的例子，涉及 z3 可以分析的指数.我们定义一个指数函数，然后让它验证exp(0) == 1:

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 返回 unsat，正如预期的那样.另一方面，这是一个 Z3 无法分析的简单示例:

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)

这应该是可满足的，因为实际上 x1 的任何值都会使 y1 > 0.然而，Z3 返回未知.考虑到 Z3 可以分析第一个示例，我可能天真地以为 Z3 能够对此进行分析.

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.

我意识到这个问题有点宽泛，但是:谁能让我深入了解 Z3 如何处理指数，以及(更具体地说)为什么它可以解决我给出的第一个例子，但不能解决第二个例子?

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?

推荐答案

一般来说很难说，因为非线性求解具有挑战性，但是您提出的案例实际上并不那么神秘.你写道:

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 将简化第二个断言，产生:

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)))

现在当 exp 展开时，你有一个常量^constant 的情况，Z3 可以处理(对于整数指数等).

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

对于第二种情况，你问的是一个关于变量指数的非常非常基本的问题，Z3 立即倒闭.这并不太奇怪，因为很多关于变量指数的问题要么是已知不可计算的，要么是未知但很难.

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 支持指数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！