mCRL2
mCRL2 copied to clipboard
Implement number by native integers.
This branch replaces the rewrite systems for positive and natural numbers based on a binary number representation (using the constructor @cDub) by a representation based on 64 bit machine numbers.
The major changes are 1) the addition of a "machine_number" to data_expressions; This entails that data_expressions inherit from aterm, and not from aterm_appl anymore. 2) The addition of the the keywords "defined_by_rewrite_rules" to indicate that a mapping or constructor is defined by explicit C++ code. 3) An adaption of the jitty and jittyc rewrite systems to recognise that a function symbol is implemented by explicit code. 4) Addition of a file machine_word.spec defining operations on machine numbers. 5) A replacement of the files pos.spec and nat.spec by a new version that employs machine numbers. 6) A new test to test that large numbers (with up to a hundred decimal digits) are correctly calculated.
From the perspective of mCRL2 users the changes should be completely transparent, except that the performance is changing, sometimes appr. 10% slower (esp. the jitty rewriter), sometimes many hundreds of times faster (jittyc rewriter, for instance calculating 100000!).
This pull request allows teamcity to test this branch.
I rebased the branch on master. There were some minor merge conflicts, especially with commit 3ff435a8fcaf4c64180399850485793054f8f205. I resolved those by running the generate_data_types.py
script repeatedly.