Make z3 use unified enum literal name transformation

RipplB · Oct 5, 2023 · 0aa36d3 · 0aa36d3
1 parent 6fd805f
commit 0aa36d3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java
@@ -254,7 +254,7 @@ private Expr<?> transformFpLit(final com.microsoft.z3.Expr term) {
 
     private Expr<EnumType> transformEnumLit(final com.microsoft.z3.Expr term, final EnumType enumType) {
         String longName = term.getFuncDecl().getName().toString();
-        String literal = longName.contains(".") ? longName.substring(longName.indexOf(".") + 1) : longName;
+        String literal = EnumType.getShortName(longName);
         return EnumLitExpr.of(enumType, literal);
     }
 

diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TypeTransformer.java
@@ -104,7 +104,7 @@ public void reset() {
     }
 
     private EnumSort createEnumSort(EnumType enumType) {
-        return context.mkEnumSort(enumType.getName(), enumType.getValues().stream().map(lit -> String.format("%s.%s", enumType.getName(), lit)).toArray(String[]::new));
+        return context.mkEnumSort(enumType.getName(), enumType.getValues().stream().map(lit -> EnumType.makeLongName(enumType, lit)).toArray(String[]::new));
     }
 
 }