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.

On Mon, 2014-10-06 at 09:03 -0700, Morgan Deters wrote:
> In src/Makefile.am:
> 
> > @@ -20,7 +20,7 @@ AM_CPPFLAGS = \
> >  AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
> >  
> >  SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
> > -THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers idl
> > +THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers idl fp
> 
> 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.
Ah.  OK.

>  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.

I've moved it after bv so that any definitions it generates will have
been resolved by the time check() gets called.

Cheers,
 - Martin