From 9ed415f819d3f7ce0d116be1c73b2b0060719d1b Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:47:39 +0200 Subject: [PATCH 01/10] Yices: Add yices_has_mcsat to the bindings --- ...rg_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c | 7 +++++++ .../sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java | 5 +++++ .../java_smt/solvers/yices2/Yices2NativeApiTest.java | 6 ++++++ 3 files changed, 18 insertions(+) diff --git a/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c b/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c index 9663fb4e28..c63236b3e9 100644 --- a/lib/native/source/yices2j/org_sosy_1lab_java_1smt_solvers_yices2_Yices2NativeApi.c +++ b/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. * diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index d642fd74e3..f861efcce1 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java @@ -796,6 +796,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); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java index b5c891c556..24f10dd00b 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java +++ b/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; @@ -613,6 +614,11 @@ public void isThreadSafe() { assertThat(yices_is_thread_safe()).isEqualTo(0); } + @Test + public void hasMCSat() { + assertThat(yices_has_mcsat()).isEqualTo(0); + } + @Test public void quantifierTest() { int boundVar = yices_new_variable(yices_int_type()); From 03e64936708ef7bb6a96f78c4e3ad821f3815014 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:49:50 +0200 Subject: [PATCH 02/10] Yices: Use absolute paths in the build script --- lib/native/source/yices2j/compile.sh | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/lib/native/source/yices2j/compile.sh b/lib/native/source/yices2j/compile.sh index 58f2c52135..57b5d1daf9 100755 --- a/lib/native/source/yices2j/compile.sh +++ b/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 From eedb5a758372cd3d33c99e384bc3389de17807a8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:50:57 +0200 Subject: [PATCH 03/10] Yices: Use the right "version" property when building yices --- build/build-publish-solvers/solver-yices.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build/build-publish-solvers/solver-yices.xml b/build/build-publish-solvers/solver-yices.xml index 998d7ea78c..3b2b36decf 100644 --- a/build/build-publish-solvers/solver-yices.xml +++ b/build/build-publish-solvers/solver-yices.xml @@ -39,7 +39,7 @@ SPDX-License-Identifier: Apache-2.0 - + From 366369e43dc73c55de83c8a835bd5c05b314f6ce Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:52:51 +0200 Subject: [PATCH 04/10] Yices: Update dependencies for yices --- lib/ivy.xml | 2 +- solvers_ivy_conf/ivy_javasmt_yices2.xml | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 0b37f16cfe..2101882159 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -198,7 +198,7 @@ SPDX-License-Identifier: Apache-2.0 - + - + - + - + From 4a54884690bf866f95589e2be0598353ec669aa4 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:52:09 +0200 Subject: [PATCH 05/10] Yices: API updates --- lib/native/source/yices2j/includes/defines.h | 2 +- .../solvers/yices2/Yices2FormulaCreator.java | 2 + .../java_smt/solvers/yices2/Yices2Model.java | 4 +- .../solvers/yices2/Yices2NativeApi.java | 131 +++++++++++------- 4 files changed, 87 insertions(+), 52 deletions(-) diff --git a/lib/native/source/yices2j/includes/defines.h b/lib/native/source/yices2j/includes/defines.h index 7133b275dd..2979826f9e 100644 --- a/lib/native/source/yices2j/includes/defines.h +++ b/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; \ diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java index bd4ddd6621..260fa47f5f 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java +++ b/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 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]); } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index f861efcce1..94bf345b92 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java @@ -29,61 +29,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 +98,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 From b685751e43ebabd2234557dcdbddd525f402338d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:55:40 +0200 Subject: [PATCH 06/10] Yices: Use yices_get_term_name to get the name of a function Otherwise Yices may put SMTLIB quotes around the name --- .../sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java index 260fa47f5f..75e3124075 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java @@ -402,7 +402,7 @@ private 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; From c56fc2a62707f0e3e80052b4f01bec521c2bf3ea Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 17:57:56 +0200 Subject: [PATCH 07/10] Yices: Enable tests that require parallel solver instances When compiled with --thread-safety Yices should be reentrant --- .../java_smt/solvers/yices2/Yices2NativeApiTest.java | 4 ++-- src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java index 24f10dd00b..33761613df 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java @@ -610,8 +610,8 @@ 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 diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index 3b3029a7d1..f380fa18ec 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -146,14 +146,14 @@ private void requireIntegers() { assume() .withMessage("Solver does not support integers") .that(solver) - .isNoneOf(Solvers.BOOLECTOR, Solvers.YICES2, Solvers.BITWUZLA); + .isNoneOf(Solvers.BOOLECTOR, Solvers.BITWUZLA); } private void requireBitvectors() { assume() .withMessage("Solver does not support bitvectors") .that(solver) - .isNoneOf(Solvers.SMTINTERPOL, Solvers.YICES2, Solvers.OPENSMT); + .isNoneOf(Solvers.SMTINTERPOL, Solvers.OPENSMT); } private void requireOptimization() { @@ -298,7 +298,7 @@ public void testFormulaTranslationWithConcurrentContexts() assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS, Solvers.YICES2); ConcurrentLinkedQueue contextAndFormulaList = new ConcurrentLinkedQueue<>(); @@ -535,7 +535,7 @@ public void continuousRunningThreadFormulaTransferTranslateTest() { assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.YICES2, Solvers.PRINCESS); // This is fine! We might access this more than once at a time, // but that gives only access to the bucket, which is threadsafe. From 376e4bc9c4f3ae71213059781407a09ebcd54762 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 18:00:13 +0200 Subject: [PATCH 08/10] Yices: Enable VariableNamesTest.testBoolVariableDump() The issue has been fixed in the new version and "(" characters in variable names now get quoted --- src/org/sosy_lab/java_smt/test/VariableNamesTest.java | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 2f61eb09cd..459dd503bf 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -537,12 +537,6 @@ public Void visitAtom(BooleanFormula pAtom, FunctionDeclaration @Test public void testBoolVariableDump() { - // FIXME: Broken on yices2 - // Yices does not quote symbols when dumping a formula, f.ex for the variable "(" we get - // (declare-fun |(| () Bool) - // (assert () - // which is not a valid SMTLIB script. - assume().that(solverToUse()).isNotEqualTo(Solvers.YICES2); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); if (var != null) { From 2a6c45739e38c8eeb31b464f5b03883f7bc556a0 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 18:00:45 +0200 Subject: [PATCH 09/10] Yices: Disable tests that are too slow --- .../test/BitvectorFormulaManagerTest.java | 5 +++++ .../java_smt/test/ProverEnvironmentTest.java | 16 ++++++++++++++++ .../test/SolverFormulaWithAssumptionsTest.java | 5 +++++ 3 files changed, 26 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index e70e051ada..02cb8a269b 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/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 values = new LinkedHashMap<>(); diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 861d441372..903659f5fa 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -24,6 +24,7 @@ import java.util.List; import java.util.Optional; import org.junit.Test; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; @@ -35,6 +36,11 @@ public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverB @Test public void assumptionsTest() throws SolverException, InterruptedException { + assume() + .withMessage("Yices2 is too slow in this test") + .that(solver) + .isNotEqualTo(Solvers.YICES2); + BooleanFormula b = bmgr.makeVariable("b"); BooleanFormula c = bmgr.makeVariable("c"); @@ -54,6 +60,11 @@ public void assumptionsWithModelTest() throws SolverException, InterruptedExcept .withMessage("MathSAT can't construct models for SAT check with assumptions") .that(solver) .isNotEqualTo(MATHSAT5); + assume() + .withMessage("Yices2 is too slow in this test") + .that(solver) + .isNotEqualTo(Solvers.YICES2); + BooleanFormula b = bmgr.makeVariable("b"); BooleanFormula c = bmgr.makeVariable("c"); @@ -154,6 +165,11 @@ public void unsatCoreWithAssumptionsTest() throws SolverException, InterruptedEx @Test public void testSatWithUnsatUnsatCoreOptions() throws InterruptedException, SolverException { requireUnsatCore(); + assume() + .withMessage("Yices2 is too slow in this test") + .that(solver) + .isNotEqualTo(Solvers.YICES2); + try (ProverEnvironment prover = context.newProverEnvironment(GENERATE_UNSAT_CORE)) { checkSimpleQuery(prover); } diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java index 2bef74b3ef..5eb1edcb47 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java @@ -184,6 +184,11 @@ public void assumptionsTest1() throws SolverException, InterruptedException { (check-sat-assumptions (A)) */ + assume() + .withMessage("Yices2 is too slow in this test") + .that(solver) + .isNotEqualTo(Solvers.YICES2); + BooleanFormula a = bmgr.makeVariable("a"); try (ProverEnvironment pe = context.newProverEnvironment()) { pe.push(); From 61445a9ed813cdb272c12b9db8ee1c4942ad2a2c Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 18:31:41 +0200 Subject: [PATCH 10/10] YIces: Fix handling of solver errors --- .../solvers/yices2/Yices2NativeApi.java | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index 94bf345b92..167442bb22 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/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"}) @@ -688,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); } @@ -698,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, @@ -708,7 +709,7 @@ public static boolean yices_check_sat_with_assumptions( @SuppressWarnings("try") private static boolean satCheckWithShutdownNotifier( Supplier satCheck, long pCtx, ShutdownNotifier shutdownNotifier) - throws InterruptedException { + throws InterruptedException, SolverException { int result; try (ShutdownHook hook = new ShutdownHook(shutdownNotifier, () -> yices_stop_search(pCtx))) { shutdownNotifier.shutdownIfNecessary(); @@ -718,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"); } }