Merge pull request #502 from sosy-lab/490-opensmt2-evaluate-simplification-of-interpolants

490 opensmt2: improve options and add simplification option for interpolants

Author: kfriedberger

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

@@ -79,9 +79,14 @@ 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));
     }
     return config;
   }

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

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -13,6 +13,7 @@
 import java.util.function.Consumer;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.IntegerOption;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.common.configuration.Option;
 import org.sosy_lab.common.configuration.Options;
@@ -25,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;
@@ -45,13 +49,27 @@ 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;
+
+    /**
+     * This option controls the level of simplification applied to interpolants.
+     *
+     * <p>For details, please see the original sources:
+     * https://github.com/usi-verification-and-security/opensmt/blob/7cef5bc983d7774874ffc177f06516c4e0f411f4/src/proof/InterpolationContext.cc#L933-L960
+     */
+    @IntegerOption(min = 0, max = 4)
+    @Option(
+        secure = true,
+        description =
+            "Level of simplification for interpolants,"
+                + "ranging from 0 (no simplification) to 4 (maximum simplification).")
+    int simplifyInterpolants = 0;
 
     final int randomSeed;
 

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

@@ -0,0 +1,36 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
+
+/**
+ * Enumeration for the different algorithms for boolean interpolation.
+ *
+ * <p>For details, please see the original sources:
+ * https://github.com/usi-verification-and-security/opensmt/blob/c267e01e1e0d4d4b7f9ba273dd910c070c1aa9b1/src/options/SMTConfig.h#L163-L168
+ */
+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,35 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
+
+/**
+ * Enumeration for the different algorithms for LRA interpolation.
+ *
+ * <p>For details, please see the original sources:
+ * https://github.com/usi-verification-and-security/opensmt/blob/c267e01e1e0d4d4b7f9ba273dd910c070c1aa9b1/src/options/SMTConfig.h#L172C42-L176
+ */
+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,33 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;
+
+/**
+ * Enumeration for the different algorithms for UF interpolation.
+ *
+ * <p>For details, please see the original sources:
+ * https://github.com/usi-verification-and-security/opensmt/blob/c267e01e1e0d4d4b7f9ba273dd910c070c1aa9b1/src/options/SMTConfig.h#L169-L171
+ */
+public enum UF {
+  STRONG(0),
+  WEAK(2),
+  RANDOM(3);
+
+  private final int value;
+
+  UF(int i) {
+    value = i;
+  }
+
+  public int getValue() {
+    return value;
+  }
+}

src/org/sosy_lab/java_smt/solvers/opensmt/interpolationAlgorithms/package-info.java

@@ -0,0 +1,12 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2025 Dirk Beyer <https://www.sosy-lab.org>
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+/** Supported interpolation algorithms. */
+package org.sosy_lab.java_smt.solvers.opensmt.interpolationAlgorithms;