Update saturation to reflect the theory

Changes are:
 - Clauses are normalized but (by default) non-normal clauses are not dropped.
 - Conseq is not used at all on extensions. Before, conseq was used but the
   plus clause was forbidden for extensions.
 - Identical statements are not normalized to one side (by default).

In some cases I've added customizable flags, in some cases I've just edited
the procedure... perhaps we should simplify everything at some point to make
things most readable.
Check for generalizations

The theory requires that a clause is never dropped if it has a specialization
that has been kept. This was actually already ensured by our strategy, as
shown by the new check added here, which was ran on the validation suite.
This check is done in a naive and very costly way, so it is disable by
default; use --check-generalizations to enable.