Add MathSAT5 logic selection via option

lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c

@@ -89,6 +89,21 @@ DEFINE_FUNC(jconf, 1create_1config) WITHOUT_ARGS
 CALL0(msat_config, create_config)
 CONF_RETURN
 
+/*
+ * msat_config msat_create_default_config(const char * 	logic)
+ * Creates a new MathSAT configuration with the default settings for the given logic.
+ * Parameters:
+ *  logic	An SMT-LIB logic name
+ * Returns:
+ *  A new configuration. In case of errors, a cfg s.t. MSAT_ERROR_CONFIG(cfg) is true is returned. 
+ *  CONF_RETURN checks this and throws for errors.
+ */
+DEFINE_FUNC(jconf, 1create_1default_1config) WITH_ONE_ARG(string)
+STRING_ARG(1)
+CALL1(msat_config, create_default_config)
+FREE_STRING_ARG(1)
+CONF_RETURN
+
 /*
  * void msat_destroy_config(msat_config cfg);
  */

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java

@@ -8,11 +8,13 @@
 
 package org.sosy_lab.java_smt.solvers.mathsat5;
 
+import static com.google.common.base.Preconditions.checkNotNull;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaManager.getMsatTerm;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_all_sat;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat_with_assumptions;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_config;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_default_config;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_config;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_env;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_free_termination_callback;
@@ -62,17 +64,18 @@ abstract class Mathsat5AbstractProver<T2> extends AbstractProver<T2> {
   protected Mathsat5AbstractProver(
       Mathsat5SolverContext pContext,
       Set<ProverOptions> pOptions,
+      String pLogic,
       Mathsat5FormulaCreator pCreator,
       ShutdownNotifier pShutdownNotifier) {
     super(pOptions);
     context = pContext;
     creator = pCreator;
-    curConfig = buildConfig(pOptions);
+    curConfig = buildConfig(pOptions, checkNotNull(pLogic));
     curEnv = context.createEnvironment(curConfig);
     shutdownNotifier = pShutdownNotifier;
   }
 
-  private long buildConfig(Set<ProverOptions> opts) {
+  private long buildConfig(Set<ProverOptions> opts, String pLogic) {
     Map<String, String> config = new LinkedHashMap<>();
     boolean generateUnsatCore = opts.contains(ProverOptions.GENERATE_UNSAT_CORE);
     config.put("model_generation", opts.contains(ProverOptions.GENERATE_MODELS) ? "true" : "false");
@@ -82,7 +85,13 @@ private long buildConfig(Set<ProverOptions> opts) {
     }
     createConfig(config); // ask subclasses for their options
 
-    long cfg = msat_create_config();
+    long cfg;
+    if (pLogic.isEmpty() || pLogic.equalsIgnoreCase("ALL")) {
+      cfg = msat_create_config();
+    } else {
+      // TODO: input validation for logics in MathSAT5
+      cfg = msat_create_default_config(pLogic);
+    }
     for (Map.Entry<String, String> entry : config.entrySet()) {
       msat_set_option_checked(cfg, entry.getKey(), entry.getValue());
     }
@@ -196,7 +205,7 @@ public List<BooleanFormula> getUnsatCore() {
   @Override
   public Optional<List<BooleanFormula>> unsatCoreOverAssumptions(
       Collection<BooleanFormula> assumptions) throws SolverException, InterruptedException {
-    Preconditions.checkNotNull(assumptions);
+    checkNotNull(assumptions);
     checkGenerateUnsatCoresOverAssumptions();
 
     closeAllEvaluators();

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java

@@ -56,8 +56,9 @@ class Mathsat5InterpolatingProver extends Mathsat5AbstractProver<Integer>
       Mathsat5SolverContext pMgr,
       ShutdownNotifier pShutdownNotifier,
       Mathsat5FormulaCreator creator,
-      Set<ProverOptions> options) {
-    super(pMgr, options, creator, pShutdownNotifier);
+      Set<ProverOptions> options,
+      String pLogic) {
+    super(pMgr, options, pLogic, creator, pShutdownNotifier);
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java

@@ -205,11 +205,22 @@ public static long msat_get_interpolant(long e, int[] groups_of_a) {
     return msat_get_interpolant(e, groups_of_a, groups_of_a.length);
   }
 
-  /*
-   * Environment creation
+  /**
+   * Creates a new MathSAT configuration. If you want to set the logic, please use {@link
+   * #msat_create_default_config(String)} instead. Original: msat_config msat_create_config()
    */
   public static native long msat_create_config();
 
+  /**
+   * Creates a new MathSAT configuration with the default settings for the given logic. Original:
+   * msat_config msat_create_default_config(const char * logic)
+   *
+   * @param logic An SMT-LIB logic name
+   * @return A new configuration.
+   * @throws IllegalArgumentException In case of errors.
+   */
+  public static native long msat_create_default_config(final String logic);
+
   public static native void msat_destroy_config(long cfg);
 
   public static native long msat_create_env(long cfg);

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java

@@ -2,7 +2,7 @@
 // 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: 2026 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -12,10 +12,12 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_config;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_default_config;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_env;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_arity;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_name;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_config;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_env;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_model_iterator;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_proof_manager;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_from_smtlib2;
@@ -59,6 +61,8 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_equals;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr;
 
+import com.google.common.collect.ImmutableSet;
+import java.util.Set;
 import org.junit.AssumptionViolatedException;
 import org.junit.Before;
 import org.junit.BeforeClass;
@@ -69,6 +73,25 @@
 
 public class Mathsat5NativeApiTest extends Mathsat5AbstractNativeApiTest {
 
+  // Some logics and other strings to test how mathsat reacts to them
+  private static final Set<String> LOGICS_TO_TEST =
+      ImmutableSet.of(
+          "unfug",
+          "",
+          "ALL",
+          "QF_LIA",
+          "QF_LRA",
+          "QF_LIRA",
+          "LIRA",
+          "QF_UFLIA",
+          "QF_UFLRA",
+          "QF_UFLIRA",
+          "QF_ALIA",
+          "QF_ALRA",
+          "QF_ALIRA",
+          "UF_AUFLIRA",
+          "AUFLIRA");
+
   private long const0;
   private long const1;
   private long var;
@@ -98,6 +121,36 @@ public void createEnvironment() {
     var = msat_make_variable(env, "rat", rationalType);
   }
 
+  // MathSAT5 seems to ignore invalid input for logics
+  @Test
+  public void createEnvironmentWithLogics() throws SolverException, InterruptedException {
+    for (String logic : LOGICS_TO_TEST) {
+      // Logics just set certain default settings in MathSAT5
+      long cfgWithLogic = msat_create_default_config(logic);
+      // Set some option just to check whether there are problems
+      msat_set_option_checked(cfgWithLogic, "model_generation", "true");
+
+      long envWithLogic = msat_create_env(cfgWithLogic);
+      msat_destroy_config(cfgWithLogic);
+
+      long const0WithLogic = msat_make_number(envWithLogic, "0");
+      long const1WithLogic = msat_make_number(envWithLogic, "1");
+      long rationalType = msat_get_rational_type(envWithLogic);
+      long varWithLogic = msat_make_variable(envWithLogic, "rat", rationalType);
+
+      long sin = msat_make_sin(envWithLogic, varWithLogic);
+
+      msat_push_backtrack_point(envWithLogic);
+
+      msat_assert_formula(
+          envWithLogic, msat_make_equal(envWithLogic, varWithLogic, const1WithLogic));
+      msat_assert_formula(envWithLogic, msat_make_equal(envWithLogic, sin, const0WithLogic));
+
+      assertThat(msat_check_sat(envWithLogic)).isFalse();
+      msat_destroy_env(envWithLogic);
+    }
+  }
+
   @Test
   public void proofTest() throws IllegalStateException, InterruptedException, SolverException {
     long cfg = msat_create_config();

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5OptimizationProver.java

@@ -59,8 +59,9 @@ class Mathsat5OptimizationProver extends Mathsat5AbstractProver<Void>
       Mathsat5SolverContext pMgr,
       ShutdownNotifier pShutdownNotifier,
       Mathsat5FormulaCreator creator,
-      Set<ProverOptions> options) {
-    super(pMgr, options, creator, pShutdownNotifier);
+      Set<ProverOptions> options,
+      String pLogic) {
+    super(pMgr, options, pLogic, creator, pShutdownNotifier);
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java

@@ -83,6 +83,13 @@ private static final class Mathsat5Settings {
     @Option(secure = true, description = "Load less stable optimizing version of mathsat5 solver.")
     boolean loadOptimathsat5 = false;
 
+    @Option(
+        secure = true,
+        description =
+            "SMT-LIB logic to configure the SMT solvers (i.e. all Provers created from a"
+                + " SolverContext with this option) with. Default: ALL")
+    private String logic = "ALL";
+
     private final @Nullable PathCounterTemplate logfile;
 
     private final ImmutableMap<String, String> furtherOptionsMap;
@@ -287,21 +294,22 @@ long createEnvironment(long cfg) {
   @Override
   protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options);
+    return new Mathsat5TheoremProver(this, shutdownNotifier, creator, options, settings.logic);
   }
 
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
       Set<ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return new Mathsat5InterpolatingProver(this, shutdownNotifier, creator, options);
+    return new Mathsat5InterpolatingProver(
+        this, shutdownNotifier, creator, options, settings.logic);
   }
 
   @Override
   public OptimizationProverEnvironment newOptimizationProverEnvironment0(
       Set<ProverOptions> options) {
     Preconditions.checkState(!closed, "solver context is already closed");
-    return new Mathsat5OptimizationProver(this, shutdownNotifier, creator, options);
+    return new Mathsat5OptimizationProver(this, shutdownNotifier, creator, options, settings.logic);
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java

@@ -26,8 +26,9 @@ class Mathsat5TheoremProver extends Mathsat5AbstractProver<Void> implements Prov
       Mathsat5SolverContext pMgr,
       ShutdownNotifier pShutdownNotifier,
       Mathsat5FormulaCreator creator,
-      Set<ProverOptions> options) {
-    super(pMgr, options, creator, pShutdownNotifier);
+      Set<ProverOptions> options,
+      String pLogic) {
+    super(pMgr, options, pLogic, creator, pShutdownNotifier);
   }
 
   @Override