  We consider the problem of solving floating-point constraints obtained from
software verification. We present UppSAT --- a new implementation of a
systematic approximation refinement framework [ZWR17] as an abstract SMT
solver. Provided with an approximation and a decision procedure (implemented in
an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver.
Additionally, UppSAT includes a library of predefined approximation components
which can be combined and extended to define new encodings, orderings and
solving strategies. We propose that UppSAT can be used as a sandbox for easy
and flexible exploration of new approximations. To substantiate this, we
explore several approximations of floating-point arithmetic. Approximations can
be viewed as a composition of an encoding into a target theory, a precision
ordering, and a number of strategies for model reconstruction and precision (or
approximation) refinement. We present encodings of floating-point arithmetic
into reduced precision floating-point arithmetic, real-arithmetic, and
fixed-point arithmetic (encoded in the theory of bit-vectors). In an
experimental evaluation, we compare the advantages and disadvantages of
approximating solvers obtained by combining various encodings and decision
procedures (based on existing state-of-the-art SMT solvers for floating-point,
real, and bit-vector arithmetic).
