How to predict a integer number with v8 z3

[TuranGM]

when I'm putting 5 numbers from:

[2353, 2497, 2281, 2400, 2184, 2208, 2472, 2448, 2232, 2257, 2305, 2160, 2329, 2424, 2376][Math.floor(Math.random() * 15)]
And it gives me an empty answer.

But when I put there 5 numbers which I got with:

[2353, 2497, 2281, 2400, 2184, 2208, 2472, 2448, 2232, 2257, 2305, 2160, 2329, 2424, 2376][Math.floor(Math.random() * 15)]
It doesn't work.As I said it gives me empty answer. So my question is what I have to change to predict integer number (preferably with numbers which I get using [2353, 2497, 2281, 2400, 2184, 2208, 2472, 2448, 2232, 2257, 2305, 2160, 2329, 2424, 2376][Math.floor(Math.random() * 15)])

[TuranGM]

I think I have to change something in xorShift128+ code.But I don't know what.

[1-alex98]

There are a lot of floating point numbers that can result in whole number. Let's say you do Math.floor(Math.random() * 15) and the outcome is 14. There are dozens of floating point numbers that could have resulted in this. Hence you have to span a huge equation that needs solving. It is certainly possible but seems to be quite a bit more difficult.

[1-alex98]

I got it to work
https://gist.github.com/1-alex98/0d26a800b5ee0b88ff8b2b550136f259
But if the multiplier is to small. 15 is too small it will print wrong numbers. To be honest I expected it to not be solver.check() == z3.sat then but it says it is satisfied but then spits out garbage.

[TuranGM]

I understand. Thanks for information!

[1-alex98]

Well to be honest I am not even sure if it works at all

[TuranGM]

Well to be honest I am not even sure if it works at all

Maybe. Honestly I tried lot of things. But it didn't work.

[1-alex98]

Ok well it seems to work if there are around 25 entries and the multiplier is 2000. But it is really hard to tell when it has enough data to make a correct prediction.

[1-alex98]

Ok after some more research. I can also let z3 tell me if there is a unique solution.
https://gist.github.com/1-alex98/0d26a800b5ee0b88ff8b2b550136f259#file-gistfile1-txt-L159
So it seems like you need at least a multiplier of around 2000 for it to have a unique solution or a lot of numbers. But if you add to many numbers it runs really long(potentially forever).

[matthewoestreich]

I ported this to Node - it was a huge pain!! Learned a lot, though!

Turned it into an NPM package that can also run as CLI...