Convex quadratic optimisation modulo linear arithmetic
Optimisation modulo theories is a new paradigm in which one optimises
an objective function subject to a Boolean combination of linear
constraints. The open-source SMT-solver Z3 currently only supports
optimising linear objective functions. The goal of this project is to
add support for optimising convex quadratic functions to Z3 based on
the classical Frank-Wolfe algorithm.