Allow floating point values in rank thresholds

[aco4]

https://github.com/Warzone2100/warzone2100/blob/master/data/mp/stats/brain.json

This file determines the experience a droid needs to obtain a certain rank. For example, a command droid requires 12 experience to obtain Green:

"CommandBrain01": {
    "name": "Command Turret",
    "ranks": [ "Rookie", "Green", "Trained", "Regular", "Professional", "Veteran", "Elite", "Special", "Hero" ],
    "thresholds": [ 0, 12, 24, 36, 48, 60, 72, 84, 96 ],
},
"ZNULLBRAIN": {
    "name": "Z NULL BRAIN",
    "ranks": [ "Rookie", "Green", "Trained", "Regular", "Professional", "Veteran", "Elite", "Special", "Hero" ],
    "thresholds": [ 0, 2, 4, 6, 8, 10, 12, 14, 16 ],
}

Floating point values currently seem to be rounded down. For example, a threshold of 12.5 seems to be treated as 12. I would like to be able to determine rank thresholds with floating point values.

Describe why do you think it is needed
Experience is already stored as a floating point value, and it would be nice to have finer control over these thresholds. No old behavior would be broken.

[aco4]

I was unable to find where in the game code these thresholds are parsed. If someone knows, I'd love to be pointed in the right direction.

[Monsterovich]

@aco4 #3705 (comment)

[aco4]

Oh, that's very unfortunate. But a reasonable explanation.

Correct me if I'm wrong, but in debug mode, clicking on a droid reveals its experience. It's always a value such as 12.2 or 9.0 or 6.8. i.e. only 1 decimal place of precision. Would it be possible (or easy enough) to simply multiply all the experience values by 10? Resulting in 122, 90, 68

Droid experience is indeed stored as a true floating point number, and cannot be easily converted into an integer.

[aco4]

I realize that I can use setExperienceModifier() to accomplish what I want