Merge pull request #390 from sosy-lab/389-further-options-for-cvc5

#389: add ConfigurationOption to give CVC5 users the option to define solver specific  options directly.

Author: baierd

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java

@@ -11,6 +11,7 @@
 import com.google.common.base.Preconditions;
 import com.google.common.collect.Collections2;
 import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableMap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import io.github.cvc5.CVC5ApiException;
 import io.github.cvc5.Result;
@@ -22,6 +23,7 @@
 import java.util.Collection;
 import java.util.Deque;
 import java.util.List;
+import java.util.Map.Entry;
 import java.util.Optional;
 import java.util.Set;
 import org.sosy_lab.common.ShutdownNotifier;
@@ -54,7 +56,8 @@ protected CVC5AbstractProver(
       ShutdownNotifier pShutdownNotifier,
       @SuppressWarnings("unused") int randomSeed,
       Set<ProverOptions> pOptions,
-      FormulaManager pMgr) {
+      FormulaManager pMgr,
+      ImmutableMap<String, String> pFurtherOptionsMap) {
     super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
 
     mgr = pMgr;
@@ -63,10 +66,14 @@ protected CVC5AbstractProver(
     solver = new Solver();
     assertedTerms.add(PathCopyingPersistentTreeMap.of());
 
-    setSolverOptions(randomSeed, pOptions, solver);
+    setSolverOptions(randomSeed, pOptions, pFurtherOptionsMap, solver);
   }
 
-  protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Solver pSolver) {
+  protected void setSolverOptions(
+      int randomSeed,
+      Set<ProverOptions> pOptions,
+      ImmutableMap<String, String> pFurtherOptionsMap,
+      Solver pSolver) {
     if (incremental) {
       pSolver.setOption("incremental", "true");
     }
@@ -86,6 +93,10 @@ protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Sol
 
     // Enable more complete quantifier solving (for more info see CVC5QuantifiedFormulaManager)
     pSolver.setOption("full-saturate-quant", "true");
+
+    for (Entry<String, String> option : pFurtherOptionsMap.entrySet()) {
+      pSolver.setOption(option.getKey(), option.getValue());
+    }
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5InterpolatingProver.java

@@ -13,6 +13,7 @@
 import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;
 
 import com.google.common.collect.FluentIterable;
+import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Sets;
 import io.github.cvc5.CVC5ApiException;
@@ -35,6 +36,7 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver<String>
 
   private final FormulaManager mgr;
   private final Set<ProverOptions> solverOptions;
+  private final ImmutableMap<String, String> furtherOptionsMap;
   private final int seed;
   private final CVC5BooleanFormulaManager bmgr;
   private final boolean validateInterpolants;
@@ -45,22 +47,28 @@ public class CVC5InterpolatingProver extends CVC5AbstractProver<String>
       int randomSeed,
       Set<ProverOptions> pOptions,
       FormulaManager pMgr,
+      ImmutableMap<String, String> pFurtherOptionsMap,
       boolean pValidateInterpolants) {
-    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr);
+    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap);
     mgr = pMgr;
     solverOptions = pOptions;
     seed = randomSeed;
     bmgr = (CVC5BooleanFormulaManager) mgr.getBooleanFormulaManager();
     validateInterpolants = pValidateInterpolants;
+    furtherOptionsMap = pFurtherOptionsMap;
   }
 
   /**
    * Sets the same solver Options of the Original Solver to the separate solvertoSet, except for
    * produce-interpolants which is set here. From CVC5AbstractProver Line 66
    */
   @Override
-  protected void setSolverOptions(int randomSeed, Set<ProverOptions> pOptions, Solver pSolver) {
-    super.setSolverOptions(randomSeed, pOptions, pSolver);
+  protected void setSolverOptions(
+      int randomSeed,
+      Set<ProverOptions> pOptions,
+      ImmutableMap<String, String> pFurtherOptionsMap,
+      Solver pSolver) {
+    super.setSolverOptions(randomSeed, pOptions, pFurtherOptionsMap, pSolver);
     pSolver.setOption("produce-interpolants", "true");
   }
 
@@ -174,7 +182,7 @@ private Term getCVC5Interpolation(Collection<Term> formulasA, Collection<Term> f
 
     // Uses a separate Solver instance to leave the original solver-context unmodified
     Solver itpSolver = new Solver();
-    setSolverOptions(seed, solverOptions, itpSolver);
+    setSolverOptions(seed, solverOptions, furtherOptionsMap, itpSolver);
 
     Term interpolant;
     try {
@@ -216,7 +224,7 @@ private void checkInterpolationCriteria(Term interpolant, Term phiPlus, Term phi
     // build and check both Craig interpolation formulas with the generated interpolant.
     Solver validationSolver = new Solver();
     // interpolation option is not required for validation
-    super.setSolverOptions(seed, solverOptions, validationSolver);
+    super.setSolverOptions(seed, solverOptions, furtherOptionsMap, validationSolver);
     try {
       validationSolver.push();
       validationSolver.assertFormula(validationSolver.mkTerm(Kind.IMPLIES, phiPlus, interpolant));

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java

@@ -2,15 +2,20 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab.java_smt.solvers.cvc5;
 
 import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.Preconditions;
+import com.google.common.base.Splitter;
+import com.google.common.base.Splitter.MapSplitter;
+import com.google.common.collect.ImmutableMap;
+import io.github.cvc5.CVC5ApiRecoverableException;
 import io.github.cvc5.Solver;
+import java.util.Map.Entry;
 import java.util.Set;
 import java.util.function.Consumer;
 import org.sosy_lab.common.ShutdownNotifier;
@@ -38,8 +43,30 @@ private static class CVC5Settings {
         description = "apply additional validation checks for interpolation results")
     private boolean validateInterpolants = false;
 
+    @Option(
+        secure = true,
+        description =
+            "Further options that will be passed to CVC5 in addition to the default options. "
+                + "Format is 'key1=value1,key2=value2'")
+    private String furtherOptions = "";
+
+    private final ImmutableMap<String, String> furtherOptionsMap;
+
     private CVC5Settings(Configuration config) throws InvalidConfigurationException {
       config.inject(this);
+
+      MapSplitter optionSplitter =
+          Splitter.on(',')
+              .trimResults()
+              .omitEmptyStrings()
+              .withKeyValueSeparator(Splitter.on('=').limit(2).trimResults());
+
+      try {
+        furtherOptionsMap = ImmutableMap.copyOf(optionSplitter.split(furtherOptions));
+      } catch (IllegalArgumentException e) {
+        throw new InvalidConfigurationException(
+            "Invalid CVC5 option in \"" + furtherOptions + "\": " + e.getMessage(), e);
+      }
     }
   }
 
@@ -94,7 +121,11 @@ public static SolverContext create(
     // We keep this instance available until the whole context is closed.
     Solver newSolver = new Solver();
 
-    setSolverOptions(newSolver, randomSeed);
+    try {
+      setSolverOptions(newSolver, randomSeed, settings.furtherOptionsMap);
+    } catch (CVC5ApiRecoverableException e) { // we do not want to recover after invalid options.
+      throw new InvalidConfigurationException(e.getMessage(), e);
+    }
 
     CVC5FormulaCreator pCreator = new CVC5FormulaCreator(newSolver);
 
@@ -133,11 +164,21 @@ public static SolverContext create(
         pCreator, manager, pShutdownNotifier, newSolver, randomSeed, settings);
   }
 
-  /** Set common options for a CVC5 solver. */
-  private static void setSolverOptions(Solver pSolver, int randomSeed) {
+  /**
+   * Set common options for a CVC5 solver.
+   *
+   * @throws CVC5ApiRecoverableException from native code.
+   */
+  private static void setSolverOptions(
+      Solver pSolver, int randomSeed, ImmutableMap<String, String> furtherOptions)
+      throws CVC5ApiRecoverableException {
     pSolver.setOption("seed", String.valueOf(randomSeed));
     pSolver.setOption("output-language", "smtlib2");
 
+    for (Entry<String, String> option : furtherOptions.entrySet()) {
+      pSolver.setOption(option.getKey(), option.getValue());
+    }
+
     // Set Strings option to enable all String features (such as lessOrEquals).
     // This should not have any effect for non-string theories.
     // pSolver.setOption("strings-exp", "true");
@@ -182,7 +223,12 @@ public Solvers getSolverName() {
   public ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
     Preconditions.checkState(!closed, "solver context is already closed");
     return new CVC5TheoremProver(
-        creator, shutdownNotifier, randomSeed, pOptions, getFormulaManager());
+        creator,
+        shutdownNotifier,
+        randomSeed,
+        pOptions,
+        getFormulaManager(),
+        settings.furtherOptionsMap);
   }
 
   @Override
@@ -200,6 +246,7 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
         randomSeed,
         pOptions,
         getFormulaManager(),
+        settings.furtherOptionsMap,
         settings.validateInterpolants);
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5TheoremProver.java

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.solvers.cvc5;
 
+import com.google.common.collect.ImmutableMap;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.common.ShutdownNotifier;
@@ -25,8 +26,9 @@ protected CVC5TheoremProver(
       ShutdownNotifier pShutdownNotifier,
       @SuppressWarnings("unused") int randomSeed,
       Set<ProverOptions> pOptions,
-      FormulaManager pMgr) {
-    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr);
+      FormulaManager pMgr,
+      ImmutableMap<String, String> pFurtherOptionsMap) {
+    super(pFormulaCreator, pShutdownNotifier, randomSeed, pOptions, pMgr, pFurtherOptionsMap);
   }
 
   @Override

src/org/sosy_lab/java_smt/test/SolverContextTest.java

@@ -2,18 +2,25 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
 package org.sosy_lab.java_smt.test;
 
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.TruthJUnit.assume;
+import static org.junit.Assert.assertThrows;
 
 import org.junit.Test;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.java_smt.SolverContextFactory;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.FormulaManager;
+import org.sosy_lab.java_smt.api.ProverEnvironment;
+import org.sosy_lab.java_smt.api.SolverContext;
+import org.sosy_lab.java_smt.api.SolverException;
 
 public class SolverContextTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
@@ -120,4 +127,52 @@ public void testFormulaAccessAfterClose() {
     assertThat(bmgr.isTrue(opTerm)).isFalse();
     assertThat(bmgr.isFalse(opTerm)).isFalse();
   }
+
+  @Test
+  @SuppressWarnings("try")
+  public void testCVC5WithValidOptions() throws InvalidConfigurationException {
+    assume().that(solverToUse()).isEqualTo(Solvers.CVC5);
+
+    var config2 =
+        createTestConfigBuilder()
+            .setOption("solver.cvc5.furtherOptions", "solve-bv-as-int=bitwise")
+            .build();
+    var factory2 = new SolverContextFactory(config2, logger, shutdownNotifierToUse());
+    try (var context2 = factory2.generateContext()) {
+      // create and ignore
+    }
+  }
+
+  @Test(timeout = 1000)
+  @SuppressWarnings({"try", "CheckReturnValue"})
+  public void testCVC5WithValidOptionsTimeLimit()
+      throws InvalidConfigurationException, InterruptedException {
+    assume().that(solverToUse()).isEqualTo(Solvers.CVC5);
+
+    //  tlimit-per is time limit in ms of wall clock time per query
+    var configValid =
+        createTestConfigBuilder().setOption("solver.cvc5.furtherOptions", "tlimit-per=1").build();
+    var factoryWOption = new SolverContextFactory(configValid, logger, shutdownNotifierToUse());
+    try (SolverContext contextWTimeLimit = factoryWOption.generateContext()) {
+      FormulaManager fmgrTimeLimit = contextWTimeLimit.getFormulaManager();
+      HardIntegerFormulaGenerator hifg =
+          new HardIntegerFormulaGenerator(
+              fmgrTimeLimit.getIntegerFormulaManager(), fmgrTimeLimit.getBooleanFormulaManager());
+      BooleanFormula hardProblem = hifg.generate(100);
+      try (ProverEnvironment proverTimeLimited = contextWTimeLimit.newProverEnvironment()) {
+        proverTimeLimited.addConstraint(hardProblem);
+        assertThrows(SolverException.class, proverTimeLimited::isUnsat);
+      }
+    }
+  }
+
+  @Test
+  public void testCVC5WithInvalidOptions() throws InvalidConfigurationException {
+    assume().that(solverToUse()).isEqualTo(Solvers.CVC5);
+
+    var config2 =
+        createTestConfigBuilder().setOption("solver.cvc5.furtherOptions", "foo=bar").build();
+    var factory2 = new SolverContextFactory(config2, logger, shutdownNotifierToUse());
+    assertThrows(InvalidConfigurationException.class, factory2::generateContext);
+  }
 }