How to change the price in the objective function, depending on its sign, in python, with Z3?

Question

My objective function is

$$ f_{objective} = \sum_{n=0}^{m} \int\limits_{I_n}^{I_n + \Delta i_n} P_{normal}(t) \,dt - \int\limits_{S_n}^{S_n + \Delta s_n} P_{CO_2}(t) \,dt $$

($P(t)$ is the price,) and it boils down to this in python:

        ...

        obj_func += self.price(soc[i - 1] - soc[i], i)

        ...

def price(self, delta_soc, index):
    if delta_soc >= 0:
        return delta_soc * self.data["price_co2"][index]
    else:
        return delta_soc * self.data["price"][index]

except it does not work like that. I get the error message.

z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.

and I understand why that is. But how can I work around that? Is there a trick so I can sell at another price than when I buy?

Answer 1

It took me a while to get the syntax right, so I share it for later generations. This seems to work as intended:

        obj_func += (soc[i - 1] - soc[i]) * \
                    z3.If(soc[i - 1] >= soc[i],
                          self.data["price"][i],
                          self.data["price_co2"][i])