From 7371dbbf1dffed3f6ee8fae3e9b522b9c50385ec Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 17:10:08 +0200 Subject: [PATCH 1/9] CVC5: Update to daily release 2025-04-24-39b3bbc In this version the concurrency issues should be fixed --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 089d59aadb..d5477a9743 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -193,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0 - + From e3c6ec8e24476d93a7ebb3d5d000381a4022edea Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 17:11:07 +0200 Subject: [PATCH 2/9] CVC5: Reenable concurrency tests --- .../sosy_lab/java_smt/test/SolverConcurrencyTest.java | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index f6f1954fb6..8ea5406061 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -124,11 +124,6 @@ public void checkThatSolverIsAvailable() throws InvalidConfigurationException { .that(solver) .isNotEqualTo(Solvers.MATHSAT5); } - - assume() - .withMessage("Solver does not support concurrency without concurrent context.") - .that(solver) - .isNotEqualTo(Solvers.CVC5); } private void requireConcurrentMultipleStackSupport() { @@ -303,7 +298,7 @@ public void testFormulaTranslationWithConcurrentContexts() assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); ConcurrentLinkedQueue contextAndFormulaList = new ConcurrentLinkedQueue<>(); @@ -540,7 +535,7 @@ public void continuousRunningThreadFormulaTransferTranslateTest() { assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.CVC5, 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 95f3be6c49cc23135221b82fcb51969c5d55d021 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 17:12:26 +0200 Subject: [PATCH 3/9] CVC5: Fix the closing sequence when destroying a CVC5 SolverContext --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index 3d070b61b5..790532e6fd 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -207,8 +207,8 @@ public String getVersion() { public void close() { if (creator != null) { closed = true; - termManager.deletePointer(); solver.deletePointer(); + termManager.deletePointer(); creator = null; } } From 8b931f2359ad8b47e3ebf21507fd2a91010de008 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 17:15:05 +0200 Subject: [PATCH 4/9] CVC5: Update debug mode tests CVC5 now uses local terms and function declarations that are only valid in their own SolverContext --- .../delegate/debugging/DebuggingSolverInformation.java | 4 ---- src/org/sosy_lab/java_smt/test/DebugModeTest.java | 4 ++-- src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java | 3 ++- 3 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java index 71d6b2a463..b348356f5e 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java @@ -48,8 +48,6 @@ public class DebuggingSolverInformation { Map.of( Solvers.PRINCESS, ConcurrentHashMap.newKeySet(), - Solvers.CVC5, - ConcurrentHashMap.newKeySet(), Solvers.YICES2, ConcurrentHashMap.newKeySet()); @@ -60,8 +58,6 @@ public class DebuggingSolverInformation { Map.of( Solvers.CVC4, ConcurrentHashMap.newKeySet(), - Solvers.CVC5, - ConcurrentHashMap.newKeySet(), Solvers.YICES2, ConcurrentHashMap.newKeySet()); diff --git a/src/org/sosy_lab/java_smt/test/DebugModeTest.java b/src/org/sosy_lab/java_smt/test/DebugModeTest.java index c0dedaa668..f6d5ea092c 100644 --- a/src/org/sosy_lab/java_smt/test/DebugModeTest.java +++ b/src/org/sosy_lab/java_smt/test/DebugModeTest.java @@ -149,7 +149,7 @@ public void noSharedFormulasTest() BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); // We expect debug mode to throw an exception for all solvers, except CVC4, CVC5 and Yices - if (!List.of(Solvers.CVC4, Solvers.CVC5, Solvers.YICES2).contains(solverToUse())) { + if (!List.of(Solvers.CVC4, Solvers.YICES2).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> checkFormulaInDebugContext(formula)); } else { checkFormulaInDebugContext(formula); @@ -180,7 +180,7 @@ public void noSharedDeclarationsTest() throws InvalidConfigurationException { "id", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType)); // We expect debug mode to throw an exception for all solvers, except Princess, CVC4 and Yices - if (!List.of(Solvers.PRINCESS, Solvers.CVC5, Solvers.YICES2).contains(solverToUse())) { + if (!List.of(Solvers.PRINCESS, Solvers.YICES2).contains(solverToUse())) { assertThrows(IllegalArgumentException.class, () -> checkDeclarationInDebugContext(id)); } else { checkDeclarationInDebugContext(id); diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 7619b7b1fe..a08232a24a 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -350,7 +350,8 @@ public void wrongContextTest() Solvers.Z3, Solvers.PRINCESS, Solvers.BOOLECTOR, - Solvers.BITWUZLA); + Solvers.BITWUZLA, + Solvers.CVC5); // FIXME: This test tries to use a formula that was created in a different context. We expect // this test to fail for most solvers, but there should be a unique error message. From 0e77f555015d52d248ccc97a8ddf68846e2d79a4 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 17:22:42 +0200 Subject: [PATCH 5/9] CVC5: Fix two native tests that depend on specific toString() outputs --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java index e15fdec270..9a61f193fd 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java @@ -202,7 +202,7 @@ public void checkFPConversion() throws CVC5ApiException { () -> termManager.mkFloatingPoint(8, 24, bvOneFourth)); assertThat(e.toString()) .contains( - "invalid argument '((_ int2bv 32) (to_int (/ 1 4)))' for 'val', expected bit-vector" + "invalid argument '((_ int_to_bv 32) (to_int (/ 1 4)))' for 'val', expected bit-vector" + " value"); } @@ -950,7 +950,7 @@ public void checkQuantifierEliminationBV() throws CVC5ApiException { Term quantElim = solver.getQuantifierElimination(assertion); - assertThat(quantElim.toString()).isEqualTo("(or (= #b01 (bvneg x_bv)) (= #b01 x_bv))"); + assertThat(quantElim.toString()).isEqualTo("(or (= #b01 (bvneg x_bv)) (= x_bv #b01))"); } @Test From 0654ee318dc381e1e7e3c569f3352eefdfcc16ee Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 23:01:53 +0200 Subject: [PATCH 6/9] CVC5: Add a comment about the crashes in TimeoutTest --- src/org/sosy_lab/java_smt/test/TimeoutTest.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/TimeoutTest.java b/src/org/sosy_lab/java_smt/test/TimeoutTest.java index ffcdcb05b3..59d6d6a0c3 100644 --- a/src/org/sosy_lab/java_smt/test/TimeoutTest.java +++ b/src/org/sosy_lab/java_smt/test/TimeoutTest.java @@ -65,7 +65,10 @@ protected Logics logicToUse() { @Before public void setUp() { - // FIXME CVC5 has interruptions, but crashes on Windows, probably due to concurrency issues + // FIXME CVC5 does not support interruption and will segfault once the timeout is reached + // The issue here seems to be that CVC5SolverContext.close() will free the C++ objects while + // the solver is still running. We could consider finding a work-around for this, or maybe + // ask the developers for a way to interrupt the solver. // TODO Add interruption for Princess assume() .withMessage(solverToUse() + " does not support interruption") From 405911c2debf24c4ac441b9e09b63dc993557243 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 25 Apr 2025 23:02:20 +0200 Subject: [PATCH 7/9] CVC5: Simplify CVC5SolverContext.getVersion --- .../sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java index 790532e6fd..97e0d269b2 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5SolverContext.java @@ -196,11 +196,7 @@ static void setSolverOptions( @Override public String getVersion() { - String version = solver.getInfo("version"); - if (version.startsWith("\"") && version.endsWith("\"")) { - version = version.substring(1, version.length() - 1); - } - return "CVC5 " + version; + return "CVC5 " + solver.getVersion(); } @Override From 72f79cca3d3f58395234bde325e0a0b502d9142d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 17 May 2025 22:22:21 +0200 Subject: [PATCH 8/9] fix warning, improve code --- .../java_smt/delegate/debugging/DebuggingSolverInformation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java index b348356f5e..9b06865d0e 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingSolverInformation.java @@ -61,7 +61,7 @@ public class DebuggingSolverInformation { Solvers.YICES2, ConcurrentHashMap.newKeySet()); - private Set definedFormulas; + private final Set definedFormulas; private final Thread solverThread = Thread.currentThread(); From d06e3c3fd3adfa478cce16321ef16295ae010f0d Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 17 May 2025 22:34:17 +0200 Subject: [PATCH 9/9] update CVC5 to latest version 2025-05-16-8aeaa19. --- lib/ivy.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index d5477a9743..5f5df5f5dd 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -193,7 +193,7 @@ SPDX-License-Identifier: Apache-2.0 - +