#389: add ConfigurationOption to give CVC5 some options directly.

Author: kfriedberger

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");

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

@@ -2,16 +2,19 @@
 // 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;
 
@@ -120,4 +123,29 @@ 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 config =
+        createTestConfigBuilder()
+            .setOption("solver.cvc5.furtherOptions", "solve-bv-as-int=bitwise")
+            .build();
+    var factory = new SolverContextFactory(config, logger, shutdownNotifierToUse());
+    try (var context = factory.generateContext()) {
+      // create and ignore
+    }
+  }
+
+  @Test
+  public void testCVC5WithInvalidOptions() throws InvalidConfigurationException {
+    assume().that(solverToUse()).isEqualTo(Solvers.CVC5);
+
+    var config =
+        createTestConfigBuilder().setOption("solver.cvc5.furtherOptions", "foo=bar").build();
+    var factory = new SolverContextFactory(config, logger, shutdownNotifierToUse());
+    assertThrows(InvalidConfigurationException.class, factory::generateContext);
+  }
 }