Add support for mutual recursion between the BV and the boolean fragment

[hargoniX]

If we want to support features like if statements efficiently it is necessary to process theory terms that consist e.g. of some BV logic which contains a boolean term which contains again further BV logic etc. The main connective here is BitVec.ofBool.

[hargoniX]

Idea: As we preprocess, for each subterm of the form BitVec.ofBool x that we encounter we add the following statements to the context:

• x -> BitVec.ofBool x = 1
• !x -> BitVec.ofBool x = 0
  This must also be recursive within x as it might contain further BitVec logic.

The bv_unsat logic will pick up BitVec.ofBool x as an atom and thus recognize and encode these theorems properly.