Sum() on floating point values in Z3

I'm trying to write something to solve for a variable amount of floating point variables given the expected average. However, I get this exception when trying to run my code.

z3.z3types.Z3Exception: b'Sort mismatch at argument #1 for function (declare-fun + (Int Int) Int) supplied sort is (_ FloatingPoint 8 24)'

It looks like Sum() doesn't work on floating point values for some reason. That, or I'm just doing something wrong.

Here's some minimal reproduction code:

from z3 import *

l = [FP('x', Float32()), FP('y', Float32()), FP('z', Float32())]
s = Solver()
#s.add(Sum(l) == 100) # uncomment for exception
s.add(l[0] + l[1] + l[2] == 100)
s.check()
print(s.model())

Solution

You are not doing anything wrong. It's just that the Sum method as exported by z3py API only supports bit-vectors, integers, and reals. In particular, it does not allow for floating-point values.

There's no reason why it shouldn't, and you can file this as a missing feature in their issue tracker: https://github.com/Z3Prover/z3/issues

(If you do so, you can also mention that the Product function has the same shortcoming; so they can fix it together.)

In the meantime, I recommend defining your own method. Something like this:

from z3 import *

import functools

def MySum(lst):
    return functools.reduce(lambda a, b: a + b, lst, 0);

l = [FP('x', Float32()), FP('y', Float32()), FP('z', Float32())]
s = Solver()
s.add(MySum(l) == 100)
s.check()
print(s.model())

Note that MySum is sufficiently polymorphic: You can use it on Ints, Reals, Floats, BitVec types, and it'll all work. What it's not doing, of course, checking to make sure that what you're passing is indeed things that you can sum, i.e., say not enumerations or some other data-type. (And in essence, that's what the internal API method is trying to do: It's checking that what you are passing is meaningful to sum up, except they missed the case for the floats.)