search

usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Separated integers from rationals and added simple `FastInteger` wrapper #751

Open Tomaqa opened 3 months ago

Tomaqa commented 3 months ago

Existing FastRational class contained some functions that are not related to rationals but to integers. I fixed this by making a derived class FastInteger and moving these specific functions there.

Tomaqa commented 3 months ago

I also corrected arithmetic operations s.t. they return FastInteger and not FastRational.

Tomaqa commented 3 months ago

I also experimented with a clearer distinction between Real and Integer, but it turned out to require quite a lot of work, so I gave up. The current solution partially divides the usage of the types, but it still uses integer operations on rational arguments while using static_cast on them. This is (currently) safe and the performance should be the same as before. But the current solution requires to explicitly cast/convert the arguments to integers, making it clearer what is going on.