usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

Handle properly `Number` abstraction and concrete types `Real` and `Integer` #752

Open Tomaqa opened 3 months ago

Tomaqa commented 3 months ago

Currently, everything is actually a real type so computation with integers is inefficient. Moreover, sometimes the types may be used interchangeably although an explicit conversion would be more appropriate.

Consider using std::variant, maybe even with CRTP for defining a common interface of reals and integers, but it should not be necessary. https://gist.github.com/olibre/3d0774df0f7a16e2da10fae2b2f26c4f