Extracted enum logic to its own method

Author: cheestree

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorContextToZ3.java

@@ -22,21 +22,8 @@ public class TranslatorContextToZ3 {
 
     static void translateVariables(Context z3, Map<String, CtTypeReference<?>> ctx,
             Map<String, Expr<?>> varTranslation) {
-        // Create EnumSorts and register enum literal constants, and create variable for enum if not present
-        Map<String, EnumSort<?>> enumSorts = new HashMap<>();
 
-        for (Map.Entry<String, CtTypeReference<?>> entry : ctx.entrySet()) {
-            String name = entry.getKey();
-            CtTypeReference<?> type = entry.getValue();
-            if (type.isEnum() && type.getDeclaration()instanceof CtEnum<?> enumDecl) {
-                EnumSort<?> enumSort = translateEnum(z3, varTranslation, enumSorts, type, enumDecl);
-                // translateEnum may have already registered name as a literal constant 
-                // (e.g. Mode.Photo), no need to overwrite
-                if (!varTranslation.containsKey(name)) {
-                    varTranslation.put(name, z3.mkConst(name, enumSort));
-                }
-            }
-        }
+        createEnumVariables(z3, ctx, varTranslation);
 
         for (Map.Entry<String, CtTypeReference<?>> entry : ctx.entrySet()) {
             String name = entry.getKey();
@@ -79,6 +66,27 @@ public static void storeVariablesSubtypes(Context z3, List<RefinedVariable> vari
         }
     }
 
+    /**
+     * Create EnumSorts and register enum literal constants, and create variable for enum if not present
+     */
+    public static void createEnumVariables(Context z3, Map<String, CtTypeReference<?>> ctx,
+            Map<String, Expr<?>> varTranslation) {
+        Map<String, EnumSort<?>> enumSorts = new HashMap<>();
+
+        for (Map.Entry<String, CtTypeReference<?>> entry : ctx.entrySet()) {
+            String name = entry.getKey();
+            CtTypeReference<?> type = entry.getValue();
+            if (type.isEnum() && type.getDeclaration()instanceof CtEnum<?> enumDecl) {
+                EnumSort<?> enumSort = translateEnum(z3, varTranslation, enumSorts, type, enumDecl);
+                // translateEnum may have already registered name as a literal constant
+                // (e.g. Mode.Photo), no need to overwrite
+                if (!varTranslation.containsKey(name)) {
+                    varTranslation.put(name, z3.mkConst(name, enumSort));
+                }
+            }
+        }
+    }
+
     private static Expr<?> getExpr(Context z3, String name, CtTypeReference<?> type) {
         String typeName = type.getQualifiedName();