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

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?

• Z3 (and z3py) has an If function. See the documentation. Not at all obvious that Z3 is a good tool for this problem. Feb 8 at 4:26
• @erwin-kalvelagen, what is a proper tool for this problem? It must be fast because I must run this frequently with ~1440 variables. Feb 8 at 5:54
• Of course, it depends on many things (characteristics of the model, nonlinearities, amount of money available to buy solvers, academic/commercial etc.). 1440 variables is usually small these days. Feb 8 at 6:54
• @ErwinKalvelagen I am in the academic context, but I prefer free software solutions. I am working on this or.stackexchange.com/questions/9853/…, which is non-linear. I hear open-source solvers are not close to commercial ones. But could Pulp be good enough? Feb 8 at 7:09
• That is not a very well-researched question: (1) PuLP is not a solver and (2) PuLP only supports linear models. I would suggest to do a little bit of a literature search, and see what colleagues did. That can help with the modeling part and give an idea about the kind of solvers used for your type of model. Feb 8 at 7:54

        obj_func += (soc[i - 1] - soc[i]) * \