Add SMT-LIB theory of floating point numbers: Part I

[Fe-r-oz]

This PR introduces an initial implementation of FloatingPointExpr based on the SMT-LIB FloatingPoint theory. While I’ve reviewed the SMT-LIB documentation, I’m still familiarizing myself with SMT-LIB format, so the implementation would need refinement. I plan to add more correctness checks and implement any the essential features (based on SMT-LIB) in future updates.

I would appreciate feedback to better understand the current state of this PR and identify the next steps to align it with the rest of the API. Additionally, I anticipate needing another PR to focus on interoperability between FloatingPointExpr, IntExpr, BitVectorExpr, and RealExpr as that is not done in this PR (although there is basic conversion from IntExpr to FPExpr and RealExpr to FPExpr , which will also require unit testing.

Please help review this PR, thank you!

Edit:

After re-reading the SMT specification, it seems that conversion to/from other sorts needs to be further polished. I have not used BitVectorExpr as some specification also uses this type as well

[codecov]

Codecov Report

Attention: Patch coverage is 67.41573% with 29 lines in your changes missing coverage. Please review.

Project coverage is 88.49%. Comparing base (dfb5585) to head (c36c702).

Files with missing lines	Patch %	Lines
src/FloatingPointExpr.jl	67.41%	29 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##             main      #83      +/-   ##
==========================================
- Coverage   90.34%   88.49%   -1.85%     
==========================================
  Files          12       13       +1     
  Lines        1015     1104      +89     
==========================================
+ Hits          917      977      +60     
- Misses         98      127      +29     

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

[Fe-r-oz]

Hi, Emi! Please let me know your thoughts and perspective on this! I’ve added some basic tests—they’re pretty basic for now, but it's a start! My main concern is to make sure its interoperable with the existing theories and more correctness checks, which I hope would be part two!