Non-i32 IntCst in solver?

[ishehadeh]

Hi, apologies for the naive question. Is there any reason (other than performance) for the IntCst type to always be i32? Would it make sense to have numbers base on i64 or even arbitrary numbers that have the required num-traits methods?

If so, I'd be happy to try tackling the implementation.

Looking into this a bit it seems like the biggest issues are:

1. Theres an larger integer type used to store the result of computations int64 right now, so that would also have to be generic
2. Lots of as casts and numeric literals (i.e. assuming IntCst is a built-in int type)
3. A few places assume i32
4. (by far the biggest) a good chunk of the module assumes IntCst is Copy. I'm not sure the implications if this isn't true (even if all the borrow checker errors are fixed)

[arbimo]

Hi,

your assessment is very much correct. There is no fundamental reason why IntCst needs to be an i32 but there are a lot of good reason why it is.

First, it is important to realize that IntCst is the central type of the solver, together with VarRef. Everything revolves around those two types and essentially all exchanged information is based on this two types.

This has the implication that both performance and ergonomics are critical. The Copy property is essential for both and I don't see a way without it: even if we could maintain performance in the cases of interest, the ergonomics of the library would be to greatly impacted.

As for why 32 bits, the main gain is that a Lit (combination of a VarRef and an IntCst) fits on a single machine word (64 bits) which is very nice for performance. 32 bits also give largely enough precision for any combinatorial problem I can think of. The problems where I would actually require larger numbers can usually be handled by scaling (which is inconvenient but a small price to pay).

To answer your question. Yes, it may make sense to support i64, i128 or other Copy integral numeric types if there is a use case for them.
It would be possible to support them with feature flags to change the underlying IntCst type. There are probably a lot of small changes to do in support for this but it does not appear extremely hard.

[ishehadeh]

Thanks for the thorough reply!
I'll try adding support.

I'm interested in this feature since because I'm trying to use a constraint solver to narrowing integer types in a toy programming language. I know, It's an oddly specific case 😅