Replace BigInt, ieee_float and fixedbv

[mikhailramalho]

We should consider replacing the classes with boost::multiprecision:

https://www.boost.org/doc/libs/1_73_0/libs/multiprecision/doc/html/index.html

They provide custom integers and floating-point types already. We would have to write a custom fixed-point backend, but it doesn't look that hard since we already have all operations written in fixedbv.cpp.

By replacing them we can simplify constant_int2t, constant_fixedbv2t, and constant_floatbv2t, but making them inherit a single base class constant_number2t with a boost::multiprecision::number member.

This should allow us to remove a lot of duplicated code from the simplification algorithms.

[rafaelsamenezes]

Instead of replacing wouldn't it be simpler to reimplement BigInt using it? By making it a wrapper we would minimize the fixes needed if the api for multiprecision changes or if we want to use another library.

[mikhailramalho]

That's one approach but replacing BigInt with cpp_int should be straightforward... The biggest work would be implementing the fixedbv backend.

My point here is to remove theses formats (BigInt, ieee_floatt and fixebvt) with something more robust and supported by a wider community; these number formats are only maintained by us and there is always a huge effort when they are bugs to fix.

[rafaelsamenezes]

BTW, should we extend this replacement to other libraries that boost also implements? Good candidates may be XML manipulation and Graph generation.

[mikhailramalho]

XML sounds like a great idea. We already use it to generate the SV-COMP witnesses, but it should be expanded for other cases, like Test-Comp specification.

Where do you plan to use the graph lib?

[github-actions[bot]]

Stale issue message