Optionally encode floating point operations as uninterpreted functions

[can-leh-emmtrix]

In our ongoing work with alive2, we often encountered cases where floating point operations remain largely unchanged while other parts of the function differ. Since, Z3's floating point theory is quite slow I am looking at using uninterpreted functions to (over) approximate these floating point operations.

This PR adds a new command line option --uf-float that encodes all floating point operations using uninterpreted functions. The encoding is a conservative approximation, meaning that if a counter-example for the approximation is found, it is not necessarily a valid counter example.

Commutativity for FPBinOp and FCmp is encoded using the encoding proposed by Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo, and Juneyoung Lee in "SMT-based Translation Validation for Machine Learning Compiler.". It does not use the other parts of the encoding. It might be interesting to encode properties other than commutativity as well though.

I decided to open this PR as a draft, to see if there is interest in upstreaming this feature and get some feedback on the direction.

Related: https://github.com/AliveToolkit/alive2/issues/916

[regehr]

so my (now former) student Zhengyang has been using floats-as-UF in his Alive-based superoptimizer. @zhengyang92 do you have feedback on this?

[can-leh-emmtrix]

I'd consider this ready for review now.

As the diff is quite large, I'd recommend looking at the first three commits individually and then looking at the diff between the third and last commit.

The main reason for the large diff is that implementing the --uf-float option required indenting the existing code:

if (is_uf_float()) {
  <create UF>
} else {
  <existing code>
}