cvc4中实数的对数/指数

Question

我正在寻找一个求解者，它可以提供涉及对数或指数的实数公式的模型。

cvc4能处理包含实数对数或指数的函数吗？类似地，cvc4能表示常量e吗？

根据this question的说法，z3只能处理常量指数，这对我没有帮助。

This question只询问整数的对数。

Answer 1

我不熟悉cvc4，但我可能有一些关于对数的有用属性，您可以根据自己的限制利用这些属性。

从技术上讲，没有一台计算机(无论多么强大)知道e是什么，因为它是超越性的(不能用有理系数多项式方程的解来表示)。

如果你是有限的，你只能取整数的对数，你可以用一个派系近似来表示e并用这个方法来解决它。这个公式最终比直接取对数要长一点，但优点是你可以有效地计算出基数是任何有理数的对数，而只能单独地求出整数的对数。

设e被分数a/b近似，其中a和b都是整数。

(a/b)^n = x

log(base a/b)(x) = n

这并没有给你带来任何东西，所以我们必须走另一条路线，这需要更多的代数。

(a/b)^n = x

(a^n)/(b^n) = x

a^n = x * b^n

log(base a)(x * b^n) = n

log(base a)(x) + log(base a)(b^n) = n

log(base a)(x) + n*log(base a)(b) = n

log(base a)(x) = n - n*log(base a)(b)

log(base a)(x) = n * (1 - log(base a)(b))

n = log(base a)(x) / (1 - log(base a)(b))

换句话说，log(base a)(x) / (1 - log(base a)(b))是ln(x)的近似，其中a/b是e的近似。显然，随着ln(x)更接近于ln(x)的实际值，a/b更接近e。注意，我在这里保持了一个通用的形式，即a/b可以表示任何有理数，而不仅仅是e。

如果这不能完全回答你的问题，我希望它至少有帮助。

只是尝试了一个武断的例子。

如果您认为a和b分别为27183和10000，那么我尝试了以下快速计算：

log(base 27183)(82834) / (1 - log(base 27138)(10000)) = 11.32452...

                                            ln(82834) = 11.32459...