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 - + 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 - + - + - + - + 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..75e3124075 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 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; diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java index eb4a06f48f..93b3b0fd49 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java +++ b/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 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 d642fd74e3..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"}) @@ -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 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); 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..33761613df 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; @@ -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 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/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. 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(); 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) {