  This paper describes an ongoing effort to develop an optimizing version of
the Eldarica Horn solver. The work starts from the observation that many kinds
of optimization problems, and in particular the MaxSAT/SMT problem, can be seen
as search problems on lattices. The paper presents a Scala library providing a
domain-specific language (DSL) to uniformly model optimization problems of this
kind, by defining, manipulating, and systematically exploring lattices with
associated objective functions. The framework can be instantiated to obtain an
optimizing Horn solver. As an illustration, the application of an optimizing
solver for repairing software-defined networks is described.
