python: relabel() and relabel_bse() should return the relabeling maps

One reason for relabeling a formula is if it must be passed to some tool that has a stricter syntax for atomic propositions. In that case we relabel all atomic proposition, call the tool, and do the reverse relabeling on the result.

Currently the python interface to relabel() and relabel_bse() returns a relabeled formula, but lose the information about what was renamed to what. We should definitely return this information, either as a Python dict, or as a black-box object that can be passed to another function to relabel in the oposite direction.