如何在z3py中表示对数公式

Question

我对z3py非常陌生。我正在尝试用z3py编写以下对数表达式。

log(x,y)

我确实搜索了很多堆栈溢出，遇到了类似的问题，但不幸的是，我无法得到一个足够满意的答案。请帮帮我!

Answer 1

更广泛地说，我们如何用Z3定义日志？

唯一能让我有所了解的方法是使用e的近似值，将exp(x)定义为(^ e x)，然后将log定义为exp的逆函数。在SMT-LIB 2中：

(define-fun exp ((x Real)) Real (^ 2.718281828459045 x))
(declare-fun log (Real) Real)
(assert (forall ((x Real)) (= (log (exp x)) x)))
(assert (forall ((x Real)) (= (exp (log x)) x)))

在Z3Py中：

from z3 import *
from math import e

# This is an approximation
def Z3_exp(x):
    return e ** x

s = Solver()

# We define Z3_log as a total function that is the inverse of Z3_exp
Z3_log = Function('log', RealSort(), RealSort())
x = Real('x')
s.add(ForAll([x], Z3_log(Z3_exp(x)) == x))
s.add(ForAll([x], Z3_exp(Z3_log(x)) == x))

这样做的明显问题是，它引入了e的近似值，这将导致一些不正确的结果，具体取决于您试图证明的内容。此外，因为它使用未解释的函数来定义log，所以将不会使用最强大的非线性求解器(nlsat)，而且由于functions are total in SMT-LIB，将会出现典型的奇怪的负参数领域问题。

另一种选择是简单地绑定e，但这仍然不准确，而且可能会有更糟糕的行为。在Z3中还有一个没有文档记录的内置符号euler，但目前它基本上是不起作用的。