Add support for Floating-Point theory (currently cvc5 only)

[augustomafra]

Adding sort and operation definitions for Floating-Point support on smt-switch.

This is a first step for other upcoming changes on pono's SMV frontend encoding problems on the theory of Floating-Point arithmetic.

[augustomafra]

Hi, @CyanoKobalamyne ,

I see that one CI test failed on my fork with "ERROR: Could not install packages due to an OSError: [Errno 28] No space left on device". Is there anything I can set on my end to have this test running on github? I relaunched it a couple of times but still hit the same issue.

Thanks!

[augustomafra]

Hi, @CyanoKobalamyne ,

Could you or other project maintainers share feedback about this PR?
I have merged it to the latest commit in main (version 1.0.6), so please let me know if there is anything else I can adjust on my request.
I'm currently working on my thesis to wrap up my Master's project at https://github.com/augustomafra/pono, so any thoughts from the Pono maintainers would be greatly appreciated, if possible.

Thanks!

[yoni206]

Hi @augustomafra and thanks for this PR, and sorry for the delay!
It would be great for smt-switch to support floating points.

In addition to the inline comments, could you add tests to the PR? I think it would make sense to add cvc5 tests here:
https://github.com/augustomafra/smt-switch/tree/63258f708b798a34a46a6ddaf7252ece4612af5b/tests/cvc5

and more generic tests (though they would now only run with cvc5) here:
https://github.com/augustomafra/smt-switch/tree/63258f708b798a34a46a6ddaf7252ece4612af5b/tests

This would include updating this file:
https://github.com/augustomafra/smt-switch/blob/63258f708b798a34a46a6ddaf7252ece4612af5b/tests/available_solvers.cpp

[yoni206]

Can you also add python bindings as mentioned in the line below?

[yoni206]

Is there a reason only these two are added, and not generic floats, indexed by integer parameters? This would be then more consistent with the SMT-LIB standard, and can be done similarly to bit-vectors.

[augustomafra]

Agreed, I will work on switching to the generic float type.
At first I assumed specialized types would be easier to adopt for my application, but when advancing in the project I noticed that I spent more effort in getting the indexes for each type when translating to the solver APIs. The templates were a way to work around that, but as you commented below, they shouldn't be needed anymore after changing to general floats.

[yoni206]

templates are rare in smt-switch so far, and i wonder if we really need them here.

[augustomafra]

Hi, @yoni206 , thanks for the directions!
I will work on the changes you suggested and update the PR. Right now I'm focused on writing my thesis, so I may take a while to return to the code.