Z3 对指数的支持

Question

我是 Z3 的新手，我正在尝试了解它的工作原理，以及它能做什么和不能做什么。我知道 Z3 至少 一些 通过幂 (^) 运算符支持指数（请参阅 Z3py returns unknown for equation using pow() function、How to represent logarithmic formula in z3py 和 Use Z3 and SMT-LIB to define sqrt function with a real number）。我不清楚的是这种支持有多广泛，以及 z3 可以对指数做出什么样的推论。

这是一个涉及指数的简单示例，z3 可以分析。我们定义一个指数函数，然后要求它验证 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 无法分析的简单示例：

(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 如何处理指数的见解，以及（更具体地说）为什么它可以解决我给出的第一个示例但不能解决第二个示例？

Answer 1

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

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

Z3 将简化第二个断言，产生：

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

然后它将传播第一个相等，产生：

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

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

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