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!
More generally, how can we define logs with Z3?
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)))
In 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))
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.
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.
