Yices: Add an option to set the logic

src/org/sosy_lab/java_smt/solvers/yices2/Yices2AbstractProver.java

@@ -35,6 +35,7 @@
 import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
 import org.sosy_lab.java_smt.basicimpl.CachingModel;
 import org.sosy_lab.java_smt.basicimpl.ShutdownHook;
+import org.sosy_lab.java_smt.solvers.yices2.Yices2SolverContext.Yices2Parameters;
 
 /**
  * Info about the option {@link ProverOptions#GENERATE_UNSAT_CORE}: Yices provides the unsat core
@@ -70,10 +71,10 @@ abstract class Yices2AbstractProver<T> extends AbstractProverWithAllSat<T>
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr,
       ShutdownNotifier pShutdownNotifier,
-      String pSolverType) {
+      Yices2Parameters pSolverParameters) {
     super(pOptions, pBmgr, pShutdownNotifier);
     creator = pCreator;
-    curEnv = newContext(pSolverType);
+    curEnv = newContext(pSolverParameters);
     stack.push(PathCopyingPersistentTreeMap.of());
   }
 
@@ -86,11 +87,9 @@ protected boolean hasPersistentModel() {
     return true;
   }
 
-  Context newContext(String solverType) {
-    try (var cfg = new Config()) {
-      cfg.set("solver-type", solverType);
-      cfg.set("mode", "interactive");
-      cfg.set("model-interpolation", "true");
+  Context newContext(Yices2Parameters options) {
+    try (var cfg = new Config(options.logic)) {
+      cfg.set("mode", options.mode);
       return new Context(cfg);
     }
   }

src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java

@@ -17,6 +17,8 @@
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Sets;
 import com.google.common.primitives.Ints;
+import com.sri.yices.Config;
+import com.sri.yices.Context;
 import com.sri.yices.InterpolationContext;
 import com.sri.yices.Status;
 import com.sri.yices.Terms;
@@ -31,6 +33,7 @@
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.solvers.yices2.Yices2SolverContext.Yices2Parameters;
 
 class Yices2InterpolatingProver extends Yices2AbstractProver<Integer>
     implements InterpolatingProverEnvironment<Integer> {
@@ -39,8 +42,8 @@ class Yices2InterpolatingProver extends Yices2AbstractProver<Integer>
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr,
       ShutdownNotifier pShutdownNotifier,
-      String pSolverType) {
-    super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverType);
+      Yices2Parameters pSolverParameters) {
+    super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverParameters);
   }
 
   @Override
@@ -66,10 +69,18 @@ public BooleanFormula getInterpolant(Collection<Integer> formulasOfA)
             transformedImmutableSetCopy(setB, stack.peekLast()::get)));
   }
 
+  private Context newSolverStack() {
+    try (var cfg = new Config()) {
+      cfg.set("solver-type", "mcsat");
+      cfg.set("model-interpolation", "true");
+      return new Context(cfg);
+    }
+  }
+
   private int interpolate(Collection<Integer> setA, Collection<Integer> setB)
       throws InterruptedException {
-    try (var ctxA = newContext("mcsat");
-        var ctxB = newContext("mcsat")) {
+    try (var ctxA = newSolverStack();
+        var ctxB = newSolverStack()) {
 
       ctxA.assertFormulas(Ints.toArray(setA));
       ctxB.assertFormulas(Ints.toArray(setB));

src/org/sosy_lab/java_smt/solvers/yices2/Yices2Prover.java

@@ -17,15 +17,16 @@
 import org.sosy_lab.java_smt.api.BooleanFormulaManager;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.solvers.yices2.Yices2SolverContext.Yices2Parameters;
 
 class Yices2Prover extends Yices2AbstractProver<Void> implements ProverEnvironment {
   Yices2Prover(
       Yices2FormulaCreator creator,
       Set<ProverOptions> pOptions,
       BooleanFormulaManager pBmgr,
       ShutdownNotifier pShutdownNotifier,
-      String pSolverType) {
-    super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverType);
+      Yices2Parameters pSolverParameters) {
+    super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverParameters);
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/yices2/Yices2SolverContext.java

@@ -28,12 +28,61 @@
 public final class Yices2SolverContext extends AbstractSolverContext {
 
   @Options(prefix = "solver.yices2")
-  private static class Yices2Parameters {
+  static class Yices2Parameters {
     @Option(
         secure = true,
-        description = "Backend to use for the solver",
-        values = {"dpllt", "mcsat"})
-    String solverType = "mcsat";
+        description = "Sets the SMTLIB logic for solver selection",
+        values = {
+          "ALL",
+          "NONE",
+          "QF_ABV",
+          "QF_ALIA",
+          "QF_ALIRA",
+          "QF_ALRA",
+          "QF_ANIA",
+          "QF_ANIRA",
+          "QF_ANRA",
+          "QF_AUF",
+          "QF_AUFBV",
+          "QF_AUFBVLIA",
+          "QF_AUFBVNIA",
+          "QF_AUFLIA",
+          "QF_AUFLIRA",
+          "QF_AUFLRA",
+          "QF_AUFNIA",
+          "QF_AUFNIRA",
+          "QF_AUFNRA",
+          "QF_AX",
+          "QF_BV",
+          "QF_BVLRA",
+          "QF_FFA",
+          "QF_IDL",
+          "QF_LIA",
+          "QF_LIRA",
+          "QF_LRA",
+          "QF_NIA",
+          "QF_NIRA",
+          "QF_NRA",
+          "QF_RDL",
+          "QF_UF",
+          "QF_UFBV",
+          "QF_UFBVLIA",
+          "QF_UFIDL",
+          "QF_UFLIA",
+          "QF_UFLIRA",
+          "QF_UFLRA",
+          "QF_UFNIA",
+          "QF_UFNIRA",
+          "QF_UFNRA",
+          "QF_UFRDL"
+        })
+    String logic = "ALL";
+
+    @Option(
+        secure = true,
+        description = "Configures the solver to allow/disable multiple SAT checks",
+        values = {"one-shot", "multi-checks", "push-pop", "interactive"})
+    String mode = "push-pop";
 
     Yices2Parameters(Configuration config) throws InvalidConfigurationException {
       config.inject(this);
@@ -132,14 +181,13 @@ public synchronized void close() {
 
   @Override
   protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
-    return new Yices2Prover(creator, pOptions, bfmgr, shutdownManager, parameters.solverType);
+    return new Yices2Prover(creator, pOptions, bfmgr, shutdownManager, parameters);
   }
 
   @Override
   protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolation0(
       Set<ProverOptions> pOptions) {
-    return new Yices2InterpolatingProver(
-        creator, pOptions, bfmgr, shutdownManager, parameters.solverType);
+    return new Yices2InterpolatingProver(creator, pOptions, bfmgr, shutdownManager, parameters);
   }
 
   @Override

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

@@ -2701,10 +2701,6 @@ public void testArrayStore1BvBvBv() {
 
     assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); // Doesn't support multiple indices
     assume().that(solver).isNotEqualTo(Solvers.CVC4); // FIXME Broken in JavaSMT
-    assume()
-        .withMessage("Yices does not support constant arrays when mcsat is used")
-        .that(solver)
-        .isNotEqualTo(Solvers.YICES2);
 
     var scalarType = FormulaType.getBitvectorTypeWithSize(8);
 
@@ -2747,10 +2743,10 @@ public void testArrayStore2BvBvBv() {
 
     assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); // Doesn't support multiple indices
     assume()
-        .withMessage("Yices does not support constant arrays when mcsat is used")
+        .withMessage("Yices returns an empty array here")
         .that(solver)
-        .isNotEqualTo(Solvers.YICES2);
-    // FIXME CVC4 array model is sometimes broken in JavaSMT. Unfixable in CVC4, fixed in CVC5.
+        .isNotEqualTo(Solvers.YICES2); // FIXME
+    // CVC4 array model is sometimes broken in JavaSMT. Unfixable in CVC4, fixed in CVC5.
     assume().that(solver).isNotEqualTo(Solvers.CVC4);
 
     var scalarType = FormulaType.getBitvectorTypeWithSize(8);
@@ -2852,10 +2848,6 @@ public void testArrayStore1IntIntInt() {
     requireConstArrays();
 
     assume().that(solver).isNotEqualTo(Solvers.CVC4); // FIXME Broken in JavaSMT
-    assume()
-        .withMessage("Yices does not support constant arrays when mcsat is used")
-        .that(solver)
-        .isNotEqualTo(Solvers.YICES2);
 
     var scalarType = FormulaType.IntegerType;
 

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

@@ -38,7 +38,6 @@ public class NonLinearArithmeticTest<T extends NumeralFormula> extends SolverBas
 
   // Boolector, CVC4, SMTInterpol, MathSAT5 and OpenSMT do not fully support non-linear arithmetic
   // (though SMTInterpol and MathSAT5 support some parts)
-
   // INFO: OpenSmt does not suport nonlinear arithmetic
   static final ImmutableSet<Solvers> SOLVER_WITHOUT_NONLINEAR_ARITHMETIC =
       ImmutableSet.of(
@@ -87,8 +86,11 @@ public void chooseNumeralFormulaManager() {
 
   @Override
   protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException {
-    return super.createTestConfigBuilder()
-        .setOption("solver.nonLinearArithmetic", nonLinearArithmetic.name());
+    var newConfig = super.createTestConfigBuilder();
+    if (solver == Solvers.YICES2) {
+      newConfig.setOption("solver.yices2.logic", "QF_AUFNIRA");
+    }
+    return newConfig.setOption("solver.nonLinearArithmetic", nonLinearArithmetic.name());
   }
 
   private T handleExpectedException(Supplier<T> supplier) {

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

@@ -55,8 +55,11 @@ protected Solvers solverToUse() {
 
   @Override
   protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException {
-    return super.createTestConfigBuilder()
-        .setOption("solver.nonLinearArithmetic", nonLinearArithmetic.name());
+    var newConfig = super.createTestConfigBuilder();
+    if (solver == Solvers.YICES2) {
+      newConfig.setOption("solver.yices2.logic", "QF_AUFNIRA");
+    }
+    return newConfig.setOption("solver.nonLinearArithmetic", nonLinearArithmetic.name());
   }
 
   private IntegerFormula handleExpectedException(Supplier<IntegerFormula> supplier) {

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

@@ -16,6 +16,8 @@
 import java.util.ArrayList;
 import java.util.List;
 import org.junit.Test;
+import org.sosy_lab.common.configuration.ConfigurationBuilder;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
@@ -29,6 +31,16 @@
 
 public class NumeralFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
+  @Override
+  protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException {
+    var newConfig = super.createTestConfigBuilder();
+    if (solver == Solvers.YICES2) {
+      // We need MCSAT for division by zero
+      newConfig.setOption("solver.yices2.logic", "QF_AUFNIRA");
+    }
+    return newConfig;
+  }
+
   @Test
   public void divZeroTest() throws SolverException, InterruptedException {
     requireIntegers();

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

@@ -22,6 +22,8 @@
 import org.junit.AssumptionViolatedException;
 import org.junit.Ignore;
 import org.junit.Test;
+import org.sosy_lab.common.configuration.ConfigurationBuilder;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -37,6 +39,14 @@
 
 @SuppressWarnings("LocalVariableName")
 public class SolverTheoriesTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
+  @Override
+  protected ConfigurationBuilder createTestConfigBuilder() throws InvalidConfigurationException {
+    var newConfig = super.createTestConfigBuilder();
+    if (solver == Solvers.YICES2) {
+      newConfig.setOption("solver.yices2.logic", "QF_AUFNIRA");
+    }
+    return newConfig;
+  }
 
   @Test
   public void basicBoolTest() throws SolverException, InterruptedException {