Changed decision selection.

The solver now first asks all theories for decision literals before deciding
the next literal from the atom queue.  Only if no theory suggests a literal,
the usual decision heuristics is used.
Introduced logic QF_AUFLIRA.

The logic QF_AUFLIRA is introduced similarly to QF_UFLIRA, but with the
addition of arrays.  Additionally, LIRA-unsatisfiable equalities like
(= intvar 0.5) are detected and simplified in the preprocessor.  This is not
a soundness fix, but a performance enhancement since we do not need to
generate cuts for these equalities anymore.