C library: add exp, log, pow models

[tautschnig]

The implementation follows Nicol N. Schraudolph: "A Fast, Compact Approximation of the Exponential Function," Neural Computation 11(4), 1999 and its discussion in
https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

@kroening and @martin-cs Would really appreciate your input on the proposed approximations.

[martin-cs]

Not unreasonable BUT we should probably decide on and document what the user can expect from our math library. The levels of accuracy are something like:

1. The C standard says essentially nothing.
2. IEEE-754 gives special cases but no requirements on accuracy.
3. Most implementations are within a few ULP ( https://members.loria.fr/PZimmermann/papers/accuracy.pdf ).
4. There are performant (at least for execution) implementations of correctly rounded functions available (https://core-math.gitlabpages.inria.fr/).

1 and 2 we can do easily but not everyone likes this #6999. I don't think we can realistically do 3 without using the actual implementations as the errors are very ideosyncratic of the implementations. For 3 and 4 and most of the implementations will completely sink the solver.

My feeling is that the right answer is to give overapproximate models of the functions such that the result always includes the correctly rounded result and then to support cr_* functions from N2596 http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2596.pdf from the solver up. If people care about the accuracy of their code they really should be using the correctly rounded functions.

But ... that's quite a bit of work and although it has been on my TODO for a while ... it hasn't got done yet so I guess any model is better than none.

[tautschnig]

I have now reworked the implementations to non-deterministically pick a result that is within the margin of error of approximation. This should be closer to soundness, but the caveats that @martin-cs called out do remain.

[codecov]

Codecov Report

All modified lines are covered by tests ✅

Comparison is base (e02fd74) 78.94% compared to head (ff137ae) 78.84%.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7906      +/-   ##
===========================================
- Coverage    78.94%   78.84%   -0.10%     
===========================================
  Files         1697     1697              
  Lines       195379   195379              
===========================================
- Hits        154242   154051     -191     
- Misses       41137    41328     +191     

see 22 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[kroening]

There may be a need to make this produce a bigger interval, given that the standards demand very little, but let's go for this for now.