Add EnumType support to JavaSMT

ftsrg · Jun 26, 2024 · 4703cb0 · 4703cb0
1 parent 0915c18
commit 4703cb0
Show file tree

Hide file tree

Showing 8 changed files with 268 additions and 325 deletions.
diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTDeclTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTDeclTransformer.java
@@ -71,12 +71,17 @@ private Formula transformConst(final ConstDecl<?> decl) {
                     .toList();
 
 
-            if (paramSorts.isEmpty()) {
-                symbol = context.getFormulaManager().makeVariable(returnSort, symbolNameFor(decl));
-            } else {
+            if (!paramSorts.isEmpty()) {
                 throw new JavaSMTSolverException("Function consts not yet supported.");
             }
 
+            // Enums can't be yet handled by formulamanager directly
+            if (returnSort.isEnumerationType()) {
+                symbol = context.getFormulaManager().getEnumerationFormulaManager().makeVariable(symbolNameFor(decl), (FormulaType.EnumerationFormulaType) returnSort);
+            } else {
+                symbol = context.getFormulaManager().makeVariable(returnSort, symbolNameFor(decl));
+            }
+
             symbolTable.put(decl, symbol);
         }
 

diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java
diff --git a/...ts/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/...ts/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java
@@ -27,6 +27,8 @@
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.bvtype.BvLitExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvType;
+import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr;
+import hu.bme.mit.theta.core.type.enumtype.EnumType;
 import hu.bme.mit.theta.core.type.functype.FuncType;
 import hu.bme.mit.theta.solver.Solver;
 import hu.bme.mit.theta.solver.SolverStatus;
@@ -287,6 +289,8 @@ private <DeclType extends Type> LitExpr<?> extractLiteral(final ConstDecl<DeclTy
                 return extractArrayLiteral(formula);
             } else if (type instanceof BvType) {
                 return extractBvConstLiteral(formula);
+            } else if (type instanceof EnumType enumType) {
+                return extractEnumLiteral(formula, enumType);
             } else {
                 return extractConstLiteral(formula);
             }
@@ -311,6 +315,14 @@ private LitExpr<?> extractBvConstLiteral(final Formula formula) {
             }
         }
 
+        private EnumLitExpr extractEnumLiteral(Formula formula, EnumType enumType) {
+            final Formula term = model.eval(formula);
+            if (term == null) {
+                return null;
+            }
+            return enumType.litFromLongName(term.toString());
+        }
+
         private LitExpr<?> extractConstLiteral(final Formula formula) {
             final Formula term = model.eval(formula);
             if (term == null) {

diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java
diff --git a/...r-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformationManager.java b/...r-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformationManager.java
@@ -29,7 +29,7 @@ final class JavaSMTTransformationManager {
     private final JavaSMTExprTransformer exprTransformer;
 
     public JavaSMTTransformationManager(final JavaSMTSymbolTable symbolTable, final SolverContext context) {
-        this.typeTransformer = new JavaSMTTypeTransformer();
+        this.typeTransformer = new JavaSMTTypeTransformer(context);
         this.declTransformer = new JavaSMTDeclTransformer(this, symbolTable, context);
         this.exprTransformer = new JavaSMTExprTransformer(this, symbolTable, context);
     }

diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java
@@ -19,24 +19,34 @@
 import hu.bme.mit.theta.core.type.arraytype.ArrayType;
 import hu.bme.mit.theta.core.type.booltype.BoolType;
 import hu.bme.mit.theta.core.type.bvtype.BvType;
+import hu.bme.mit.theta.core.type.enumtype.EnumType;
 import hu.bme.mit.theta.core.type.fptype.FpType;
 import hu.bme.mit.theta.core.type.inttype.IntType;
 import hu.bme.mit.theta.core.type.rattype.RatType;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.EnumerationFormula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.SolverContext;
+
+import java.util.HashMap;
+import java.util.Map;
 
 final class JavaSMTTypeTransformer {
 
+    private final SolverContext solverContext;
     private final FormulaType<BooleanFormula> boolSort;
     private final FormulaType<IntegerFormula> intSort;
     private final FormulaType<RationalFormula> realSort;
+    private final Map<String, FormulaType<EnumerationFormula>> enumSorts;
 
-    JavaSMTTypeTransformer() {
+    JavaSMTTypeTransformer(final SolverContext solverContext) {
+        this.solverContext = solverContext;
         boolSort = FormulaType.BooleanType;
         intSort = FormulaType.IntegerType;
         realSort = FormulaType.RationalType;
+        enumSorts = new HashMap<>();
     }
 
     public FormulaType<?> toSort(final Type type) {
@@ -46,6 +56,8 @@ public FormulaType<?> toSort(final Type type) {
             return intSort;
         } else if (type instanceof RatType) {
             return realSort;
+        } else if (type instanceof EnumType enumType) {
+            return enumSorts.computeIfAbsent(enumType.getName(), name -> solverContext.getFormulaManager().getEnumerationFormulaManager().declareEnumeration(name, enumType.getLongValues()));
         } else if (type instanceof BvType bvType) {
             return FormulaType.getBitvectorTypeWithSize(bvType.getSize());
         } else if (type instanceof FpType fpType) {

diff --git a/subprojects/xsts/xsts-analysis/build.gradle.kts b/subprojects/xsts/xsts-analysis/build.gradle.kts
@@ -27,4 +27,5 @@ dependencies {
     testImplementation(project(":theta-solver-z3"))
     testImplementation(project(":theta-solver-z3-legacy"))
     testImplementation(project(":theta-solver-smtlib"))
+    testImplementation(project(":theta-solver-javasmt"))
 }
diff --git a/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java b/subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java
@@ -21,6 +21,7 @@
 import hu.bme.mit.theta.common.logging.Logger.Level;
 import hu.bme.mit.theta.solver.SolverFactory;
 import hu.bme.mit.theta.solver.SolverManager;
+import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverManager;
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager;
 import hu.bme.mit.theta.xsts.XSTS;
 import hu.bme.mit.theta.xsts.analysis.config.XstsConfig;
@@ -353,7 +354,7 @@ public static Collection<Object[]> data() {
 
     @BeforeClass
     public static void installSolver() {
-        if (SOLVER_STRING.contains("Z3")) {
+        if (SOLVER_STRING.contains("Z3") || SOLVER_STRING.contains("JavaSMT")) {
             return;
         }
         try (final var solverManager = SmtLibSolverManager.create(Path.of(SMTLIB_HOME), new ConsoleLogger(Level.DETAIL))) {
@@ -373,6 +374,7 @@ public void test() throws Exception {
         SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3legacy.Z3SolverManager.create());
         SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create());
         SolverManager.registerSolverManager(SmtLibSolverManager.create(Path.of(SMTLIB_HOME), logger));
+        SolverManager.registerSolverManager(JavaSMTSolverManager.create());
 
         final SolverFactory solverFactory;
         try {