z3pyでの対数式の表現方法

Question

私はz3pyの新機能です。私はz3pyで以下の対数表現をコード化しようとしています。

log(x,y) 

スタックオーバーフローを多数検索して同様の質問がありましたが、残念ながら十分な回答が得られませんでした。私を助けてください！

Answer 1

さらに一般的に、Z3でログを定義するにはどうすればよいですか？

私はまったく牽引力を得ている唯一の方法は、eの近似値を使用(^ e x)としてexp(x)を定義し、expの逆数である合計関数としてlogを定義することです。 SMT-LIB 2では：

Z3Pyで

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

：

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もありますが、現時点では本質的に機能していません。