Add solver independent quantifier elimination with ultimate eliminator

.classpath

@@ -14,6 +14,15 @@ SPDX-License-Identifier: Apache-2.0
 	<classpathentry kind="src" path="src"/>
 	<classpathentry kind="lib" path="bin/"/>
 	<classpathentry kind="lib" path="lib/java/core/guava.jar" sourcepath="lib/java-contrib/guava-sources.jar"/>
+
+	<classpathentry kind="lib" path="lib/java/core/ultimate-model-checker-utils.jar" sourcepath="lib/java-contrib/ultimate-model-checker-utils-sources.jar"/>
+        <classpathentry kind="lib" path="lib/java/core/ultimate-core-rcp.jar" sourcepath="lib/java-contrib/ultimate-core-rcp-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/core/ultimate-core.jar" sourcepath="lib/java-contrib/ultimate-core-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/core/ultimate-model.jar" sourcepath="lib/java-contrib/ultimate-model-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/core/ultimate-library-smtlib.jar" sourcepath="lib/java-contrib/ultimate-library-smtlib-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/core/ultimate-library-smtlib-utils.jar" sourcepath="lib/java-contrib/ultimate-library-smtlib-utils-sources.jar"/>
+	<classpathentry kind="lib" path="lib/java/core/ultimate-util.jar" sourcepath="lib/java-contrib/ultimate-util-sources.jar"/>
+
 	<classpathentry kind="lib" path="lib/java/test/guava-testlib.jar" sourcepath="lib/java-contrib/guava-testlib-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/truth.jar" sourcepath="lib/java-contrib/truth-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/junit.jar"/>

lib/ivy.xml

@@ -167,6 +167,28 @@ SPDX-License-Identifier: Apache-2.0
         <!-- SmtInterpol -->
         <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources"/>
 
+        <!-- UltimateEliminator -->
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-model-checker-utils"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-core-rcp"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-core"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-model"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-library-smtlib"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-library-smtlib-utils"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="ultimate-util"
+                    rev="2022-10-13-r05bfb7ad3d" conf="core->runtime; contrib->sources"/>
+
+        <!-- Princess for our Maven release -->
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+        <!-- Princess for our Ivy release-->
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12"
+                    conf="runtime-princess->default; contrib->sources"/>
+          <!-- Exclude dependency on java-cup and replace it with java-cup-runtime, which is enough.-->
         <!-- Princess and Ostrich for our Maven release -->
         <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-11-08" conf="runtime-princess-with-javacup->default; contrib->sources"/>
         <dependency org="io.github.uuverifiers" name="ostrich_2.13" rev="1.4.1" conf="runtime-princess-with-javacup->default; contrib->sources"/>

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -292,17 +292,23 @@ private SolverContext generateContext0(Solvers solverToCreate)
 
       case PRINCESS:
         return PrincessSolverContext.create(
-            config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
+            config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic, logger);
 
       case YICES2:
-        return Yices2SolverContext.create(nonLinearArithmetic, shutdownNotifier, loader);
+        return Yices2SolverContext.create(nonLinearArithmetic, shutdownNotifier, loader, logger);
 
       case BOOLECTOR:
         return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader);
 
       case BITWUZLA:
         return BitwuzlaSolverContext.create(
-            config, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode, loader);
+            config,
+            shutdownNotifier,
+            logfile,
+            randomSeed,
+            floatingPointRoundingMode,
+            loader,
+            logger);
 
       default:
         throw new AssertionError("no solver selected");

src/org/sosy_lab/java_smt/api/QuantifiedFormulaManager.java

@@ -23,20 +23,70 @@ enum Quantifier {
     EXISTS
   }
 
+  enum QuantifierEliminationMethod {
+    /** Use the solver's built-in quantifier elimination method. */
+    NATIVE,
+
+    /** Use the solver's built-in quantifier elimination method. */
+    NATIVE_FALLBACK_ON_FAILURE,
+
+    /** Use the solver's built-in quantifier elimination method. */
+    NATIVE_FALLBACK_WITH_WARNING_ON_FAILURE,
+
+    /** Whether the solver should enable quantifier eliminiation via UltimateEliminator. */
+    ULTIMATE_ELIMINATOR,
+
+    /**
+     * Whether the solver should enable quantifier eliminiation via UltimateEliminator and fall back
+     * to the native quantifier elimination if UltimateEliminator's elimination method fails. The
+     * solver will not log a warning in this case.
+     */
+    ULTIMATE_ELIMINATOR_FALLBACK_ON_FAILURE,
+
+    /**
+     * Whether the solver should enable quantifier eliminiation via UltimateEliminator and back to
+     * the native quantifier elimination if UltimateEliminator's elimination method fails. The
+     * solver will log a warning in this case.
+     */
+    ULTIMATE_ELIMINATOR_FALLBACK_WITH_WARNING_ON_FAILURE,
+  }
+
+  enum QuantifierCreationMethod {
+    /**
+     * Whether the solver should eliminate the quantifier via UltimateEliminator before inserting it
+     * to the native quantified formula.
+     */
+    ULTIMATE_ELIMINATOR_BEFORE_FORMULA_CREATION,
+
+    /**
+     * Whether the solver should eliminate the quantifier via UltimateEliminator before inserting it
+     * to the native quantified formula and fall back to the native quantifier creation if
+     * UltimateEliminator fails. The solver will not log a warning in this case.
+     */
+    ULTIMATE_ELIMINATOR_BEFORE_FORMULA_CREATION_FALLBACK,
+
+    /**
+     * Whether the solver should eliminate the quantifier via UltimateEliminator before inserting it
+     * to the native quantified formula and fall back to the native quantifier creation if
+     * UltimateEliminator fails. The solver will log a warning in this case.
+     */
+    ULTIMATE_ELIMINATOR_BEFORE_FORMULA_CREATION_FALLBACK_WARN_ON_FAILURE
+  }
+
   /**
-   * @return An existentially quantified formula.
    * @param pVariables The variables that will get bound (variables) by the quantification.
    * @param pBody The {@link BooleanFormula}} within that the binding will be performed.
+   * @return An existentially quantified formula.
    * @throws IllegalArgumentException If the list {@code pVariables} is empty.
    */
   default BooleanFormula exists(List<? extends Formula> pVariables, BooleanFormula pBody) {
     return mkQuantifier(Quantifier.EXISTS, pVariables, pBody);
   }
 
   /**
-   * @return A universally quantified formula.
    * @param pVariables The variables that will get bound (variables) by the quantification.
    * @param pBody The {@link BooleanFormula}} within that the binding will be performed.
+   * @return A universally quantified formula.
    * @throws IllegalArgumentException If the list {@code pVariables} is empty.
    */
   default BooleanFormula forall(List<? extends Formula> pVariables, BooleanFormula pBody) {
@@ -54,15 +104,67 @@ default BooleanFormula exists(Formula quantifiedArg, BooleanFormula pBody) {
   }
 
   /**
-   * @return A quantified formula
+   * @param pVariables The variables that will get bound (variables) by the quantification.
+   * @param pBody The {@link BooleanFormula}} within that the binding will be performed.
+   * @param pMethod The {@link QuantifierCreationMethod}} to decide on the creation method.
+   * @return An existentially quantified formula.
+   * @throws IllegalArgumentException If the list {@code pVariables} is empty.
+   */
+  default BooleanFormula exists(
+      List<? extends Formula> pVariables, BooleanFormula pBody, QuantifierCreationMethod pMethod) {
+    return mkQuantifier(Quantifier.EXISTS, pVariables, pBody, pMethod);
+  }
+
+  /**
+   * @param pVariables The variables that will get bound (variables) by the quantification.
+   * @param pBody The {@link BooleanFormula}} within that the binding will be performed.
+   * @param pMethod The {@link QuantifierCreationMethod}} to decide on the creation method.
+   * @return A universally quantified formula.
+   * @throws IllegalArgumentException If the list {@code pVariables} is empty.
+   */
+  default BooleanFormula forall(
+      List<? extends Formula> pVariables, BooleanFormula pBody, QuantifierCreationMethod pMethod) {
+    return mkQuantifier(Quantifier.FORALL, pVariables, pBody, pMethod);
+  }
+
+  /** Syntax sugar, see {@link #forall(List, BooleanFormula)}. */
+  default BooleanFormula forall(
+      Formula quantifiedArg, BooleanFormula pBody, QuantifierCreationMethod pMethod) {
+    return forall(ImmutableList.of(quantifiedArg), pBody, pMethod);
+  }
+
+  /** Syntax sugar, see {@link #exists(List, BooleanFormula)}. */
+  default BooleanFormula exists(
+      Formula quantifiedArg, BooleanFormula pBody, QuantifierCreationMethod pMethod) {
+    return exists(ImmutableList.of(quantifiedArg), pBody, pMethod);
+  }
+
+  /**
    * @param q Quantifier type
    * @param pVariables The variables that will get bound (variables) by the quantification.
    * @param pBody The {@link BooleanFormula}} within that the binding will be performed.
+   * @return A quantified formula
    * @throws IllegalArgumentException If the list {@code pVariables} is empty.
    */
   BooleanFormula mkQuantifier(
       Quantifier q, List<? extends Formula> pVariables, BooleanFormula pBody);
 
+  /**
+   * Create a formula with a specific quantifier elimination method.
+   *
+   * @param q Quantifier type
+   * @param pVariables The variables that will get bound (variables) by the quantification.
+   * @param pBody The {@link BooleanFormula}} within that the binding will be performed.
+   * @param pMethod The {@link QuantifierCreationMethod}} to decide on the creation method.
+   * @return A boolean formula where the quantifier may already have been eliminated.
+   * @throws IllegalArgumentException If the list {@code pVariables} is empty.
+   */
+  BooleanFormula mkQuantifier(
+      Quantifier q,
+      List<? extends Formula> pVariables,
+      BooleanFormula pBody,
+      QuantifierCreationMethod pMethod);
+
   /**
    * Eliminate the quantifiers for a given formula. If this is not possible, it will return the
    * input formula. Note that CVC4 only supports this for LIA and LRA.
@@ -72,4 +174,17 @@ BooleanFormula mkQuantifier(
    */
   BooleanFormula eliminateQuantifiers(BooleanFormula pF)
       throws InterruptedException, SolverException;
+
+  /**
+   * Eliminate the quantifiers for a given formula using either UltimateEliminator or the native
+   * method. If this is not possible, depending on the given method it will fallback to the
+   * alternative method or throw an Exception. Note that CVC4 only supports this for LIA and LRA in
+   * the native elimination.
+   *
+   * @param pF Formula with quantifiers.
+   * @param pMethod enum value for method to be used for eliminating quantifiers.
+   * @return New formula without quantifiers.
+   */
+  BooleanFormula eliminateQuantifiers(BooleanFormula pF, QuantifierEliminationMethod pMethod)
+      throws InterruptedException, SolverException;
 }