Floating point infrastructure

I think this is the complete infrastructure required to add a floating-point solver, but I am still in the process of checking it.

Outstanding issues:

1. What should the copyright assignment say?
2. The are a few instructions that I didn't know how to parse.
3. I need to check if there are any updates to the theory that need to be encorporated.

This ordering is not only the ordering that is used for building the theory subdirs, but also the order in which theories get assigned internal IDs, and thus the order they are called in for check()/etc.  We might want to move fp earlier, certainly before quantifiers (which expects to go last---and idl is a special case since as a replacement procedure it actually has the same ID as the arith theory).  I'd suggest around the same place as bv, depending on how you handle the encoding in the future you may want it just before bv.