change bounded -> finite; _is_finite_with_finite_vars

Variables that are already infinite cannot simply have their
attribute changed to finite or there will be a clash of
assumptions (i.e. inconsistent assumptions) so only those that
have finite=None will be changed. In addition, since variables
are identified by name and assumptions, to avoid collision with
an existing finite symbol with the same name, Dummy is used.
Merge pull request #7 from smichr/solver_refactor

Solver refactor