Applied fixes and suggestions for enums

Created AST node and visitors for enums. Changed grammar as suggested to specific rules and positioning to avoid ambiguity. Changed format.
liquid-java · rcosta358 · Apr 11, 2026 · Mar 3, 2026 · Mar 3, 2026 · Mar 4, 2026
commit a359d1f9c5a33345c9905f11d9fecf0a71ca9e8f
diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
@@ -57,7 +57,7 @@ aliasCall:
 	ID_UPPER '(' args? ')';
 
 enumCall: 
-	OBJECT_TYPE;
+	ENUM_CALL;
 
 args:	pred (',' pred)* ;
 
@@ -97,6 +97,7 @@ BOOLOP	 : '=='|'!='|'>='|'>'|'<='|'<';
 ARITHOP : '+'|'*'|'/'|'%';//|'-';
 
 BOOL    : 'true' | 'false';
+ENUM_CALL: [a-zA-Z_][a-zA-Z0-9_]* '.' [a-zA-Z_][a-zA-Z0-9_]*;
 ID_UPPER: ([A-Z][a-zA-Z0-9]*);
 OBJECT_TYPE:
 		  (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);

diff --git a/...a-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/...a-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
@@ -126,13 +126,9 @@ public <R> void visitCtMethod(CtMethod<R> method) {
     public <T extends Enum<?>> void visitCtEnum(CtEnum<T> enumRead) {
         String enumName = enumRead.getSimpleName();
         String qualifiedEnumName = enumRead.getQualifiedName();
-        int ordinal = 0;
-        for (CtEnumValue ev : enumRead.getEnumValues()) {
-            String varName = String.format(Formats.ENUM_VALUE, enumName, ev.getSimpleName());
-            Predicate refinement = Predicate.createEquals(Predicate.createVar(varName),
-                    Predicate.createLit(String.valueOf(ordinal), Types.INT));
-            context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), refinement);
-            ordinal++;
+        for (CtEnumValue<?> ev : enumRead.getEnumValues()) {
+            String varName = String.format(Formats.ENUM, enumName, ev.getSimpleName());
+            context.addGlobalVariableToContext(varName, qualifiedEnumName, enumRead.getReference(), null);
         }
         super.visitCtEnum(enumRead);
     }

diff --git a/...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java
@@ -271,7 +271,7 @@ public <T> void visitCtFieldRead(CtFieldRead<T> fieldRead) {
                     BuiltinFunctionPredicate.length(targetName, fieldRead)));
         } else if (fieldRead.getVariable().getDeclaringType().isEnum()) {
             String target = fieldRead.getVariable().getDeclaringType().getSimpleName();
-            String enumLiteral = String.format(Formats.ENUM_VALUE, target, fieldName);
+            String enumLiteral = String.format(Formats.ENUM, target, fieldName);
             fieldRead.putMetadata(Keys.REFINEMENT,
                     Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral)));
         } else {

diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Enumerate.java
@@ -0,0 +1,74 @@
+package liquidjava.rj_language.ast;
+
+import java.util.List;
+
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
+
+public class Enumerate extends Expression {
+
+    private final String enumTypeName;
+    private final String enumConstantName;
+
+    public Enumerate(String enumTypeName, String enumConstantName) {
+        this.enumTypeName = enumTypeName;
+        this.enumConstantName = enumConstantName;
+    }
+
+    public String getEnumTypeName() {
+        return enumTypeName;
+    }
+
+    public String getEnumConstantName() {
+        return enumConstantName;
+    }
+
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
+        return visitor.visitEnumerate(this);
+    }
+
+    @Override
+    public void getVariableNames(List<String> toAdd) {
+        // end leaf
+    }
+
+    @Override
+    public void getStateInvocations(List<String> toAdd, List<String> all) {
+        // end leaf
+    }
+
+    @Override
+    public boolean isBooleanTrue() {
+        return false;
+    }
+
+    @Override
+    public String toString() {
+        return enumTypeName + "." + enumConstantName;
+    }
+
+    @Override
+    public int hashCode() {
+        final int prime = 31;
+        int result = 1;
+        result = prime * result + ((enumTypeName == null) ? 0 : enumTypeName.hashCode());
+        result = prime * result + ((enumConstantName == null) ? 0 : enumConstantName.hashCode());
+        return result;
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null || getClass() != obj.getClass())
+            return false;
+        Enumerate other = (Enumerate) obj;
+        return enumTypeName.equals(other.enumTypeName) && enumConstantName.equals(other.enumConstantName);
+    }
+
+    @Override
+    public Expression clone() {
+        return new Enumerate(enumTypeName, enumConstantName);
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java
@@ -7,6 +7,7 @@
 import liquidjava.diagnostics.errors.SyntaxError;
 import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Enumerate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.GroupExpression;
@@ -161,7 +162,7 @@ else if (rc instanceof LitContext)
         else if (rc instanceof VarContext)
             return new Var(((VarContext) rc).ID().getText());
         else if (rc instanceof EnumContext) {
-            return new Var(enumCreate((EnumContext) rc));
+            return enumCreate((EnumContext) rc);
         } else {
             return create(((InvocationContext) rc).functionCall());
         }
@@ -237,13 +238,12 @@ private List<Expression> getArgs(ArgsContext args) throws LJError {
         return le;
     }
 
-    private String enumCreate(EnumContext rc) {
-        String enumText = rc.enumCall().getText();
+    private Enumerate enumCreate(EnumContext enumContext) {
+        String enumText = enumContext.enumCall().getText();
         int lastDot = enumText.lastIndexOf('.');
-        String enumClass = enumText.substring(0, lastDot);
-        String enumConst = enumText.substring(lastDot + 1);
-        String varName = String.format(Formats.ENUM_VALUE, enumClass, enumConst);
-        return varName;
+        String enumTypeName = enumText.substring(0, lastDot);
+        String enumConstName = enumText.substring(lastDot + 1);
+        return new Enumerate(enumTypeName, enumConstName);
     }
 
     private Expression literalCreate(LiteralContext literalContext) throws LJError {

diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
@@ -3,6 +3,7 @@
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Enumerate;
 import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
@@ -40,5 +41,7 @@ public interface ExpressionVisitor<T> {
 
     T visitUnaryExpression(UnaryExpression exp) throws LJError;
 
+    T visitEnumerate(Enumerate en) throws LJError;
+
     T visitVar(Var var) throws LJError;
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
@@ -5,6 +5,7 @@
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.rj_language.ast.AliasInvocation;
 import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Enumerate;
 import liquidjava.rj_language.ast.FunctionInvocation;
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
@@ -120,4 +121,9 @@ public Expr<?> visitUnaryExpression(UnaryExpression exp) throws LJError {
         default -> null;
         };
     }
+
+    @Override
+    public Expr<?> visitEnumerate(Enumerate en) throws LJError {
+        return ctx.makeEnum(en.getEnumTypeName(), en.getEnumConstantName());
+    }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java
@@ -1,6 +1,7 @@
 package liquidjava.smt;
 
 import com.microsoft.z3.Context;
+import com.microsoft.z3.EnumSort;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;
@@ -13,6 +14,8 @@
 import liquidjava.processor.context.GhostFunction;
 import liquidjava.processor.context.GhostState;
 import liquidjava.processor.context.RefinedVariable;
+import spoon.reflect.declaration.CtEnum;
+import spoon.reflect.declaration.CtType;
 import spoon.reflect.reference.CtTypeReference;
 
 public class TranslatorContextToZ3 {
@@ -41,19 +44,24 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
 
     private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
         String typeName = type.getQualifiedName();
+
+        if (type.isEnum()) {
+            CtType<?> decl = type.getDeclaration();
+            if (decl instanceof CtEnum<?> enumDecl) {
+                String[] enumValueNames = enumDecl.getEnumValues().stream().map(ev -> ev.getSimpleName()).toArray(String[]::new);
+                EnumSort<Object> enumSort = z3.mkEnumSort(typeName, enumValueNames);
+                return z3.mkConst(name, enumSort);
+            }
+        }
+
         return switch (typeName) {
         case "int", "short", "char", "java.lang.Integer", "java.lang.Short", "java.lang.Character" -> z3
                 .mkIntConst(name);
         case "boolean", "java.lang.Boolean" -> z3.mkBoolConst(name);
         case "long", "java.lang.Long" -> z3.mkRealConst(name);
         case "float", "double", "java.lang.Float", "java.lang.Double" -> (FPExpr) z3.mkConst(name, z3.mkFPSort64());
         case "int[]" -> z3.mkArrayConst(name, z3.mkIntSort(), z3.mkIntSort());
-        case "java.lang.Enum" -> z3.mkIntConst(name);
-        default -> {
-            if (type.isEnum())
-                yield z3.mkIntConst(name);
-            yield z3.mkConst(name, z3.mkUninterpretedSort(typeName));
-        }
+        default -> z3.mkConst(name, z3.mkUninterpretedSort(typeName));
         };
     }
 

diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
@@ -3,6 +3,7 @@
 import com.microsoft.z3.ArithExpr;
 import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.EnumSort;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;
@@ -26,6 +27,7 @@
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.utils.Pair;
 import liquidjava.utils.Utils;
+import liquidjava.utils.constants.Formats;
 import liquidjava.utils.constants.Keys;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
 
@@ -121,6 +123,11 @@ public Expr<?> makeVariable(String name) throws LJError {
         return expr;
     }
 
+    public Expr<?> makeEnum(String enumTypeName, String enumConstantName) throws LJError {
+        String varName = String.format(Formats.ENUM, enumTypeName, enumConstantName);
+        return getVariableTranslation(varName);
+    }
+
     public Expr<?> makeFunctionInvocation(String name, Expr<?>[] params) throws LJError {
         if (name.equals("addToIndex"))
             return makeStore(params);

diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java
@@ -5,5 +5,5 @@ public final class Formats {
     public static final String INSTANCE = "#%s_%d";
     public static final String THIS = "this#%s";
     public static final String RET = "#ret_%d";
-    public static final String ENUM_VALUE = "enum#%s#%s";
+    public static final String ENUM = "%s.%s";
 }