如何在z3py中表示对数公式 [英] How to represent logarithmic formula in z3py

问题描述

我对 z3py 很陌生.我正在尝试在 z3py 中编写以下对数表达式.

I am very new to z3py. I am trying to code the following logarithmic expressions in z3py .

log(x,y)

我确实经常搜索堆栈溢出并遇到类似的问题，但不幸的是我无法得到足够令人满意的答案.请帮帮我！

I did search stack overflow a lot and came across a similar question, but unfortunately I could not get a satisfactory enough answer. Please help me!

推荐答案

更一般地说，我们如何用 Z3 定义日志?

More generally, how can we define logs with Z3?

我获得任何吸引力的唯一方法是使用 e 的近似值，将 exp(x) 定义为 (^ ex)，然后将 log 定义为 exp 的逆函数.在 SMT-LIB 2 中:

The only way I have gotten any traction at all is to use an approximate value for e, define exp(x) as (^ e x), and then define log as a total function that is the inverse of exp. In 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)，而且，因为 SMT-LIB 中的函数是全部，对于否定参数会有典型的奇怪域问题.

The obvious problem with this is that it introduces an approximation for e, which will cause some incorrect results depending on what you are trying to prove. Also, because it uses uninterpreted functions to define log, the most powerful nonlinear solver (nlsat) will not be used, and also, because functions are total in SMT-LIB, there will be the typical weird domain issues for negative arguments.

另一种方法是简单地绑定 e，但这仍然不准确，并且可能有更糟糕的行为.Z3 中还有一个未公开的内置符号 euler，但目前它基本上没有功能.

An alternative would be to simply bound e, but this is still not exact, and is likely to have worse behavior. There is also an undocumented built-in symbol euler in Z3, but at the moment it is essentially non-functional.

这篇关于如何在z3py中表示对数公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！