Add Null & Boxed Types Support

[rcosta358]

This PR adds support for null checking in LiquidJava.
It also allows us to refine boxed types which previously were also not supported (Integer, Boolean, Short, Long, Float and Double).

Changes

Refinements Language

• Added the null literal to the grammar
• Added the LiteralNull AST node

Typing

• The literal null can be assigned to any non-primitive type
• String literals, literals of boxed types and new object instances implicitly carry the refinement _ != null, while the literal null carries the refinement _ == null

Z3 Translation

• Nulls are converted to uninterpreted constants of the uninterpreted sort java.lang.Object
• In equality comparisons, null literals are converted to the sort of the other operand to match both sorts
• Boxed types are now mapped to the same Z3 sorts as their primitive types (e.g., java.lang.Integer => Int) to avoid errors like “Sorts java.lang.Integer and Int are incompatible"

Simplification

• The simplifier removes redundant null checks when an equality to a non-null literal already implies a non-null value. This way, s == -1 && s != null simplifies to s == -1 instead of -1 != null

Testing

• Added various tests to ensure the correctness of these changes