From 492c0e825026c8d1adb3c8a4a8a74d7e0d4c5101 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 8 Sep 2025 21:39:48 +0200 Subject: [PATCH 1/5] Tests: Enable tests that were previously disabled, but are now running fine --- .../test/BooleanFormulaManagerTest.java | 5 +- .../test/FloatingPointFormulaManagerTest.java | 10 +-- .../java_smt/test/FormulaClassifierTest.java | 19 ++---- .../java_smt/test/FormulaManagerTest.java | 2 - .../test/InterpolatingProverTest.java | 15 ----- src/org/sosy_lab/java_smt/test/ModelTest.java | 12 +--- .../java_smt/test/QuantifierManagerTest.java | 65 ++----------------- .../java_smt/test/SolverAllSatTest.java | 3 - .../java_smt/test/SolverBasedTest0.java | 1 - .../java_smt/test/SolverConcurrencyTest.java | 18 ++--- .../java_smt/test/SolverFormulaIOTest.java | 2 +- .../SolverFormulaWithAssumptionsTest.java | 11 ---- .../java_smt/test/SolverStackTest0.java | 10 --- .../java_smt/test/SolverTheoriesTest.java | 16 ++--- .../java_smt/test/SolverVisitorTest.java | 48 ++++---------- .../test/StringFormulaManagerTest.java | 23 +++---- .../java_smt/test/UfEliminationTest.java | 3 - .../java_smt/test/VariableNamesTest.java | 18 +---- 18 files changed, 55 insertions(+), 226 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java index 2af4869e12..594cbeddac 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaManagerTest.java @@ -269,13 +269,12 @@ public void testDisjunctionArgsExtractionRecursive() @Test public void simplificationTest() { - // Boolector and CVC5 fail this as it either simplifies to much, or nothing - // TODO: maybe this is just a matter of options, check! + // Boolector fail this as it either simplifies to much, or nothing assume() .withMessage( "Solver %s fails on this test as it does not simplify any formulas.", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.BOOLECTOR, Solvers.CVC5); + .isNotEqualTo(Solvers.BOOLECTOR); BooleanFormula tru = bmgr.makeBoolean(true); BooleanFormula fals = bmgr.makeBoolean(false); diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 74390241cf..f8579710cf 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -1082,15 +1082,12 @@ private List getListOfFloats() { Float.POSITIVE_INFINITY, Float.NEGATIVE_INFINITY, 0.0f, + -0.0f, 1f, -1f, 2f, -2f); - if (solverToUse() != Solvers.MATHSAT5) { - flts.add(-0.0f); // MathSat5 fails for NEGATIVE_ZERO - } - for (int i = 1; i < 10; i++) { for (int j = 1; j < 10; j++) { flts.add((float) (i * Math.pow(10, j))); @@ -1119,15 +1116,12 @@ private List getListOfDoubles() { Double.POSITIVE_INFINITY, Double.NEGATIVE_INFINITY, 0.0, + -0.0, 1d, -1d, 2d, -2d); - if (solverToUse() != Solvers.MATHSAT5) { - dbls.add(-0.0); // MathSat5 fails for NEGATIVE_ZERO - } - for (int i = 1; i < 10; i++) { for (int j = 1; j < 10; j++) { dbls.add(i * Math.pow(10, j)); diff --git a/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java b/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java index 4817b67a76..440c0a322f 100644 --- a/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java +++ b/src/org/sosy_lab/java_smt/test/FormulaClassifierTest.java @@ -165,7 +165,6 @@ public void test_ABVIRA() { requireBitvectors(); requireIntegers(); requireRationals(); - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula String query = NUMERAL_VARS + BV_VARS @@ -180,7 +179,6 @@ public void test_ABV() { requireArrays(); requireQuantifiers(); requireBitvectors(); - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula String query = BOOL_VARS + BV_VARS @@ -195,7 +193,6 @@ public void test_QF_AUFBV() { requireParser(); requireArrays(); requireBitvectors(); - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula String query = BV_VARS + "(assert (and (= bv bv2) (= bvarr bvarr2) (= (bvfoo bv) bv2)" + "))"; classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_AUFBV"); @@ -205,7 +202,8 @@ public void test_QF_AUFBV() { public void test_QF_BV() { requireParser(); requireBitvectors(); - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula + // Princess rewrites the formula and replaces the bitvector constant with an integer term + assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); String query = BV_VARS + "(assert (bvult bv (bvadd bv #x1)))"; classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_BV"); @@ -236,7 +234,6 @@ public void test_QF_NIA() { requireIntegers(); requireNonlinear(); String query = NUMERAL_VARS + "(assert (< xx (* x x)))"; - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_NIA"); } @@ -258,7 +255,6 @@ public void test_QF_UFLIRA() { requireIntegers(); requireRationals(); // NUMERAL_VARS includes REALs String query = NUMERAL_VARS + "(assert (= (foo x) x))"; - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_UF"); } @@ -271,11 +267,11 @@ public void test_QF_UF() { .withMessage("MathSAT does not support functions with Bool arguments") .that(solverToUse()) .isNotEqualTo(Solvers.MATHSAT5); - classifier.visit(mgr.parse(query)); assume() + .withMessage("Princess will rewrite UFs with boolean arguments") .that(solverToUse()) - .isNotEqualTo(Solvers.PRINCESS); // Princess classifies it as QF_UFLIA - // TODO: see why Princess classifies this wrongly + .isNotEqualTo(Solvers.PRINCESS); + classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_UF"); } @@ -285,7 +281,6 @@ public void test_QF_UFBVLIRA() { requireBitvectors(); requireRationals(); requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula String query = NUMERAL_VARS + BV_VARS + "(assert (and (= bv bv2) (= (foo x) x)))"; classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_UFBV"); @@ -295,7 +290,6 @@ public void test_QF_UFBVLIRA() { public void test_QF_UFBV() { requireParser(); requireBitvectors(); - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula String query = BV_VARS + "(assert (and (= bv bv2) (= (bvfoo bv) bv2)))"; classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_UFBV"); @@ -307,7 +301,6 @@ public void test_QF_UFLIRA2() { requireIntegers(); requireRationals(); // NUMERAL_VARS includes REALs String query = NUMERAL_VARS + "(assert (< xx (+ x (foo x))))"; - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula classifier.visit(mgr.parse(query)); assertThat(classifier.toString()).isEqualTo("QF_UFLIA"); } @@ -349,7 +342,7 @@ public void test_UFNRA() { requireParser(); requireRationals(); requireNonlinear(); - requireQuantifiers(); // TODO SMTInterpol fails when parsing this + requireQuantifiers(); String query = NUMERAL_VARS + "(assert (exists ((zz Real)) (< (* y yy) (bar y))))"; assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); // Princess rewrites the formula classifier.visit(mgr.parse(query)); diff --git a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java index c57a026149..2cf4a2eaf6 100644 --- a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java @@ -35,7 +35,6 @@ public class FormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBase public void testEmptySubstitution() throws SolverException, InterruptedException { requireSubstitution(); requireIntegers(); - assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS); IntegerFormula variable1 = imgr.makeVariable("variable1"); IntegerFormula variable2 = imgr.makeVariable("variable2"); @@ -56,7 +55,6 @@ public void testEmptySubstitution() throws SolverException, InterruptedException public void testNoSubstitution() throws SolverException, InterruptedException { requireSubstitution(); requireIntegers(); - assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS); IntegerFormula variable1 = imgr.makeVariable("variable1"); IntegerFormula variable2 = imgr.makeVariable("variable2"); diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 4cc7cae699..9287b00f67 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -199,11 +199,6 @@ public void binaryInterpolationWithConstantFalse() public void binaryBVInterpolation1() throws SolverException, InterruptedException { requireBitvectors(); - assume() - .withMessage("Solver %s runs into timeout on this test", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); @@ -262,11 +257,6 @@ public void sequentialInterpolation() throws SolverException, InterruptedExc InterpolatingProverEnvironment stack = newEnvironmentForTest(); requireIntegers(); - assume() - .withMessage("Solver %s runs into timeout on this test", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - int i = index.getFreshId(); IntegerFormula zero = imgr.makeNumber(0); @@ -426,11 +416,6 @@ public void sequentialInterpolationWithFewPartitions() public void sequentialBVInterpolation() throws SolverException, InterruptedException { requireBitvectors(); - assume() - .withMessage("Solver %s runs into timeout on this test", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - InterpolatingProverEnvironment stack = newEnvironmentForTest(); int i = index.getFreshId(); diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 431a20e921..a299d89c67 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1152,11 +1152,6 @@ public void testGetArrays3() throws SolverException, InterruptedException { requireArrays(); requireArrayModel(); - assume() - .withMessage("As of now, only Princess does not support multi-dimensional arrays") - .that(solver) - .isNotSameInstanceAs(Solvers.PRINCESS); - // create formula for "arr[5][3][1]==x && x==123" BooleanFormula f = mgr.parse( @@ -1741,12 +1736,7 @@ private void checkModelAssignmentsValid( public void ufTest() throws SolverException, InterruptedException { requireQuantifiers(); requireBitvectors(); - // only Z3 fulfills these requirements - - assume() - .withMessage("solver does not implement optimisation") - .that(solverToUse()) - .isEqualTo(Solvers.Z3); + requireOptimization(); BitvectorType t32 = FormulaType.getBitvectorTypeWithSize(32); FunctionDeclaration si1 = fmgr.declareUF("*signed_int@1", t32, t32); diff --git a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java index 6640729f2f..f1b892f8d7 100644 --- a/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/QuantifierManagerTest.java @@ -114,11 +114,6 @@ private SolverException handleSolverException(SolverException e) throws SolverEx @Test public void testLIAForallArrayConjunctUnsat() throws SolverException, InterruptedException { - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT setUpLIA(); @@ -131,15 +126,8 @@ public void testLIAForallArrayConjunctUnsat() throws SolverException, Interrupte @Test public void testBVForallArrayConjunctUnsat() throws SolverException, InterruptedException { - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT setUpBV(); - // Princess does not support bitvectors in arrays - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); BooleanFormula f = bmgr.and( @@ -181,8 +169,6 @@ public void testBVForallArrayConjunctSat() throws SolverException, InterruptedEx // (forall x . b[x] = 0) AND (b[123] = 0) is SAT setUpBV(); - // Princess does not support bitvectors in arrays - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); BooleanFormula f = bmgr.and( @@ -243,11 +229,6 @@ public void testLIAForallArrayDisjunctSat2() throws SolverException, Interrupted @Test public void testLIANotExistsArrayConjunct1() throws SolverException, InterruptedException { - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - // (not exists x . not b[x] = 0) AND (b[123] = 1) is UNSAT setUpLIA(); BooleanFormula f = @@ -283,11 +264,6 @@ public void testLIANotExistsArrayConjunct2() throws SolverException, Interrupted @Test public void testLIANotExistsArrayConjunct3() throws SolverException, InterruptedException { - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - // (not exists x . b[x] = 0) AND (b[123] = 0) is UNSAT setUpLIA(); BooleanFormula f = @@ -355,8 +331,6 @@ public void testLIAExistsArrayConjunct1() throws SolverException, InterruptedExc public void testBVExistsArrayConjunct1() throws SolverException, InterruptedException { // (exists x . b[x] = 0) AND (b[123] = 1) is SAT setUpBV(); - // Princess does not support bitvectors in arrays - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); BooleanFormula f = bmgr.and( @@ -370,11 +344,6 @@ public void testBVExistsArrayConjunct1() throws SolverException, InterruptedExce @Test public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedException { setUpLIA(); - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT BooleanFormula f = @@ -384,15 +353,8 @@ public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedExc @Test public void testBVExistsArrayConjunct2() throws SolverException, InterruptedException { - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT setUpBV(); - // Princess does not support bitvectors in arrays - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); BooleanFormula f = bmgr.and(qmgr.exists(ImmutableList.of(xbv), bvArray_at_x_eq_1), bv_forall_x_a_at_x_eq_0); @@ -460,8 +422,10 @@ public void testLIAExistsArrayDisjunct1() throws SolverException, InterruptedExc public void testBVExistsArrayDisjunct1() throws SolverException, InterruptedException { // (exists x . b[x] = 0) OR (forall x . b[x] = 1) is SAT setUpBV(); - // Princess does not support bitvectors in arrays - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); + assume() + .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.PRINCESS); BooleanFormula f = bmgr.or( @@ -486,8 +450,6 @@ public void testLIAExistsArrayDisjunct2() throws SolverException, InterruptedExc public void testBVExistsArrayDisjunct2() throws SolverException, InterruptedException { // (exists x . b[x] = 1) OR (exists x . b[x] = 1) is SAT setUpBV(); - // Princess does not support bitvectors in arrays - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); BooleanFormula f = bmgr.or( @@ -819,11 +781,6 @@ public void testIntrospectionExistsInteger() { @Test public void testEmpty() { - assume() - .withMessage("TODO: The JavaSMT code for Princess explicitly allows this.") - .that(solverToUse()) - .isNotEqualTo(Solvers.PRINCESS); - // An empty list of quantified variables throws an exception. assertThrows( IllegalArgumentException.class, @@ -881,11 +838,10 @@ public void checkBVQuantifierEliminationFail() throws InterruptedException, Solv requireBitvectors(); requireQuantifierElimination(); // Boolector quants need to be reworked - // Princess does not support bitvectors in arrays assume() .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.CVC5, Solvers.PRINCESS); + .isNotEqualTo(Solvers.CVC5); int width = 2; BitvectorFormula xx = bvmgr.makeVariable(width, "x_bv"); @@ -938,8 +894,6 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE // quantifier-free equivalent: (and (= b2 #x00000006) // (= a3 #x00000000)) - // Z3 fails this currently. Remove once that's not longer the case! - assume().that(solverToUse()).isNotEqualTo(Solvers.Z3); int width = 32; BitvectorFormula a2 = bvmgr.makeVariable(width, "a2"); @@ -965,11 +919,6 @@ public void checkBVQuantifierElimination2() throws InterruptedException, SolverE @Test public void testExistsRestrictedRange() throws SolverException, InterruptedException { setUpLIA(); - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - ArrayFormula b = amgr.makeArray("b", FormulaType.IntegerType, FormulaType.IntegerType); BooleanFormula bAtXEq1 = imgr.equal(amgr.select(b, x), imgr.makeNumber(1)); @@ -1023,10 +972,6 @@ public void testExistsRestrictedRangeWithoutInconclusiveSolvers() @Test public void testForallRestrictedRange() throws SolverException, InterruptedException { setUpLIA(); - assume() - .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); ArrayFormula b = amgr.makeArray("b", FormulaType.IntegerType, FormulaType.IntegerType); diff --git a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java index b43e77bfb3..7775633373 100644 --- a/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverAllSatTest.java @@ -77,9 +77,6 @@ public void setupEnvironment() { // TODO how can we support allsat in MathSat5-interpolation-prover? assume().that(solverToUse()).isNotEqualTo(Solvers.MATHSAT5); - // CVC4 and Boolector do not support interpolation - assume().that(solverToUse()).isNoneOf(Solvers.CVC4, Solvers.BOOLECTOR, Solvers.Z3); - env = context.newProverEnvironmentWithInterpolation(ProverOptions.GENERATE_ALL_SAT); break; diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e96c7b39f1..7a137e1973 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -337,7 +337,6 @@ protected void requireParser() { } protected void requireArrayModel() { - // INFO: OpenSmt does not support model generation for array assume() .withMessage("Solver %s does not support model generation for arrays", solverToUse()) .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index 3b3029a7d1..840d44941a 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -134,7 +134,7 @@ private void requireConcurrentMultipleStackSupport() { Solvers.SMTINTERPOL, Solvers.BITWUZLA, Solvers.BOOLECTOR, - Solvers.OPENSMT, // INFO: OpenSMT does not support concurrent stacks + Solvers.OPENSMT, Solvers.MATHSAT5, Solvers.Z3, Solvers.PRINCESS, @@ -292,13 +292,11 @@ BooleanFormula getFormula() { public void testFormulaTranslationWithConcurrentContexts() throws InvalidConfigurationException, InterruptedException, SolverException { requireIntegers(); - // CVC4 does not support parsing and therefore no translation. - // Princess has a wierd bug - // TODO: Look into the Princess problem + // CVC4 and CVC5 do not support parsing and therefore no translation. assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.CVC5); ConcurrentLinkedQueue contextAndFormulaList = new ConcurrentLinkedQueue<>(); @@ -529,13 +527,15 @@ private void intConcurrencyTest(SolverContext context) @Test public void continuousRunningThreadFormulaTransferTranslateTest() { requireIntegers(); - // CVC4 does not support parsing and therefore no translation. - // Princess has a wierd bug - // TODO: Look into the Princess problem + // CVC4 and CVC5 do not support parsing and therefore no translation. assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.CVC5); + assume() + .withMessage("Princess will run out of memory") + .that(solver) + .isNotEqualTo(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/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index f59932d77e..b09b4b044b 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java @@ -363,7 +363,7 @@ public void redundancyTest() { .withMessage( "Solver %s does not remove redundant sub formulae from formula dump.", solverToUse()) .that(solverToUse()) - .isNoneOf(Solvers.YICES2, Solvers.CVC5); + .isNotEqualTo(Solvers.YICES2); assume() .withMessage( diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java index 2bef74b3ef..8a5b46f754 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaWithAssumptionsTest.java @@ -19,7 +19,6 @@ import java.util.List; import org.junit.Test; 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.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -65,11 +64,6 @@ public void basicAssumptionsTest() throws SolverException, InterruptedException, InvalidConfigurationException { requireInterpolation(); - assume() - .withMessage("Solver %s runs into timeout on this test", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - IntegerFormula v1 = imgr.makeVariable("v1"); IntegerFormula v2 = imgr.makeVariable("v2"); @@ -112,11 +106,6 @@ public void assumptionsTest() throws SolverException, InterruptedException, InvalidConfigurationException { requireInterpolation(); - assume() - .withMessage("Solver %s runs into timeout on this test", solverToUse()) - .that(solverToUse()) - .isNotEqualTo(Solvers.CVC5); - int n = 5; IntegerFormula x = imgr.makeVariable("x"); diff --git a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java index 6bbcdae4c8..3754aac4c5 100644 --- a/src/org/sosy_lab/java_smt/test/SolverStackTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverStackTest0.java @@ -51,14 +51,6 @@ private void requireMultipleStackSupport() { .isNotEqualTo(Solvers.BOOLECTOR); } - protected final void requireUfValuesInModel() { - assume() - .withMessage( - "Integration of solver does not support retrieving values for UFs from a model") - .that(solver) - .isNotEqualTo(Solvers.Z3); - } - @Test public void simpleStackTestBool() throws SolverException, InterruptedException { BasicProverEnvironment stack = newEnvironmentForTest(context); @@ -631,8 +623,6 @@ public void modelForSatFormulaWithUF() throws SolverException, InterruptedExcept assertThat(model.evaluate(varA)).isEqualTo(BigInteger.ZERO); assertThat(model.evaluate(varB)).isEqualTo(BigInteger.ZERO); - requireUfValuesInModel(); - assertThat(model.evaluate(fmgr.callUF(uf, imgr.makeNumber(BigDecimal.ZERO)))) .isEqualTo(BigInteger.ZERO); } diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index 238e7cad19..85d1feeba7 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -727,11 +727,6 @@ public void testMakeBitVectorArray() { requireArrays(); requireBitvectors(); - assume() - .withMessage("Solver does not support bit-vector arrays.") - .that(solver) - .isNotEqualTo(Solvers.PRINCESS); - BitvectorFormula _i = mgr.getBitvectorFormulaManager().makeVariable(64, "i"); ArrayFormula _b = amgr.makeArray( @@ -745,6 +740,9 @@ public void testMakeBitVectorArray() { // Mathsat5 has a different internal representation of the formula assertThat(_b_at_i.toString()).isEqualTo("(`read_T(19)_T(21)` b i)"); break; + case PRINCESS: + assertThat(_b_at_i.toString()).isEqualTo("select(b, i)"); + break; case BOOLECTOR: assume() .withMessage("Solver %s does not printing formulae.", solverToUse()) @@ -818,11 +816,6 @@ public void testNestedBitVectorArray() { requireBitvectors(); requireIntegers(); - assume() - .withMessage("Solver does not support bit-vector arrays.") - .that(solver) - .isNotEqualTo(Solvers.PRINCESS); - IntegerFormula _i = imgr.makeVariable("i"); ArrayFormula> multi = amgr.makeArray( @@ -838,6 +831,9 @@ public void testNestedBitVectorArray() { assertThat(valueInMulti.toString()) .isEqualTo("(`read_int_T(19)` (`read_int_T(20)` multi " + "i) i)"); break; + case PRINCESS: + assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); + break; default: assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)"); } diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 9ecc665d8e..9cb791bbc5 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -211,11 +211,7 @@ public void bitvectorIdVisit() throws SolverException, InterruptedException { bvmgr.greaterOrEquals(x, y, true), bvmgr.greaterOrEquals(x, y, false))) { mgr.visit(f, new FunctionDeclarationVisitorNoUF()); - if (Solvers.PRINCESS != solver) { - // Princess models BV theory with intervals, such as "mod_cast(lower, upper , value)". - // The interval function is of FunctionDeclarationKind.OTHER and thus we cannot check it. - mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); - } + mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); BooleanFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); assertThat(f2).isEqualTo(f); assertThatFormula(f).isEquivalentTo(f2); @@ -243,11 +239,7 @@ public void bitvectorIdVisit() throws SolverException, InterruptedException { bvmgr.rotateLeft(x, y), bvmgr.rotateRight(x, y))) { mgr.visit(f, new FunctionDeclarationVisitorNoUF()); - if (Solvers.PRINCESS != solver) { - // Princess models BV theory with intervals, such as "mod_cast(lower, upper , value)". - // The interval function is of FunctionDeclarationKind.OTHER and thus we cannot check it. - mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); - } + mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); BitvectorFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); assertThat(f2).isEqualTo(f); assertThatFormula(bmgr.not(bvmgr.equal(f, f2))).isUnsatisfiable(); @@ -261,12 +253,8 @@ public void bitvectorIdVisit2() throws SolverException, InterruptedException { BitvectorFormula n = bvmgr.makeBitvector(8, 13); for (BitvectorFormula f : new BitvectorFormula[] {n}) { - mgr.visit(f, new FunctionDeclarationVisitorNoUF()); - if (Solvers.PRINCESS != solver) { - // Princess models BV theory with intervals, such as "mod_cast(lower, upper , value)". - // The interval function is of FunctionDeclarationKind.OTHER and thus we cannot check it. - mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); - } + mgr.visit(f, new SolverVisitorTest.FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new SolverVisitorTest.FunctionDeclarationVisitorNoOther(mgr)); BitvectorFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); assertThat(f2).isEqualTo(f); assertThatFormula(bmgr.not(bvmgr.equal(f, f2))).isUnsatisfiable(); @@ -281,7 +269,7 @@ public void integerConstantVisit() { 0, 1, 2, 17, 127, 255, -1, -2, -17, -127, 127000, 255000, -100, -200, -1700, -127000, -255000, }) { - ConstantsVisitor visitor = new ConstantsVisitor(); + SolverVisitorTest.ConstantsVisitor visitor = new ConstantsVisitor(); mgr.visit(imgr.makeNumber(n), visitor); assertThat(visitor.found).containsExactly(BigInteger.valueOf(n)); } @@ -676,10 +664,7 @@ public TraversalProcess visitFunction( break; case BV_NOT: case BV_NEG: - // Yices is special in some cases - if (Solvers.YICES2 != solverToUse()) { - assertThat(pArgs).hasSize(1); - } + assertThat(pArgs).hasSize(1); break; case BV_ADD: assertThat(pArgs).contains(x); @@ -688,6 +673,7 @@ public TraversalProcess visitFunction( case BV_MUL: assertThat(pArgs).contains(y); assertThat(pArgs).hasSize(2); + // Yices is special in some cases if (Solvers.YICES2 != solverToUse()) { assertThat(pArgs).contains(x); } @@ -722,8 +708,8 @@ public void stringInBooleanFormulaIdVisit() throws SolverException, InterruptedE smgr.prefix(x, y), smgr.suffix(x, y), smgr.in(x, r))) { - mgr.visit(f, new FunctionDeclarationVisitorNoUF()); - mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); + mgr.visit(f, new SolverVisitorTest.FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new SolverVisitorTest.FunctionDeclarationVisitorNoOther(mgr)); BooleanFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); assertThat(f2).isEqualTo(f); assertThatFormula(f).isEquivalentTo(f2); @@ -747,7 +733,8 @@ public void stringInStringFormulaVisit() throws SolverException, InterruptedExce .add(smgr.charAt(x, offset)) .add(smgr.toStringFormula(offset)) .add(smgr.concat(x, y, z)); - if (solverToUse() != Solvers.PRINCESS) { // TODO Princess crashes with MatchError of IFunApp + if (solverToUse() != Solvers.PRINCESS) { + // TODO Princess crashes with MatchError of IFunApp, fixed in Ostrich 2.0 formulas.add(smgr.fromCodePoint(cp)); } if (solverToUse() != Solvers.Z3) { @@ -782,13 +769,10 @@ public void stringInRegexFormulaVisit() { .add(smgr.closure(r)) .add(smgr.concat(r, r, r, s, s, s)) .add(smgr.cross(r)); - if (solverToUse() != Solvers.Z3) { - formulas.add(smgr.difference(r, s)).add(smgr.complement(r)); - // invalid function OTHER/INTERNAL in visitor, bug in Z3? - } + formulas.add(smgr.difference(r, s)).add(smgr.complement(r)); for (RegexFormula f : formulas.build()) { - mgr.visit(f, new FunctionDeclarationVisitorNoUF()); - mgr.visit(f, new FunctionDeclarationVisitorNoOther(mgr)); + mgr.visit(f, new SolverVisitorTest.FunctionDeclarationVisitorNoUF()); + mgr.visit(f, new SolverVisitorTest.FunctionDeclarationVisitorNoOther(mgr)); RegexFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); assertThat(f2).isEqualTo(f); } @@ -1159,8 +1143,6 @@ public void testIntegerFormulaQuantifierHandlingTrivialUNSAT() throws Exception public void testNestedIntegerFormulaQuantifierHandling() throws Exception { requireQuantifiers(); requireIntegers(); - // Z3 returns UNKNOWN as its quantifiers can not handle this. - assume().that(solverToUse()).isNotEqualTo(Solvers.Z3); assume() .withMessage("Yices2 quantifier support is very limited at the moment") .that(solverToUse()) @@ -1181,8 +1163,6 @@ public void testNestedIntegerFormulaQuantifierHandling() throws Exception { public void testNestedIntegerFormulaQuantifierRecursiveHandling() throws Exception { requireQuantifiers(); requireIntegers(); - // Z3 returns UNKNOWN as its quantifiers can not handle this. - assume().that(solverToUse()).isNotEqualTo(Solvers.Z3); assume() .withMessage("Yices2 quantifier support is very limited at the moment") .that(solverToUse()) diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index 29fe5d89b0..ce2da4e6cc 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -122,7 +122,7 @@ private StringFormula makeStringEscaped(String pString) { } private void requireVariableStringLiterals() { - // FIXME: Remove once support for operations on non-singleton Strings has been added + // FIXME: Remove once we've updated to Ostrich 2.0 // See https://github.com/uuverifiers/ostrich/issues/88 assume() .withMessage( @@ -162,7 +162,7 @@ public void testOutputUnescape() throws SolverException, InterruptedException { .isEqualTo("\\u{39E}"); // Test with a character that is not in the BMP - if (solver != Solvers.PRINCESS && solver != Solvers.CVC5) { + if (solver != Solvers.PRINCESS) { String str = Character.toString(0x200cb); assertThat(model.evaluate(smgr.makeString(str))).isEqualTo(str); } @@ -186,8 +186,6 @@ public void testRegexAll3() throws SolverException, InterruptedException { @Test public void testRegexAllChar() throws SolverException, InterruptedException { - requireVariableStringLiterals(); - RegexFormula regexAllChar = smgr.allChar(); assertThatFormula(smgr.in(a, regexAllChar)).isSatisfiable(); @@ -204,8 +202,6 @@ public void testRegexAllChar() throws SolverException, InterruptedException { @Test public void testRegexAllCharUnicode() throws SolverException, InterruptedException { - requireVariableStringLiterals(); - RegexFormula regexAllChar = smgr.allChar(); // special single characters. @@ -217,8 +213,10 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti assertThatFormula(smgr.in(makeStringEscaped("\\u{fa6a}"), regexAllChar)).isTautological(); assertThatFormula(smgr.in(smgr.makeString("頻"), regexAllChar)).isTautological(); // Xiangqi Black Horse from Supplementary Multilingual Plane - assertThatFormula(smgr.in(makeStringEscaped("\\u{1fa6a}"), regexAllChar)).isTautological(); - + if (solver != Solvers.PRINCESS) { + // Princess does not support codepoint > 0xffff + assertThatFormula(smgr.in(makeStringEscaped("\\u{1fa6a}"), regexAllChar)).isTautological(); + } // Combining characters are not matched as one character. assertThatFormula(smgr.in(smgr.makeString("ab"), regexAllChar)).isUnsatisfiable(); assertThatFormula(smgr.in(smgr.makeString("abcdefgh"), regexAllChar)).isUnsatisfiable(); @@ -244,8 +242,6 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti @Test public void testStringRegex2() throws SolverException, InterruptedException { - requireVariableStringLiterals(); - RegexFormula regex = smgr.concat(smgr.closure(a2z), smgr.makeRegex("ll"), smgr.closure(a2z)); assertThatFormula(smgr.in(hello, regex)).isSatisfiable(); } @@ -381,9 +377,6 @@ public void testStringRange() throws SolverException, InterruptedException { @Test public void testStringPrefixSuffixConcat() throws SolverException, InterruptedException { - // FIXME: Princess will timeout on this test - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); - // check whether "prefix + suffix == concat" StringFormula prefix = smgr.makeVariable("prefix"); StringFormula suffix = smgr.makeVariable("suffix"); @@ -542,12 +535,12 @@ public void testStringLengthPositiv() throws SolverException, InterruptedExcepti @Test public void testStringCompare() throws SolverException, InterruptedException { + // TODO regression: + // - CVC5 was able to solve this in v1.0.2, but no longer in v1.0.5 assume() .withMessage("Solver is quite slow for this example") .that(solverToUse()) .isNotEqualTo(Solvers.CVC5); - // TODO regression: - // - CVC5 was able to solve this in v1.0.2, but no longer in v1.0.5 requireVariableStringLiterals(); diff --git a/src/org/sosy_lab/java_smt/test/UfEliminationTest.java b/src/org/sosy_lab/java_smt/test/UfEliminationTest.java index 5f3bbe2e01..b98dbc562f 100644 --- a/src/org/sosy_lab/java_smt/test/UfEliminationTest.java +++ b/src/org/sosy_lab/java_smt/test/UfEliminationTest.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.test; -import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.api.FormulaType.BooleanType; import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; @@ -20,7 +19,6 @@ import java.util.Map; import org.junit.Before; import org.junit.Test; -import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FunctionDeclaration; @@ -184,7 +182,6 @@ public void nestedUfs3() throws SolverException, InterruptedException { public void twoFormulasTest() throws SolverException, InterruptedException { // See FormulaManagerTest.testEmptySubstitution(), FormulaManagerTest.testNoSubstitution() requireIntegers(); - assume().withMessage("Princess fails").that(solver).isNotEqualTo(Solvers.PRINCESS); // f := uf(v1, v3) XOR uf(v2, v4) IntegerFormula variable1 = imgr.makeVariable("variable1"); diff --git a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java index 2f61eb09cd..c1a8641731 100644 --- a/src/org/sosy_lab/java_smt/test/VariableNamesTest.java +++ b/src/org/sosy_lab/java_smt/test/VariableNamesTest.java @@ -296,8 +296,6 @@ public void testNameIntArray() throws SolverException, InterruptedException { public void testNameBvArray() throws SolverException, InterruptedException { requireBitvectors(); requireArrays(); - // Someone who knows princess has to debug this! - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); for (String name : NAMES) { testName0( name, @@ -335,8 +333,6 @@ public void testNameUF1Int() throws SolverException, InterruptedException { @Test public void testNameUFBv() throws SolverException, InterruptedException { requireBitvectors(); - // Someone who knows princess has to debug this! - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); for (String name : getAllNames()) { testName0( name, @@ -401,10 +397,7 @@ public Void visitQuantifier( Quantifier pQuantifier, List pBoundVariables, BooleanFormula pBody) { - if (solverToUse() != Solvers.PRINCESS) { - // TODO Princess does not (yet) return quantified variables. assertThat(pBoundVariables).hasSize(1); - } for (Formula f : pBoundVariables) { Map map = mgr.extractVariables(f); assertThat(map).hasSize(1); @@ -487,10 +480,7 @@ public Void visitQuantifier( Quantifier pQuantifier, List pBoundVariables, BooleanFormula pBody) { - if (solverToUse() != Solvers.PRINCESS) { - // TODO Princess does not return quantified variables. assertThat(pBoundVariables).hasSize(1); - } for (Formula f : pBoundVariables) { Map map = mgr.extractVariables(f); assertThat(map).hasSize(1); @@ -537,11 +527,7 @@ 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. + // FIXME: Broken on yices2, fixed in 2.7.0 assume().that(solverToUse()).isNotEqualTo(Solvers.YICES2); for (String name : getAllNames()) { BooleanFormula var = createVariableWith(bmgr::makeVariable, name); @@ -610,8 +596,6 @@ public void testIntArrayVariable() { public void testBvArrayVariable() { requireArrays(); requireBitvectors(); - // Someone who knows princess has to debug this! - assume().that(solverToUse()).isNotEqualTo(Solvers.PRINCESS); for (String name : getAllNames()) { createVariableWith( v -> From 3c9d298c6017e1124be1e08ce79197fbf00e58b4 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 8 Sep 2025 21:40:57 +0200 Subject: [PATCH 2/5] Tests: Enable parallel tests for CVC5 Concurrency now works on CVC5. We should remember to update DebugMode --- .../sosy_lab/java_smt/test/DebugModeTest.java | 3 +- .../test/SolverThreadLocalityTest.java | 57 ------------------- 2 files changed, 2 insertions(+), 58 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java index dbfe92732b..4d614a82e8 100644 --- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java +++ b/src/org/sosy_lab/java_smt/test/DebugModeTest.java @@ -112,6 +112,7 @@ public void nonLocalThreadTest() { }); // We expect debug mode to throw an exception only on CVC5 + // TODO CVC5 supports this now. Update debug mode if (solverToUse() == Solvers.CVC5) { assertThrows(IllegalStateException.class, () -> checkForExceptions(result)); } else { @@ -179,7 +180,7 @@ public void noSharedDeclarationsTest() throws InvalidConfigurationException { newFmgr.declareUF( "id", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType)); - // We expect debug mode to throw an exception for all solvers, except Princess, CVC4 and Yices + // We expect debug mode to throw an exception for all solvers, except Princess and Yices if (!List.of(Solvers.PRINCESS, Solvers.YICES2).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> checkDeclarationInDebugContext(id)); } else { diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 5718007828..7546f46ead 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -9,12 +9,9 @@ package org.sosy_lab.java_smt.test; import static com.google.common.truth.TruthJUnit.assume; -import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.collect.ImmutableList; -import com.google.common.truth.Truth; -import java.util.Collection; import java.util.concurrent.ExecutionException; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; @@ -41,9 +38,6 @@ public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolv private HardIntegerFormulaGenerator hardProblem; private static final int DEFAULT_PROBLEM_SIZE = 8; - private static final Collection SOLVERS_NOT_SUPPORTING_FORMULA_THREAD_SHARING = - ImmutableList.of(Solvers.CVC5); - @Before public void makeThreads() { executor = Executors.newFixedThreadPool(2); @@ -78,7 +72,6 @@ public void allLocalTest() throws InterruptedException, SolverException { public void nonLocalContextTest() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); // generate a new context in another thread, i.e., non-locally Future result = executor.submit(() -> factory.generateContext()); @@ -113,7 +106,6 @@ public void nonLocalContextTest() public void nonLocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); // generate a new formula in another thread, i.e., non-locally Future result = @@ -142,7 +134,6 @@ public void nonLocalFormulaTest() @Test public void nonLocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); @@ -173,53 +164,6 @@ public void nonLocalProverTest() throws InterruptedException, ExecutionException assert task.get() == null; } - @Test - public void nonLocalFormulaTranslationTest() throws Throwable { - // Test that even when using translation, the thread local problem persists for CVC5 - requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - - BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); - - // generate a new prover in another thread, i.e., non-locally - Future task; - if (SOLVERS_NOT_SUPPORTING_FORMULA_THREAD_SHARING.contains(solverToUse())) { - task = - executor.submit( - () -> - assertThrows( - io.github.cvc5.CVC5ApiException.class, - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push( - context - .getFormulaManager() - .translateFrom(formula, context.getFormulaManager())); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException exception) { - throw new RuntimeException(exception); - } - })); - Truth.assertThat(task.get()).isInstanceOf(io.github.cvc5.CVC5ApiException.class); - - } else { - task = - executor.submit( - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push( - context - .getFormulaManager() - .translateFrom(formula, context.getFormulaManager())); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException exception) { - throw new RuntimeException(exception); - } - }); - Truth.assertThat(task.get()).isNull(); - } - } - @Override protected Logics logicToUse() { return Logics.QF_LIA; @@ -264,7 +208,6 @@ public void localInterpolationTest() throws InterruptedException, SolverExce public void nonLocalInterpolationTest() throws InterruptedException, ExecutionException { requireIntegers(); requireInterpolation(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula f1 = imgr.lessThan(imgr.makeVariable("A"), imgr.makeVariable("B")); BooleanFormula f2 = imgr.lessThan(imgr.makeVariable("B"), imgr.makeVariable("A")); From 1997a023f91f6d4ab052392d7e97fed143b5752d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 8 Sep 2025 22:11:58 +0200 Subject: [PATCH 3/5] Tests: Add a note about the failing Princess test --- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index a299d89c67..f114929117 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1152,6 +1152,8 @@ public void testGetArrays3() throws SolverException, InterruptedException { requireArrays(); requireArrayModel(); + // FIXME Add support for multi-dimensional array to the Princess backend + // create formula for "arr[5][3][1]==x && x==123" BooleanFormula f = mgr.parse( From dd333a32a895c243d3ef815493f94b358a01e3b6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 8 Sep 2025 22:01:28 +0200 Subject: [PATCH 4/5] Tests: Add a note about the failing CVC5 test --- src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java index 9287b00f67..90275f1d8e 100644 --- a/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java +++ b/src/org/sosy_lab/java_smt/test/InterpolatingProverTest.java @@ -285,6 +285,10 @@ public void sequentialInterpolation() throws SolverException, InterruptedExc List itps4 = stack.getSeqInterpolants( Lists.transform(ImmutableList.of(TA, TA, TA, TB, TC, TD, TD), ImmutableSet::of)); + + // FIXME With CVC5 the last interpolant returned by CVC5InterpolatingProver.getCVC5Interpolation + // is "null". Replacing it with "false" fixes the test + List itps5 = stack.getSeqInterpolants( Lists.transform(ImmutableList.of(TA, TA, TB, TC, TD, TA, TD), ImmutableSet::of)); From 87abbabcb440f4d9cbd6caf0f0b2090eadc6eada Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 9 Sep 2025 11:56:41 +0200 Subject: [PATCH 5/5] Tests: Re-enable timeouts for two tests --- src/org/sosy_lab/java_smt/test/ModelTest.java | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index f114929117..d769c4b4f1 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -1729,7 +1729,6 @@ private void checkModelAssignmentsValid( // supported yet // TODO: only filter out UF formulas here, not all if (solver != Solvers.BOOLECTOR) { - // CVC5 crashes here assertThatFormula(bmgr.and(pModelAssignments)).implies(constraint); } } @@ -2401,8 +2400,7 @@ public void testGetBooleans1() throws SolverException, InterruptedException { false); } - @Test // (timeout = 10_000) - // TODO CVC5 crashes on making the first boolean symbol when using timeout ???. + @Test(timeout = 10_000) public void testDeeplyNestedFormulaLIA() throws SolverException, InterruptedException { requireIntegers(); @@ -2412,8 +2410,7 @@ public void testDeeplyNestedFormulaLIA() throws SolverException, InterruptedExce var -> imgr.equal(var, imgr.makeNumber(1))); } - @Test // (timeout = 10_000) - // TODO CVC5 crashes on making the first boolean symbol when using timeout ???. + @Test(timeout = 10_000) public void testDeeplyNestedFormulaBV() throws SolverException, InterruptedException { requireBitvectors();