librumur: support for enum types
The implementation of these departs somewhat from CMurphi. Where CMurphi implements each member of each enum as a separate value (i.e. enum members in distinct enums will still have different numerical representations), we simply implement enums as C would. We'll need to do a little more work to prevent accidental comparison of distinct enum values, but this representation should allow us to more efficiently encode enum values in the state. This only matters for input models that contain large enum types, but empirically it seems like this is much more common than one might think. E.g. see [0]. The EnumValue class and related symbol table declaration implemented in this commit is a bit awkward. It would be nice to implement this in a cleaner way, but I couldn't immediately think of a better alternative. [0]: https://bitbucket.org/jderick/preach/commits/e7cecfc142253799bdf5d5cc5ed60015ec5cd0a8
parent
abeb93ee
Please register or sign in to comment