Currently IPASIR uses int whenever it denotes the type of a literal.
Problem
This generally is not FFI friendly since int does not have a fixed size and could theoretically be anything between 16-bit to 64-bit. Practically it is 32-bit on most platforms but there is no guarantee.
If two programs compiled with different assumptions for the size of int were to communicate with each other over the IPASIR interface this would lead to failure.
Changing int to int32_t should not break IPASIR users since most (if not all) production ready solvers use 32-bit integers for their literal representation anyways. With this PR this information is now also encoded.
Future Enhancementss
Even though it would make sense for IPASIR to only use fixed-sized integer types in general I did not replace any other types since the literal type notation is the most important at this point and also I wanted to keep the PR small and contained.
Downsides
One downside of using the standard C header <stdint.h> (with C++ it is <cstdint>) is that the type int32_t might not be available since it is marked as optional. However, in these cases we are on either an 8-bit or 16-bit platform and probably do not want to run a SAT solver anyways.
This is a breaking change, however to my personal understanding it would only break in scenarios that are already broken due to the problem stated above or in cases where both client and solver use 64-bit literals so far.
My personal motivation for this to be merged is that I would feel far more confident with my IPASIR bindings from another language.
Currently IPASIR uses
intwhenever it denotes the type of a literal.Problem
This generally is not FFI friendly since
intdoes not have a fixed size and could theoretically be anything between 16-bit to 64-bit. Practically it is 32-bit on most platforms but there is no guarantee.If two programs compiled with different assumptions for the size of
intwere to communicate with each other over the IPASIR interface this would lead to failure. Changinginttoint32_tshould not break IPASIR users since most (if not all) production ready solvers use 32-bit integers for their literal representation anyways. With this PR this information is now also encoded.Future Enhancementss
Even though it would make sense for IPASIR to only use fixed-sized integer types in general I did not replace any other types since the literal type notation is the most important at this point and also I wanted to keep the PR small and contained.
Downsides
<stdint.h>(with C++ it is<cstdint>) is that the typeint32_tmight not be available since it is marked as optional. However, in these cases we are on either an 8-bit or 16-bit platform and probably do not want to run a SAT solver anyways.My personal motivation for this to be merged is that I would feel far more confident with my IPASIR bindings from another language.