title: Python -- Optimize system of inequalities
body: <p>I am working on a program in Python in which a small part involves optimizing a system of equations / inequalities. Ideally, I would have wanted to do as can be done in Modelica, write out the equations and let the solver take care of it. </p>
  
  <p>The operation of solvers and linear programming is a bit out of my comfort zone, but I decided to try anyway. The problem is that the general design of the program is object-oriented, and there are many different possibilities of combinations to form up the equations, as well as some non-linearities, so I have not been able to translate this into a linear programming problem (but I might be wrong) .</p>
  
  <p>After some research I found that the <a href="https://github.com/Z3Prover/z3" rel="noreferrer">Z3</a> solver seemed to do what I wanted. I came up with this (this looks like a typical case of what I would like to optimize):</p>
  
  <pre><code>from z3 import *
  
  a = Real('a')
  b = Real('b')
  c = Real('c')
  d = Real('d')
  e = Real('e')
  g = Real('g')
  f = Real('f')
  cost = Real('cost')
  
  opt = Optimize()
  opt.add(a + b - 350 == 0)
  opt.add(a - g == 0)
  opt.add(c - 400 == 0)
  opt.add(b - d * 0.45 == 0)
  opt.add(c - f - e - d == 0)
  opt.add(d &lt;= 250)
  opt.add(e &lt;= 250)
  
  opt.add(cost == If(f &gt; 0, f * 50, f * 0.4) + e * 40 + d * 20 + 
    If(g &gt; 0, g * 50, g * 0.54))
  
  h = opt.minimize(cost)
  opt.check()
  opt.lower(h)
  opt.model()
  </code></pre>
  
  <p>Now this works, and gives me the result I want, despite it not being extremely fast (I need to solve such systems several thousands of times). 
  But I am not sure I am using the right tool for the job (Z3 is a "theorem prover"). </p>
  
  <p>The API is basically exactly what I need, but I would be curious if other packages allow a similar syntax. Or should I try to formulate the problem in a different way to allow a standard LP approach? (although I have no idea how)</p>