Update Yices to version 2.7.0

build/build-publish-solvers/solver-yices.xml

@@ -39,7 +39,7 @@ SPDX-License-Identifier: Apache-2.0
             <copy file="lib/native/source/yices2j/libyices2j.so" tofile="libyices2j-${yices2.version}.so"/>
 
             <ivy:resolve conf="solver-yices2" file="solvers_ivy_conf/ivy_yices2.xml" />
-            <publishToRepository solverName="Yices" solverVersion="${version}"/>
+            <publishToRepository solverName="Yices" solverVersion="${yices2.version}"/>
         </sequential>
     </target>
 

lib/ivy.xml

@@ -198,7 +198,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.8.1-gc1454189" conf="runtime-bitwuzla-x64->solver-bitwuzla-x64; runtime-bitwuzla-arm64->solver-bitwuzla-arm64; contrib->sources,javadoc"/>
 
         <!-- additional JavaSMT components with Solver Binaries -->
-        <dependency org="org.sosy_lab" name="javasmt-yices2" rev="4.1.1-734-g3732f7e08" conf="runtime-yices2->runtime; contrib->sources" />
+        <dependency org="org.sosy_lab" name="javasmt-yices2" rev="5.0.1-682-g0dbe8366f" conf="runtime-yices2->runtime; contrib->sources"/>
         <!-- <dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.6.4-264-g553897f5" conf="runtime->solver-yices2" /> -->
 
         <!-- Several JARs declare animal-sniffer-annotations.jar as dependency in their manifest, although they do not really need it.

lib/native/source/yices2j/compile.sh

@@ -34,12 +34,11 @@ cd ${DIR}
 
 JNI_HEADERS="$(../get_jni_headers.sh)"
 
-RELATIVE_ROOT_DIR="../../../.."
-YICES_SRC_DIR=$RELATIVE_ROOT_DIR/"$1"/src/include
-YICES_LIB_DIR=$RELATIVE_ROOT_DIR/"$1"/build/x86_64-pc-linux-gnu-release/lib/
-GMP_HEADER_DIR=$RELATIVE_ROOT_DIR/"$2"
+YICES_SRC_DIR="$1"/src/include
+YICES_LIB_DIR="$1"/build/x86_64-pc-linux-gnu-release/lib/
+GMP_HEADER_DIR="$2"
 GMP_LIB_DIR=$GMP_HEADER_DIR/.libs
-GPERF_HEADER_DIR=$RELATIVE_ROOT_DIR/"$3"
+GPERF_HEADER_DIR="$3"
 GPERF_LIB_DIR=$GPERF_HEADER_DIR/lib
 
 # check requirements

lib/native/source/yices2j/includes/defines.h

@@ -149,7 +149,7 @@ typedef void jvoid; // for symmetry to jint, jlong etc.
   if(arg##id < 0) { \
     throwException(jenv, "java/lang/IllegalArgumentException", "An yval_id cannot be negative."); \
   }\
-  if(arg##tag < 0 || arg##tag > 8) { \
+  if(arg##tag < 0 || arg##tag > 9) { \
     throwException(jenv, "java/lang/IllegalArgumentException", "Yval_tag is negative or not a valid yval_tag."); \
   } \
   m_arg##num->node_id = arg##id; \

lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c

@@ -1598,6 +1598,13 @@ DEFINE_FUNC(int, 1is_1thread_1safe) WITHOUT_ARGS
 CALL0(int, is_thread_safe)
 INT_RETURN
 
+/*
+ * Check if yices was compiled with MCSAT support
+ */
+DEFINE_FUNC(int, 1has_1mcsat) WITHOUT_ARGS
+CALL0(int, has_mcsat)
+INT_RETURN
+
 /*
  * The function first checks whether f is satisifiable or unsatisfiable.
  *

solvers_ivy_conf/ivy_javasmt_yices2.xml

@@ -33,19 +33,19 @@ SPDX-License-Identifier: Apache-2.0
     </publications>
 
     <dependencies>
-        <dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.6.4-264-g553897f5" conf="runtime->solver-yices2" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-yices2" rev="2.7.0-mcsat" conf="runtime->solver-yices2"/>
 
         <!-- keep the following dependencies synchronized with the default lib/ivy.xml and build-jar-yices2.xml -->
 
         <!-- SoSy-Lab Common Library -->
-        <dependency org="org.sosy_lab" name="common" rev="0.3000-585-g7a5f95c1" conf="runtime->runtime; sources->sources"/>
+        <dependency org="org.sosy_lab" name="common" rev="0.3000-609-g90a352c" conf="runtime->runtime; sources->sources"/>
 
         <!-- Google Core Libraries for Java
              Contains a lot of helpful data structures. -->
-        <dependency org="com.google.guava" name="guava" rev="33.2.1-jre" conf="runtime->default; sources->sources"/>
+        <dependency org="com.google.guava" name="guava" rev="33.4.0-jre" conf="runtime->default; sources->sources"/>
 
         <!-- Annotations we use for @Nullable etc. -->
-        <dependency org="org.checkerframework" name="checker-qual" rev="3.44.0" conf="runtime->default; sources->sources"/>
+        <dependency org="org.checkerframework" name="checker-qual" rev="3.48.4" conf="runtime->default; sources->sources"/>
 
     </dependencies>
 

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

@@ -13,6 +13,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_AND;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_APP_TERM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_CONST;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_FF_CONSTANT;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_GE_ATOM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_SUM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BIT_TERM;
@@ -160,6 +161,7 @@ public class Yices2FormulaCreator extends FormulaCreator<Integer, Integer, Long,
       ImmutableSet.of(
           YICES_BOOL_CONST,
           YICES_ARITH_CONST,
+          YICES_ARITH_FF_CONSTANT,
           YICES_BV_CONST,
           YICES_VARIABLE,
           YICES_UNINTERPRETED_TERM);
@@ -400,7 +402,7 @@ private <R> R visitFunctionApplication(
       case YICES_APP_TERM:
         functionKind = FunctionDeclarationKind.UF;
         functionArgs = getArgs(pF);
-        functionName = yices_term_to_string(functionArgs.get(0));
+        functionName = yices_get_term_name(functionArgs.get(0));
         functionDeclaration = functionArgs.get(0);
         functionArgs.remove(0);
         break;

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

@@ -16,6 +16,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_SCALAR;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_TUPLE;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_UNKNOWN;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.tagForValKind;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_application;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvtype_size;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_def_terms;
@@ -112,7 +113,8 @@ private ImmutableList<ValueAssignment> getFunctionAssignment(int t, int[] yval)
     for (int i = 2; i < expandFun.length - 1; i += 2) {
       int[] expandMap;
       if (expandFun[i + 1] == YVAL_MAPPING) {
-        expandMap = yices_val_expand_mapping(model, expandFun[i], arity, expandFun[i + 1]);
+        expandMap =
+            yices_val_expand_mapping(model, expandFun[i], arity, tagForValKind(expandFun[i + 1]));
       } else {
         throw new IllegalArgumentException("Unexpected YVAL tag " + yval[1]);
       }

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

@@ -10,6 +10,7 @@
 
 import java.util.function.Supplier;
 import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.ShutdownHook;
 
 @SuppressWarnings({"unused", "checkstyle:methodname", "checkstyle:parametername"})
@@ -29,61 +30,62 @@ private Yices2NativeApi() {}
   public static final int YICES_CONSTRUCTOR_ERROR = -1;
   public static final int YICES_BOOL_CONST = 0;
   public static final int YICES_ARITH_CONST = 1;
-  public static final int YICES_BV_CONST = 2;
-  public static final int YICES_SCALAR_CONST = 3; // NOT used in JavaSMT
-  public static final int YICES_VARIABLE = 4;
-  public static final int YICES_UNINTERPRETED_TERM = 5;
-
-  public static final int YICES_ITE_TERM = 6; // if-then-else
-  public static final int YICES_APP_TERM = 7; // application of an uninterpreted function
-  public static final int YICES_UPDATE_TERM = 8; // function update
-  public static final int YICES_TUPLE_TERM = 9; // tuple constructor
-  public static final int YICES_EQ_TERM = 10; // equality
-  public static final int YICES_DISTINCT_TERM = 11; // distinct t_1 ... t_n
-  public static final int YICES_FORALL_TERM = 12; // quantifier
-  public static final int YICES_LAMBDA_TERM = 13; // lambda
-  public static final int YICES_NOT_TERM = 14; // (not t)
-  public static final int YICES_OR_TERM = 15; // n-ary OR
-  public static final int YICES_XOR_TERM = 16; // n-ary XOR
-
-  public static final int YICES_BV_ARRAY = 17; // array of boolean terms
-  public static final int YICES_BV_DIV = 18; // unsigned division
-  public static final int YICES_BV_REM = 19; // unsigned remainder
-  public static final int YICES_BV_SDIV = 20; // signed division
-  public static final int YICES_BV_SREM = 21; // remainder in signed division (rounding to 0)
-  public static final int YICES_BV_SMOD = 22; // remainder in signed division (rounding to
+  public static final int YICES_ARITH_FF_CONSTANT = 2; // finite field rational constant
+  public static final int YICES_BV_CONST = 3;
+  public static final int YICES_SCALAR_CONST = 4; // NOT used in JavaSMT
+  public static final int YICES_VARIABLE = 5;
+  public static final int YICES_UNINTERPRETED_TERM = 6;
+
+  public static final int YICES_ITE_TERM = 7; // if-then-else
+  public static final int YICES_APP_TERM = 8; // application of an uninterpreted function
+  public static final int YICES_UPDATE_TERM = 9; // function update
+  public static final int YICES_TUPLE_TERM = 10; // tuple constructor
+  public static final int YICES_EQ_TERM = 11; // equality
+  public static final int YICES_DISTINCT_TERM = 12; // distinct t_1 ... t_n
+  public static final int YICES_FORALL_TERM = 13; // quantifier
+  public static final int YICES_LAMBDA_TERM = 14; // lambda
+  public static final int YICES_NOT_TERM = 15; // (not t)
+  public static final int YICES_OR_TERM = 16; // n-ary OR
+  public static final int YICES_XOR_TERM = 17; // n-ary XOR
+
+  public static final int YICES_BV_ARRAY = 18; // array of boolean terms
+  public static final int YICES_BV_DIV = 19; // unsigned division
+  public static final int YICES_BV_REM = 20; // unsigned remainder
+  public static final int YICES_BV_SDIV = 21; // signed division
+  public static final int YICES_BV_SREM = 22; // remainder in signed division (rounding to 0)
+  public static final int YICES_BV_SMOD = 23; // remainder in signed division (rounding to
   // -infinity)
-  public static final int YICES_BV_SHL = 23; // shift left (padding with 0)
-  public static final int YICES_BV_LSHR = 24; // logical shift right (padding with 0)
-  public static final int YICES_BV_ASHR = 25; // arithmetic shift right (padding with sign bit)
-  public static final int YICES_BV_GE_ATOM = 26; // unsigned comparison: (t1 >= t2)
-  public static final int YICES_BV_SGE_ATOM = 27; // signed comparison (t1 >= t2)
-  public static final int YICES_ARITH_GE_ATOM = 28; // atom (t1 >= t2) for arithmetic terms: t2 is
+  public static final int YICES_BV_SHL = 24; // shift left (padding with 0)
+  public static final int YICES_BV_LSHR = 25; // logical shift right (padding with 0)
+  public static final int YICES_BV_ASHR = 26; // arithmetic shift right (padding with sign bit)
+  public static final int YICES_BV_GE_ATOM = 27; // unsigned comparison: (t1 >= t2)
+  public static final int YICES_BV_SGE_ATOM = 28; // signed comparison (t1 >= t2)
+  public static final int YICES_ARITH_GE_ATOM = 29; // atom (t1 >= t2) for arithmetic terms: t2 is
   // always 0
-  public static final int YICES_ARITH_ROOT_ATOM = 29; // atom (0 <= k <= root_count(p)) && (x r
+  public static final int YICES_ARITH_ROOT_ATOM = 30; // atom (0 <= k <= root_count(p)) && (x r
   // root(p,k)) for r in <, <=, ==, !=, >, >=
 
-  public static final int YICES_ABS = 30; // absolute value
-  public static final int YICES_CEIL = 31; // ceil
-  public static final int YICES_FLOOR = 32; // floor
-  public static final int YICES_RDIV = 33; // real division (as in x/y)
-  public static final int YICES_IDIV = 34; // integer division
-  public static final int YICES_IMOD = 35; // modulo
-  public static final int YICES_IS_INT_ATOM = 36; // integrality test: (is-int t)
-  public static final int YICES_DIVIDES_ATOM = 37; // divisibility test: (divides t1 t2)
+  public static final int YICES_ABS = 31; // absolute value
+  public static final int YICES_CEIL = 32; // ceil
+  public static final int YICES_FLOOR = 33; // floor
+  public static final int YICES_RDIV = 34; // real division (as in x/y)
+  public static final int YICES_IDIV = 35; // integer division
+  public static final int YICES_IMOD = 36; // modulo
+  public static final int YICES_IS_INT_ATOM = 37; // integrality test: (is-int t)
+  public static final int YICES_DIVIDES_ATOM = 38; // divisibility test: (divides t1 t2)
 
   // projections
-  public static final int YICES_SELECT_TERM = 38; // tuple projection
-  public static final int YICES_BIT_TERM = 39; // bit-select: extract the i-th bit of a bitvector
+  public static final int YICES_SELECT_TERM = 39; // tuple projection
+  public static final int YICES_BIT_TERM = 40; // bit-select: extract the i-th bit of a bitvector
 
   // sums
-  public static final int YICES_BV_SUM = 40; // sum of pairs a * t where a is a bitvector constant
+  public static final int YICES_BV_SUM = 41; // sum of pairs a * t where a is a bitvector constant
   // (and t is a bitvector term)
-  public static final int YICES_ARITH_SUM = 41; // sum of pairs a * t where a is a rational (and t
+  public static final int YICES_ARITH_SUM = 42; // sum of pairs a * t where a is a rational (and t
   // is an arithmetic term)
-
-  // products
-  public static final int YICES_POWER_PRODUCT = 42; // power products: (t1^d1 * ... * t_n^d_n)
+  public static final int YICES_ARITH_FF_SUM = 43; // sum of pairs a * t where a is an finite
+  // field constant (and t is an finite field arithmetic term) products
+  public static final int YICES_POWER_PRODUCT = 44; // power products: (t1^d1 * ... * t_n^d_n)
 
   // Workaround as Yices misses some useful operators,
   // MAX_INT avoids collisions with existing constants
@@ -97,11 +99,41 @@ private Yices2NativeApi() {}
   public static final int YVAL_BOOL = 1;
   public static final int YVAL_RATIONAL = 2;
   public static final int YVAL_ALGEBRAIC = 3;
-  public static final int YVAL_BV = 4;
-  public static final int YVAL_SCALAR = 5;
-  public static final int YVAL_TUPLE = 6;
-  public static final int YVAL_FUNCTION = 7;
-  public static final int YVAL_MAPPING = 8;
+  public static final int YVAL_FINITEFIELD = 4;
+  public static final int YVAL_BV = 5;
+  public static final int YVAL_SCALAR = 6;
+  public static final int YVAL_TUPLE = 7;
+  public static final int YVAL_FUNCTION = 8;
+  public static final int YVAL_MAPPING = 9;
+
+  public static int tagForValKind(int valKind) {
+    switch (valKind) {
+      case 0:
+        return YVAL_UNKNOWN; // UNKNOWN_VALUE
+      case 1:
+        return YVAL_BOOL; // BOOLEAN_VALUE
+      case 2:
+        return YVAL_RATIONAL; // RATIONAL_VALUE
+      case 3:
+        return YVAL_FINITEFIELD; // FINITEFIELD_VALUE
+      case 4:
+        return YVAL_ALGEBRAIC; // ALGEBRAIC_VALUE
+      case 5:
+        return YVAL_BV; // BITVECTOR_VALUE
+      case 6:
+        return YVAL_TUPLE; // TUPPLE_VALUE
+      case 7:
+        return YVAL_SCALAR; // UNINTERPRETED_VALUE
+      case 8:
+        return YVAL_FUNCTION; // FUNCTION_VALUE
+      case 9:
+        return YVAL_MAPPING; // MAP_VALUE
+      case 10:
+        return YVAL_FUNCTION; // UPDATE_VALUE
+      default:
+        throw new IllegalArgumentException("Unknown valKind: " + valKind);
+    }
+  }
 
   /*
    * Yices initialization and exit
@@ -657,7 +689,7 @@ public static native int yices_check_context_with_assumptions(
    * @param params Set to 0 for default search parameters.
    */
   public static boolean yices_check_sat(long ctx, long params, ShutdownNotifier shutdownNotifier)
-      throws IllegalStateException, InterruptedException {
+      throws IllegalStateException, InterruptedException, SolverException {
     return satCheckWithShutdownNotifier(
         () -> yices_check_context(ctx, params), ctx, shutdownNotifier);
   }
@@ -667,7 +699,7 @@ public static boolean yices_check_sat(long ctx, long params, ShutdownNotifier sh
    */
   public static boolean yices_check_sat_with_assumptions(
       long ctx, long params, int size, int[] assumptions, ShutdownNotifier shutdownNotifier)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     return satCheckWithShutdownNotifier(
         () -> yices_check_context_with_assumptions(ctx, params, size, assumptions),
         ctx,
@@ -677,7 +709,7 @@ public static boolean yices_check_sat_with_assumptions(
   @SuppressWarnings("try")
   private static boolean satCheckWithShutdownNotifier(
       Supplier<Integer> satCheck, long pCtx, ShutdownNotifier shutdownNotifier)
-      throws InterruptedException {
+      throws InterruptedException, SolverException {
     int result;
     try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, () -> yices_stop_search(pCtx))) {
       shutdownNotifier.shutdownIfNecessary();
@@ -687,16 +719,18 @@ private static boolean satCheckWithShutdownNotifier(
     return check_result(result);
   }
 
-  private static boolean check_result(int result) {
+  private static boolean check_result(int result) throws InterruptedException, SolverException {
     switch (result) {
       case YICES_STATUS_SAT:
         return true;
       case YICES_STATUS_UNSAT:
         return false;
+      case YICES_STATUS_INTERRUPTED:
+        throw new InterruptedException();
+      case YICES_STATUS_ERROR:
+        throw new SolverException("SAT check returned \"unknown\"");
       default:
-        // TODO Further ERROR CLARIFICATION
-        String code = (result == YICES_STATUS_UNKNOWN) ? "\"unknown\"" : result + "";
-        throw new IllegalStateException("Yices check returned:" + code);
+        throw new SolverException("Internal solver exception");
     }
   }
 
@@ -796,6 +830,11 @@ public static String yices_model_to_string(long m) {
    */
   public static native int yices_is_thread_safe();
 
+  /**
+   * @return int 1 if the Yices2-lib is compiled with MCSAT support and 0 otherwise
+   */
+  public static native int yices_has_mcsat();
+
   /** The function first checks whether f is satisifiable or unsatisfiable. */
   public static native int yices_check_formula(int term, String logic, long model, String delegate);
 

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

@@ -54,6 +54,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_by_name;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_name;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_has_mcsat;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_idiv;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_iff;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_init;
@@ -609,8 +610,13 @@ public void bvMul() {
 
   @Test
   public void isThreadSafe() {
-    // TODO: this explains why our concurrency tests fail ;D FIX!
-    assertThat(yices_is_thread_safe()).isEqualTo(0);
+    // Check that we compiled with --thread-safety to make it reentrant
+    assertThat(yices_is_thread_safe()).isEqualTo(1);
+  }
+
+  @Test
+  public void hasMCSat() {
+    assertThat(yices_has_mcsat()).isEqualTo(0);
   }
 
   @Test

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

@@ -121,6 +121,11 @@ public void bvTooSmallNum() {
 
   @Test
   public void bvModelValue32bit() throws SolverException, InterruptedException {
+    assume()
+        .withMessage("Yices2 is too slow in this test")
+        .that(solver)
+        .isNotEqualTo(Solvers.YICES2);
+
     BitvectorFormula var = bvmgr.makeVariable(32, "var");
 
     Map<Long, Long> values = new LinkedHashMap<>();