How to define Integer log function

[rowanG077]

Hello everyone,

I'm interested in writing various helper mathematical function in Z3 to use in automated proofs. One of those functions is the Log function. I'm interested in writing both the ceiling Log, flooring log and a normal log. But even a normal log I can't get to work. Here I'm using Z3Py:

from z3 import *

s = Solver()

Z3_log = Function('log', IntSort(), IntSort(), IntSort())
base = Int('base')
value = Int('value')

s.add(ForAll([base, value], Z3_log(base, base ** value) == value))
s.add(ForAll([base, value], base ** (Z3_log(base, value)) == value))

but I get an exception:

Traceback (most recent call last):
  File "solve.py", line 29, in <module>
    s.add(ForAll([base, value], Z3_log(base, base ** value) == value))
  File "/nix/store/y7lsanlyyzc18abk7svp7v83d4rnq4zb-z3-4.8.14-python/lib/python3.8/site-packages/z3/z3.py", line 843, in __call__
    tmp = self.domain(i).cast(args[i])
  File "/nix/store/y7lsanlyyzc18abk7svp7v83d4rnq4zb-z3-4.8.14-python/lib/python3.8/site-packages/z3/z3.py", line 2312, in cast
    if val_s.is_bool() and self.is_int():
AttributeError: 'ArithSortRef' object has no attribute 'is_bool'

Is this expected? In addition how could I write the same log function but it should round up or down if it's it does not have an exact integer solution.

[LeventErkok]

The problem here is that ** always generates a real-valued result, regardless of the argument types:

>>> x = Int('x')
>>> (x ** x).sort()
Real

I'm not sure if this is on purpose, or if it's a bug. @NikolajBjorner can opine.

Assuming this is on purpose (or until the bug is fixed) you can write your axioms as:

from z3 import *

s = Solver()

Z3_log = Function('log', IntSort(), IntSort(), IntSort())
base = Int('base')
value = Int('value')

s.add(ForAll([base, value], Z3_log(base, ToInt(base ** value)) == value))
s.add(ForAll([base, value], ToInt(base ** (Z3_log(base, value))) == value))

Or, alternatively:

s.add(ForAll([base, value], Z3_log(base, ToInt(base ** value)) == value))
s.add(ForAll([base, value], base ** ToReal(Z3_log(base, value)) == ToReal(value)))

I'm not sure which version would be preferable. I doubt either will perform all that well without well-chosen pattern instantiations. But that's a tangential question.

[NikolajBjorner]

2 ** -1 is not an integer so the range type cannot be integer.

[NikolajBjorner]

is_bool was not defined, this was now fixed.

The original formula still throws an exception because the ** returns a Real, which is not a sub-sort of Int, as required by the signature of Z3_log. The formula isn't well typed.