OpenSMT: Use enums for the options that select an interpolation algorithm

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java

@@ -79,9 +79,12 @@ static SMTConfig getConfigInstance(
     config.setOption(":print-cores-full", optUnsatCore);
     config.setOption(":produce-interpolants", new SMTOption(interpolation));
     if (interpolation) {
-      config.setOption(":interpolation-bool-algorithm", new SMTOption(pSolverOptions.algBool));
-      config.setOption(":interpolation-euf-algorithm", new SMTOption(pSolverOptions.algUf));
-      config.setOption(":interpolation-lra-algorithm", new SMTOption(pSolverOptions.algLra));
+      config.setOption(
+          ":interpolation-bool-algorithm", new SMTOption(pSolverOptions.algBool.getValue()));
+      config.setOption(
+          ":interpolation-euf-algorithm", new SMTOption(pSolverOptions.algUf.getValue()));
+      config.setOption(
+          ":interpolation-lra-algorithm", new SMTOption(pSolverOptions.algLra.getValue()));
       config.setOption(
           ":simplify-interpolants", new SMTOption(pSolverOptions.simplifyInterpolants));
     }

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtSolverContext.java

@@ -26,6 +26,9 @@
 import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
 import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
 import org.sosy_lab.java_smt.solvers.opensmt.api.LogicFactory;
+import org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms.Core;
+import org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms.LA;
+import org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms.UF;
 
 public final class OpenSmtSolverContext extends AbstractSolverContext {
   private final OpenSmtFormulaCreator creator;
@@ -46,13 +49,13 @@ static class OpenSMTOptions {
     Logics logic = Logics.QF_AUFLIRA;
 
     @Option(secure = true, description = "Algorithm for boolean interpolation")
-    int algBool = 0;
+    Core algBool = Core.MCMILLAN;
 
     @Option(secure = true, description = "Algorithm for UF interpolation")
-    int algUf = 0;
+    UF algUf = UF.STRONG;
 
     @Option(secure = true, description = "Algorithm for LRA interpolation")
-    int algLra = 0;
+    LA algLra = LA.STRONG;
 
     @IntegerOption(min = 0, max = 4)
     @Option(

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/Core.java

@@ -0,0 +1,30 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
+
+public enum Core {
+  MCMILLAN(0),
+  PUDLAK(1),
+  MCMILLAN_PRIME(2),
+  PROOF_SENSITIVE(3),
+  PROOF_SENSITIVE_WEAK(4),
+  PROOF_SENSITIVE_STRONG(5);
+
+  private final int value;
+
+  Core(int i) {
+    value = i;
+  }
+
+  public int getValue() {
+    return value;
+  }
+}

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/LA.java

@@ -0,0 +1,29 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
+
+public enum LA {
+  STRONG(0),
+  WEAK(2),
+  FACTOR(3),
+  DECOMPOSING_STRONG(4),
+  DECOMPOSING_WEAK(5);
+
+  private final int value;
+
+  LA(int i) {
+    value = i;
+  }
+
+  public int getValue() {
+    return value;
+  }
+}

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/UF.java

@@ -0,0 +1,27 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
+
+public enum UF {
+  STRONG(0),
+  WEAK(2),
+  RANDOM(3);
+
+  private final int value;
+
+  UF(int i) {
+    value = i;
+  }
+
+  public int getValue() {
+    return value;
+  }
+}