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]
        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?

  • $\begingroup$ Z3 (and z3py) has an If function. See the documentation. Not at all obvious that Z3 is a good tool for this problem. $\endgroup$ Feb 8 at 4:26
  • $\begingroup$ @erwin-kalvelagen, what is a proper tool for this problem? It must be fast because I must run this frequently with ~1440 variables. $\endgroup$ Feb 8 at 5:54
  • 2
    $\begingroup$ 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. $\endgroup$ Feb 8 at 6:54
  • $\begingroup$ @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? $\endgroup$ Feb 8 at 7:09
  • 1
    $\begingroup$ 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. $\endgroup$ Feb 8 at 7:54

1 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],
  • $\begingroup$ While this should work in principle, it is not useable in z3. Z3 becomes super slow and does not terminate. $\endgroup$ Feb 13 at 8:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.