clingo icon indicating copy to clipboard operation
clingo copied to clipboard

Clingo only supports 32 bit ints even through it uses a 64 bit model

Open domoritz opened this issue 6 years ago • 13 comments

Clingo version says that it uses a 64 bit address model

clingo --version
clingo version 5.2.2
Address model: 64-bit

libgringo version 5.2.2
Configuration: with Python 3.6.4, without Lua

libclasp version 3.3.3 (libpotassco version 1.0.1)
Configuration: WITH_THREADS=1
Copyright (C) Benjamin Kaufmann

License: The MIT License <https://opensource.org/licenses/MIT>

However, large numbers start to wrap around.

$ echo 'a(2147483648).' | clingo
clingo version 5.2.2
Reading from stdin
Solving...
Answer: 1
a(-2147483648)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.001s

Is this intended behavior? I couldn't find any documentation for this.

domoritz avatar Mar 10 '18 04:03 domoritz

This is intended. Supporting 64 bit integers would greatly increase memory consumption.

rkaminsk avatar Mar 12 '18 20:03 rkaminsk

Thank you for the clarification! Is that limitation documented somewhere? I couldn't find any mention in https://www.mat.unical.it/aspcomp2013/files/ASP-CORE-2.03b.pdf. Would it make sense to add a warning in gringo when numbers overflow or underflow?

domoritz avatar Mar 13 '18 21:03 domoritz

Is that limitation documented somewhere?

I can't remember that we put it anywhere. Our guide could be a good place to add this information.

Would it make sense to add a warning in gringo when numbers overflow or underflow?

It might help, but it is not that easy to implement. A lot of places in the code would have to be adjusted. And the C/C++ language does not make it easy to check for these overflows.

rkaminsk avatar Mar 13 '18 22:03 rkaminsk

It might help, but it is not that easy to implement. A lot of places in the code would have to be adjusted. And the C/C++ language does not make it easy to check for these overflows.

Okay, I thought this could be added to the parser but I thought that without knowing how things are implemented. thanks for the clarifications. For now, I clamp all numbers to max int 32 when I generate ASP programs.

domoritz avatar Mar 13 '18 22:03 domoritz

For now, I clamp all numbers to max int 32 when I generate ASP programs.

Be careful when you use arithmetic in your program. Numbers might still overflow. If you do not need to use arithmetic, you could as well use strings, e.g., 1 becomes "1".

rkaminsk avatar Mar 13 '18 22:03 rkaminsk

I am going to mark this question with the enhancement label. In the future I might implement better handling of overflows. But don't expect anything soon.

rkaminsk avatar Mar 13 '18 22:03 rkaminsk

I would appreciate 64bit ints. perhaps with a switch as an argument or compilation option.

jachymb avatar Jun 08 '18 12:06 jachymb

There is no way to simply increase the size of the numbers supported by clingo.

rkaminsk avatar Jun 10 '18 15:06 rkaminsk

I would also like to suggest arbitrary large integers. I understand that deviating from 32 bit ints will impact performance but could there be a separate notation for bigints or a cli argument that enables big ints?

davidgrupp avatar Dec 12 '21 03:12 davidgrupp

Supporting big integers on the grounder side would be possible without sacrificing (much) performance. The solving part only supports minimize/sum constraints over 32 bit integers. Big integer constraints would have to be supported additionally because the performance hit would be noticeable. Another difficult part would be to expose them via the API. Then, there are also license issues. The gmp is GPL but there are (slower) MIT alternatives.

I'll keep these things in mind but don't expect anything to happen soon.

rkaminsk avatar Dec 12 '21 10:12 rkaminsk

@rkaminsk thanks for quick response

davidgrupp avatar Dec 13 '21 23:12 davidgrupp

Hi @rkaminsk, in theory, if I/someone were to create a fork with 64 bit numbers (not biginter), could you please comment on some assumptions/questions?

  • Implementing this probably isn't as easy as replacing some type definitions. Are there any major obstacles?
  • Apart from caching disadvantages, roughly the same performance could be expected on most CPUs
  • The memory consumption would be doubled at most

kherud avatar Jan 15 '24 10:01 kherud

Hi @rkaminsk, in theory, if I/someone were to create a fork with 64 bit numbers (not biginter), could you please comment on some assumptions/questions?

  • Implementing this probably isn't as easy as replacing some type definitions. Are there any major obstacles?

  • Apart from caching disadvantages, roughly the same performance could be expected on most CPUs

  • The memory consumption would be doubled at most

@kherud: I am currently working on this. I decided to add biginter support because this has the nice side effect that operations no longer overflow. Since this is a big change, integration into the system will still take some time.

rkaminsk avatar Jan 15 '24 10:01 rkaminsk