mCRL2 icon indicating copy to clipboard operation
mCRL2 copied to clipboard

Implement number by native integers.

Open jgroote opened this issue 6 years ago • 1 comments

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.

jgroote avatar Jan 02 '19 15:01 jgroote

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.

tneele avatar Jan 03 '19 08:01 tneele