I am looking for a solver that can provide models of formulas on real numbers involving logarithms or exponentials.
Can cvc4 handle functions which contain logarithms or exponentials of real numbers? Similarly, can cvc4 express the constant e?
According to this question, z3 can only handle constant exponents, which does not help me.
This question only asks about logarithms for integers.
I am unfamiliar with cvc4 but I perhaps have some useful properties about logarithms that you may be able to exploit based on your limitations.
Technically speaking, no computer (no matter how powerful) knows what e is because it is transcendental (cannot be expressed as the solution to a polynomial equation with rational coefficients).
If you are limited such that you can only take logarithms for integers, you can express e as a faction approximation and solve it that way. The formula ends up being a bit longer than just taking the logarithm directly but the advantage is that you can effectively calculate the logarithm where the base is any rational number, while only individually finding logarithms of whole numbers.
Let e be approximated by the fraction a/b where both a and b are integers.
(a/b)^n = x
log(base a/b)(x) = n
This doesn't really get you anywhere so we have to take a different route that requires a bit more algebra.
(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))
In other words, log(base a)(x) / (1 - log(base a)(b)) is an approximation for ln(x) where a/b is an approximation of e. Obviously, this approximation for ln(x) gets closer to the real value of ln(x) as a/b more closely approximates e. Note I kept this in a general form here that a/b could represent any rational number, not just e.
If this doesn't answer your question fully, I hope it at least helps.
Just tried an arbitrary example.
If you consider a and b as 27183 and 10000 respectively, I tried this quick calculation:
log(base 27183)(82834) / (1 - log(base 27138)(10000)) = 11.32452...
ln(82834) = 11.32459...