Redesign of BTOR encoder, includes lazy casting

[makaimann]

This would restructure the BTOR encoder to use a dictionary look-up for each function, instead of a sequence of ifs. Furthermore, it lazily casts between bool and BV(1) with a preference for BV(1).

This is passing tests locally, but I'm not sure that it's ready to be merged yet which is why it's a draft. In particular, I'm not sure that it's robust to updates. For example, it expects the exact right number of tokens on each line, based on the operator. Yosys occasionally appends wirenames to a line, even if they're not state elements (which I don't think is standard BTOR), so we have to search for these and remove them before passing to the dictionary-lookup functions. Do you think this makes sense or would you prefer a different approach?