Support for class Constants

[CatarinaGamboa]

We did not support using static final fields from classes in predicates or using the values in Java code.
For example, both these cases would not have been possible before, and now are acceptable

    static void clampInt(@Refinement("_ >= Integer.MIN_VALUE && _ <= Integer.MAX_VALUE") int x) {
    }

    public static void main(String[] args) {
        clampInt(0);
        clampInt(Integer.MAX_VALUE);
    }

• Resolution follows Java scoping rules: fully-qualified name → compilation-unit imports (single + on-demand) → implicit java.lang, with reflection as the source-of-truth. User-defined enums/classes are left untouched for the existing SMT path.
• Based on reflection, find the declaration and get the value assigned to it, and add it as a value.

[CatarinaGamboa]

Do we need to call this all the time?

it will just see if there are enums to resolve in a small expression, if there are no enums it doesnt do anything else, so its fine

[CatarinaGamboa]

@rcosta358 I'm not sure how this affects error messages as it will appear directly with the value in the SMT, but there is no link between the var and its value so we might need a followup pr to handle that

[rcosta358]

Can't we treat those as variables instead? That way we'll solve that for free.

[CatarinaGamboa]

Can't we treat those as variables instead? That way we'll solve that for free.

we can add a new expression with the equality instead of replacing it, is that what you mean?

[rcosta358]

Yep, exactly, that way we can also expand them to their values in the simplification.

[CatarinaGamboa]

We keep the resolved value here instead of substituting it

[rcosta358]

LGTM. Also fixed some issues, namely improving the error messages related to static final fields, referencing local static final fields (which don't need to be imported), and resolving static final char fields.