refactor(BV): Merge Congruence and Constraints (#1010)

* refactor(BV): Hide constraint representation

This patch makes the representation of bit-vector constraints abstract.
This is preparatory work for further refactoring, as there is no reason
to expose it outside of the `Constraint` module.

* refactor(BV): Extract signature of the `Constraint` module

This is in preparation of further refactoring work to make `Constraints`
a functor.

* refactor(BV): Fold `Congruence` into `Constraints`

In #944, the `Congruence` module was added to simplify handling
dependences for both domains and constraints, because we tracked domains
separately for all terms.

After #1004, we now track domains only for uninterpreted leaves, and the
`Congruence` module is only used for `Constraints`. This leads to a sort
of double indirection: the `Congruence` module keeps track of reverse
uninterpreted leaves -> class representative dependencies, and then the
`Constraints` module keeps track of reverse class representative ->
constraint dependencies.

This patch removes the `Congruence` module entirely; instead, the
`Constraints` module is now keeping track of reverse uninterpreted
leaves -> constraint dependencies directly.

Further refactoring work will move the `Congruence` module to
`Rel_utils` as it can be a generally useful module for other theories.

* refactor(CP): Generalize `Constraints` module

This patch moves the `Constraints` module from the BV theory to the
`Rel_utils` theory and make it a functor. This makes it independent from
the implementation of BV constraints and makes it useable in other
theories in the future.