incorrect choco output for reference to a constant

[mantkiew]

For a model

abstract ASIL -> integer
A : ASIL -> 1
B : ASIL -> 2
C : ASIL -> 3
D : ASIL -> 4

the compiler produces

...
c0_ASIL.refToUnique(Int);
c0_A.extending(c0_ASIL).refTo(Int);
c0_B.extending(c0_ASIL).refTo(Int);
c0_C.extending(c0_ASIL).refTo(Int);
c0_D.extending(c0_ASIL).refTo(Int);

whereas the correct output should be

...
c0_ASIL.refToUnique(Int);
c0_A.extending(c0_ASIL).refToUnique(1);
c0_B.extending(c0_ASIL).refToUnique(2);
c0_C.extending(c0_ASIL).refToUnique(3);
c0_D.extending(c0_ASIL).refToUnique(4);

[JLiangWaterloo]

That's not supported right now by the backend (the refToUnique(1) part), but can't it be encoded easily with constraints like the following?

c0_A.extending(c0_ASIL);
c0_A.addConstraint(equal(joinRef($this()), 1));
c0_B.extending(c0_ASIL);
c0_B.addConstraint(equal(joinRef($this()), 2));
c0_C.extending(c0_ASIL);
c0_C.addConstraint(equal(joinRef($this()), 3));
c0_D.extending(c0_ASIL);
c0_D.addConstraint(equal(joinRef($this()), 4));

There would be no loss of efficiency since the backend has very good static analysis for these types of constraints and it will easily figure out that A/B/C/D must refer to 1/2/3/4 respectively.

[mantkiew]

Ok, I'll do it this way for int literals.