From 02d93be68e0a849d13a784f4a50396effc5d7b9d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 8 Dec 2023 16:07:23 +0100 Subject: [PATCH 01/46] Added tests to narrow down bug #339. So far no luck, but we did stumble upon bug #310 for CVC5. --- .../java_smt/test/SolverThreadLocalTest.java | 155 ++++++++++++++++++ 1 file changed, 155 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java new file mode 100644 index 0000000000..fcb1636e46 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -0,0 +1,155 @@ +/* + * JavaSMT is an API wrapper for a collection of SMT solvers. + * This file is part of JavaSMT. + * + * Copyright (C) 2007-2016 Dirk Beyer + * All rights reserved. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.TruthJUnit.assume; +import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; + +import java.util.concurrent.ExecutionException; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +import org.junit.Test; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.ShutdownNotifier; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.LogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +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.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.FormulaManager; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; + +public class SolverThreadLocalTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { + @Test + public void allLocalTest() throws InterruptedException, SolverException { + requireIntegers(); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + BooleanFormula formula = gen.generate(8); + + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } + } + + @Test public void nonlocalContext() throws ExecutionException, InterruptedException, + SolverException { + requireIntegers(); + + /* FIXME: Exception for CVC5 (related to #310?) + io.github.cvc5.CVC5ApiException: + Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null object + */ + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); + + ExecutorService executor = Executors.newSingleThreadExecutor(); + Future result = executor.submit(() -> { + try { + Configuration config = Configuration.builder() + .setOption("solver.solver", solverToUse().toString()) + .build(); + } catch (InvalidConfigurationException e) { + throw new RuntimeException(e); + } + LogManager logger = LogManager.createTestLogManager(); + ShutdownNotifier shutdownNotifier = ShutdownManager.create().getNotifier(); + + SolverContextFactory factory = new SolverContextFactory(config, logger, shutdownNotifier); + return factory.generateContext(); + }); + + executor.shutdownNow(); + + SolverContext context = result.get(); + FormulaManager mgr = context.getFormulaManager(); + + BooleanFormulaManager bmgr = mgr.getBooleanFormulaManager(); + IntegerFormulaManager imgr = mgr.getIntegerFormulaManager(); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + BooleanFormula formula = gen.generate(8); // CVC5 throws an exception here + + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } + } + + @Test + public void nonlocalFormulaTest() throws InterruptedException, SolverException, + ExecutionException { + requireIntegers(); + + /* FIXME: Exception for CVC5 (related to #310?) + Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null object + */ + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); + + ExecutorService executor = Executors.newSingleThreadExecutor(); + Future result = executor.submit(() -> { + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + return gen.generate(8); + }); + + BooleanFormula formula = result.get(); + executor.shutdownNow(); + + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } + } + + @Test + public void nonlocalProverTest() throws InterruptedException, ExecutionException { + requireIntegers(); + + /* FIXME: Exception for CVC5 + io.github.cvc5.CVC5ApiException: + Given term is not associated with the node manager of this solver + */ + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + BooleanFormula formula = gen.generate(8); + + ExecutorService executor = Executors.newSingleThreadExecutor(); + Future result = executor.submit( + () -> { + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); // CVC5 throws an exception here + return prover.isUnsat(); + } + }); + + Boolean isUnsat = result.get(); + executor.shutdownNow(); + + assert(isUnsat).equals(true); + } +} From 65e4c32fb9c72da8e99b978357da1315b85b8767 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 10 Dec 2023 20:42:16 +0100 Subject: [PATCH 02/46] Fix build issues. --- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index fcb1636e46..d09ff6f71e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -69,8 +69,9 @@ public void allLocalTest() throws InterruptedException, SolverException { ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = executor.submit(() -> { + Configuration config; try { - Configuration config = Configuration.builder() + config = Configuration.builder() .setOption("solver.solver", solverToUse().toString()) .build(); } catch (InvalidConfigurationException e) { @@ -150,6 +151,6 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException Boolean isUnsat = result.get(); executor.shutdownNow(); - assert(isUnsat).equals(true); + assert isUnsat.equals(true); } } From 5e1f046d1bade0f3c414f60e5049302416d3ca39 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 10 Dec 2023 21:38:13 +0100 Subject: [PATCH 03/46] Fixed checkstyle errors. --- .../java_smt/test/SolverThreadLocalTest.java | 79 ++++++++++--------- 1 file changed, 43 insertions(+), 36 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index d09ff6f71e..70cdc32c2b 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -57,8 +57,8 @@ public void allLocalTest() throws InterruptedException, SolverException { } } - @Test public void nonlocalContext() throws ExecutionException, InterruptedException, - SolverException { + @Test + public void nonlocalContext() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); /* FIXME: Exception for CVC5 (related to #310?) @@ -68,42 +68,46 @@ public void allLocalTest() throws InterruptedException, SolverException { assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); ExecutorService executor = Executors.newSingleThreadExecutor(); - Future result = executor.submit(() -> { - Configuration config; - try { - config = Configuration.builder() - .setOption("solver.solver", solverToUse().toString()) - .build(); - } catch (InvalidConfigurationException e) { - throw new RuntimeException(e); - } - LogManager logger = LogManager.createTestLogManager(); - ShutdownNotifier shutdownNotifier = ShutdownManager.create().getNotifier(); - - SolverContextFactory factory = new SolverContextFactory(config, logger, shutdownNotifier); - return factory.generateContext(); - }); + Future result = + executor.submit( + () -> { + try { + Configuration newConfig = + Configuration.builder() + .setOption("solver.solver", solverToUse().toString()) + .build(); + + LogManager newLogger = LogManager.createTestLogManager(); + ShutdownNotifier newShutdownNotifier = ShutdownManager.create().getNotifier(); + + SolverContextFactory newFactory = + new SolverContextFactory(newConfig, newLogger, newShutdownNotifier); + return factory.generateContext(); + } catch (InvalidConfigurationException e) { + throw new RuntimeException(e); + } + }); executor.shutdownNow(); - SolverContext context = result.get(); - FormulaManager mgr = context.getFormulaManager(); + SolverContext newContext = result.get(); + FormulaManager newMgr = context.getFormulaManager(); - BooleanFormulaManager bmgr = mgr.getBooleanFormulaManager(); - IntegerFormulaManager imgr = mgr.getIntegerFormulaManager(); + BooleanFormulaManager newBmgr = newMgr.getBooleanFormulaManager(); + IntegerFormulaManager newImgr = newMgr.getIntegerFormulaManager(); - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(newImgr, newBmgr); BooleanFormula formula = gen.generate(8); // CVC5 throws an exception here - try (BasicProverEnvironment prover = context.newProverEnvironment()) { + try (BasicProverEnvironment prover = newContext.newProverEnvironment()) { prover.push(formula); assertThat(prover).isUnsatisfiable(); } } @Test - public void nonlocalFormulaTest() throws InterruptedException, SolverException, - ExecutionException { + public void nonlocalFormulaTest() + throws InterruptedException, SolverException, ExecutionException { requireIntegers(); /* FIXME: Exception for CVC5 (related to #310?) @@ -112,10 +116,12 @@ public void nonlocalFormulaTest() throws InterruptedException, SolverException, assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); ExecutorService executor = Executors.newSingleThreadExecutor(); - Future result = executor.submit(() -> { - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - return gen.generate(8); - }); + Future result = + executor.submit( + () -> { + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + return gen.generate(8); + }); BooleanFormula formula = result.get(); executor.shutdownNow(); @@ -140,13 +146,14 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException BooleanFormula formula = gen.generate(8); ExecutorService executor = Executors.newSingleThreadExecutor(); - Future result = executor.submit( - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push(formula); // CVC5 throws an exception here - return prover.isUnsat(); - } - }); + Future result = + executor.submit( + () -> { + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); // CVC5 throws an exception here + return prover.isUnsat(); + } + }); Boolean isUnsat = result.get(); executor.shutdownNow(); From fb3d922d4583d4034d9d54b75fa6cc8ac98e2094 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 10 Dec 2023 21:52:42 +0100 Subject: [PATCH 04/46] Fixed license header. --- .../java_smt/test/SolverThreadLocalTest.java | 26 +++++-------------- 1 file changed, 7 insertions(+), 19 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 70cdc32c2b..3acf7d33d1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -1,22 +1,10 @@ -/* - * JavaSMT is an API wrapper for a collection of SMT solvers. - * This file is part of JavaSMT. - * - * Copyright (C) 2007-2016 Dirk Beyer - * All rights reserved. - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2023 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 package org.sosy_lab.java_smt.test; From f02f9ad4b2e3bb3a3fba98f1c35ce244d89b06f9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 10 Dec 2023 22:01:24 +0100 Subject: [PATCH 05/46] Fixed nonlocalContext test in SolverThreadLocalTest. --- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 3acf7d33d1..0a3cce1c0e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -79,7 +79,7 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S executor.shutdownNow(); SolverContext newContext = result.get(); - FormulaManager newMgr = context.getFormulaManager(); + FormulaManager newMgr = newContext.getFormulaManager(); BooleanFormulaManager newBmgr = newMgr.getBooleanFormulaManager(); IntegerFormulaManager newImgr = newMgr.getIntegerFormulaManager(); From 202722b94c042a2d9e948af11755e7daba035d5d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 10 Dec 2023 22:03:08 +0100 Subject: [PATCH 06/46] Fixed bug in nonlocalContext test. --- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 0a3cce1c0e..1aacdaa5d0 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -70,7 +70,7 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S SolverContextFactory newFactory = new SolverContextFactory(newConfig, newLogger, newShutdownNotifier); - return factory.generateContext(); + return newFactory.generateContext(); } catch (InvalidConfigurationException e) { throw new RuntimeException(e); } From 01c3ce4c461ea2d5f72936f5d53c535d508ecc5d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 10 Dec 2023 22:04:54 +0100 Subject: [PATCH 07/46] Make sure new context gets closed in SolverThreadLocal.nonlocalContext. --- .../java_smt/test/SolverThreadLocalTest.java | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 1aacdaa5d0..60820b152a 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -78,18 +78,19 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S executor.shutdownNow(); - SolverContext newContext = result.get(); - FormulaManager newMgr = newContext.getFormulaManager(); + try (SolverContext newContext = result.get()) { + FormulaManager newMgr = newContext.getFormulaManager(); - BooleanFormulaManager newBmgr = newMgr.getBooleanFormulaManager(); - IntegerFormulaManager newImgr = newMgr.getIntegerFormulaManager(); + BooleanFormulaManager newBmgr = newMgr.getBooleanFormulaManager(); + IntegerFormulaManager newImgr = newMgr.getIntegerFormulaManager(); - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(newImgr, newBmgr); - BooleanFormula formula = gen.generate(8); // CVC5 throws an exception here + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(newImgr, newBmgr); + BooleanFormula formula = gen.generate(8); // CVC5 throws an exception here - try (BasicProverEnvironment prover = newContext.newProverEnvironment()) { - prover.push(formula); - assertThat(prover).isUnsatisfiable(); + try (BasicProverEnvironment prover = newContext.newProverEnvironment()) { + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } } } From 4003c34b4489e4160b1b4c2938c7a2e13e3465e6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 14 Dec 2023 18:22:01 +0100 Subject: [PATCH 08/46] Added assertion to check if ShutdownNotifer was actually triggered when MathSat returns a "user-requested termination" error. --- .../solvers/mathsat5/Mathsat5AbstractProver.java | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index ec8cf34116..b7620781e5 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -39,6 +39,7 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; +import java.util.Objects; import java.util.Optional; import java.util.Set; import org.sosy_lab.common.ShutdownNotifier; @@ -100,7 +101,19 @@ private long buildConfig(Set opts) { @Override public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); - return !msat_check_sat(curEnv); + boolean result; + try { + result = !msat_check_sat(curEnv); + } + catch (IllegalStateException pE) { + if (Objects.equals( + pE.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { + assert shutdownNotifier.shouldShutdown(); + throw new InterruptedException(); + } + throw pE; + } + return result; } @Override From 6e356cbd7cd324c19eb8d29c193a4929188fe779 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 14 Dec 2023 18:32:17 +0100 Subject: [PATCH 09/46] Suppress resource warnings when using Executors.newSingleThreadExecutor. --- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 60820b152a..5ff0f33bbc 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -45,6 +45,7 @@ public void allLocalTest() throws InterruptedException, SolverException { } } + @SuppressWarnings("resource") @Test public void nonlocalContext() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); @@ -94,6 +95,8 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S } } + + @SuppressWarnings("resource") @Test public void nonlocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { @@ -121,6 +124,7 @@ public void nonlocalFormulaTest() } } + @SuppressWarnings("resource") @Test public void nonlocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); From c8c7712f1f571c947301ea630f4909c0f8172860 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 14 Dec 2023 18:53:46 +0100 Subject: [PATCH 10/46] Rewrote termination check for MathSAT to address the failed assertion from 4003c34b4489e4160b1b4c2938c7a2e13e3465e6. --- lib/ivy.xml | 2 +- ...osy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c | 7 +------ .../java_smt/solvers/mathsat5/Mathsat5SolverContext.java | 6 +----- 3 files changed, 3 insertions(+), 12 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 701c0cf037..4d2c401cb5 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -158,7 +158,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c index 30831f2a1b..ca912ab062 100644 --- a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c +++ b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c @@ -74,12 +74,7 @@ static int call_java_termination_callback(void *user_data) { } jboolean result = (*jenv)->CallBooleanMethod(jenv, helper->obj, helper->callback_method); - - if ((*jenv)->ExceptionCheck(jenv)) { - return 1; - } - - return result; + return result; } /* diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 6c356e10cf..39095a9161 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -122,11 +122,7 @@ private Mathsat5SolverContext( this.shutdownNotifier = shutdownNotifier; this.creator = creator; - terminationTest = - () -> { - shutdownNotifier.shutdownIfNecessary(); - return false; - }; + terminationTest = shutdownNotifier::shouldShutdown; } private static void logLicenseInfo(LogManager logger) { From 3196f7f676769bc2ee65ba3a88a2b20e731fc78a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 14 Dec 2023 18:55:34 +0100 Subject: [PATCH 11/46] Fixed formating --- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 3 +-- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 1 - 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index b7620781e5..224d8516d8 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -104,8 +104,7 @@ public boolean isUnsat() throws InterruptedException, SolverException { boolean result; try { result = !msat_check_sat(curEnv); - } - catch (IllegalStateException pE) { + } catch (IllegalStateException pE) { if (Objects.equals( pE.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { assert shutdownNotifier.shouldShutdown(); diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 5ff0f33bbc..d5a5a4f2fc 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -95,7 +95,6 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S } } - @SuppressWarnings("resource") @Test public void nonlocalFormulaTest() From 9e2abee261b1cfe0af14deb7e8b1231e225bb5cd Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 14 Dec 2023 23:11:52 +0100 Subject: [PATCH 12/46] Added tests for interpolation to SolverThreadLocalTest. This includes a test for bug #339 in MathSAT. --- .../java_smt/test/SolverThreadLocalTest.java | 189 +++++++++++++++--- 1 file changed, 162 insertions(+), 27 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index d5a5a4f2fc..c91734120d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -8,13 +8,14 @@ package org.sosy_lab.java_smt.test; -import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; +import java.util.List; import java.util.concurrent.ExecutionException; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; import java.util.concurrent.Future; +import java.util.concurrent.TimeUnit; import org.junit.Test; import org.sosy_lab.common.ShutdownManager; import org.sosy_lab.common.ShutdownNotifier; @@ -22,14 +23,15 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory; -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.BooleanFormulaManager; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class SolverThreadLocalTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @Test @@ -50,12 +52,6 @@ public void allLocalTest() throws InterruptedException, SolverException { public void nonlocalContext() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); - /* FIXME: Exception for CVC5 (related to #310?) - io.github.cvc5.CVC5ApiException: - Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null object - */ - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = executor.submit( @@ -77,8 +73,6 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S } }); - executor.shutdownNow(); - try (SolverContext newContext = result.get()) { FormulaManager newMgr = newContext.getFormulaManager(); @@ -86,7 +80,16 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S IntegerFormulaManager newImgr = newMgr.getIntegerFormulaManager(); HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(newImgr, newBmgr); - BooleanFormula formula = gen.generate(8); // CVC5 throws an exception here + + // FIXME: Exception for CVC5 (related to bug #310?) + // io.github.cvc5.CVC5ApiException: + // Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null object + // at io.github.cvc5.Sort.getKind + // (Native Method) + // at io.github.cvc5.Sort.getKind + // (Sort.java:93) + // at .. + BooleanFormula formula = gen.generate(8); try (BasicProverEnvironment prover = newContext.newProverEnvironment()) { prover.push(formula); @@ -101,21 +104,25 @@ public void nonlocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); - /* FIXME: Exception for CVC5 (related to #310?) - Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null object - */ - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = executor.submit( () -> { HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + + // FIXME: Exception for CVC5 (related to bug #310?) + // io.github.cvc5.CVC5ApiException: + // Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null + // object + // at io.github.cvc5.Sort.getKind + // (Native Method) + // at io.github.cvc5.Sort.getKind + // (Sort.java:93) + // at .. return gen.generate(8); }); BooleanFormula formula = result.get(); - executor.shutdownNow(); try (BasicProverEnvironment prover = context.newProverEnvironment()) { prover.push(formula); @@ -128,12 +135,6 @@ public void nonlocalFormulaTest() public void nonlocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); - /* FIXME: Exception for CVC5 - io.github.cvc5.CVC5ApiException: - Given term is not associated with the node manager of this solver - */ - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); BooleanFormula formula = gen.generate(8); @@ -142,14 +143,148 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException executor.submit( () -> { try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push(formula); // CVC5 throws an exception here + // FIXME: Exception for CVC5 + // io.github.cvc5.CVC5ApiException: + // Given term is not associated with the node manager of this solver + // at io.github.cvc5.Solver.assertFormula + // (Native Method) + // at io.github.cvc5.Solver.assertFormula + // (Solver.java:1455) + // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.addConstraintImpl + // (CVC5AbstractProver.java:114) + // at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint + // (AbstractProver.java:108) + // at .. + prover.push(formula); + return prover.isUnsat(); } }); - Boolean isUnsat = result.get(); - executor.shutdownNow(); + assert result.get(); + } + + @Override + protected Logics logicToUse() { + return Logics.QF_LIA; + } + + private void checkInterpolant( + BooleanFormula formulaA, BooleanFormula formulaB, BooleanFormula itp) + throws SolverException, InterruptedException { + assertThatFormula(formulaA).implies(itp); + assertThatFormula(bmgr.and(itp, formulaB)).implies(bmgr.makeBoolean(false)); + } + + @SuppressWarnings({"unchecked", "resource"}) + @Test + public void localInterpolationTest() throws InterruptedException, SolverException { + requireIntegers(); + requireInterpolation(); + + BooleanFormula f1 = imgr.lessThan(imgr.makeVariable("A"), imgr.makeVariable("B")); + BooleanFormula f2 = imgr.lessThan(imgr.makeVariable("B"), imgr.makeVariable("A")); + + try (InterpolatingProverEnvironment prover = + (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation()) { + prover.push(f1); + T id2 = prover.push(f2); + + assertThat(prover).isUnsatisfiable(); + + BooleanFormula itp = prover.getInterpolant(List.of(id2)); + checkInterpolant(f2, f1, itp); + + prover.pop(); + prover.push(itp); - assert isUnsat.equals(true); + assertThat(prover).isUnsatisfiable(); + } + } + + @SuppressWarnings({"unchecked", "resource"}) + @Test + public void nonlocalInterpolationTest() throws InterruptedException, ExecutionException { + requireIntegers(); + requireInterpolation(); + + ExecutorService executor = Executors.newFixedThreadPool(5); + + BooleanFormula f1 = imgr.lessThan(imgr.makeVariable("A"), imgr.makeVariable("B")); + BooleanFormula f2 = imgr.lessThan(imgr.makeVariable("B"), imgr.makeVariable("A")); + + try (InterpolatingProverEnvironment prover = + (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation()) { + T id1 = prover.push(f1); + + Future task1 = executor.submit( + () -> { + try { + // FIXME: Exception for CVC5 + // java.lang.IllegalStateException: + // You tried to use push() on an CVC5 assertion stack illegally. + // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl + // (CVC5AbstractProver.java:89) + // at org.sosy_lab.java_smt.basicimpl.AbstractProver.push + // (AbstractProver.java:88) + // at .. + prover.push(f2); + + // FIXME: Exception for MathSAT (bug #339) + // java.lang.StackOverflowError + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve + // (Native Method) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat + // (Mathsat5NativeApi.java:156) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat + // (Mathsat5AbstractProver.java:106) + // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable + // (ProverEnvironmentSubject.java:67) + // at .. + assertThat(prover).isUnsatisfiable(); + + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); + + assert task1.get() == null; + + Future itp = + executor.submit( + () -> { + BooleanFormula interpol = prover.getInterpolant(List.of(id1)); + Future task2 = + executor.submit( + () -> { + try { + checkInterpolant(f1, f2, interpol); + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); + assert task2.get() == null; + return interpol; + }); + + executor.awaitTermination(100, TimeUnit.MILLISECONDS); + prover.pop(); + + Future task3 = executor.submit( + () -> { + try { + prover.pop(); + + prover.push(itp.get()); + prover.push(f2); + + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException | ExecutionException pE) { + throw new RuntimeException(pE); + } + }); + + assert task3.get() == null; + } } } From 88711559ea2c3d226595f6ed2a72d7864f24767d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 00:29:35 +0100 Subject: [PATCH 13/46] Simplified nonLocalProverTest --- .../sosy_lab/java_smt/test/SolverThreadLocalTest.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index c91734120d..75977f01d9 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -139,7 +139,7 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException BooleanFormula formula = gen.generate(8); ExecutorService executor = Executors.newSingleThreadExecutor(); - Future result = + Future task = executor.submit( () -> { try (BasicProverEnvironment prover = context.newProverEnvironment()) { @@ -156,12 +156,13 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException // (AbstractProver.java:108) // at .. prover.push(formula); - - return prover.isUnsat(); + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); } }); - assert result.get(); + assert task.get() == null; } @Override From d78b8f43bae377d6407f14a1de764068c9154913 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 00:31:37 +0100 Subject: [PATCH 14/46] Added a minimal test case for bug #339. --- .../sosy_lab/java_smt/test/Bug339Test.java | 76 +++++++++++++++++++ 1 file changed, 76 insertions(+) create mode 100644 src/org/sosy_lab/java_smt/test/Bug339Test.java diff --git a/src/org/sosy_lab/java_smt/test/Bug339Test.java b/src/org/sosy_lab/java_smt/test/Bug339Test.java new file mode 100644 index 0000000000..87f9506580 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/Bug339Test.java @@ -0,0 +1,76 @@ +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.TruthJUnit.assume; +import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; + +import java.util.concurrent.ExecutionException; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; +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.SolverException; + +public class Bug339Test extends SolverBasedTest0.ParameterizedSolverBasedTest0 { + private final ExecutorService executor = Executors.newSingleThreadExecutor(); + + @Test + public void brokenTest() throws InterruptedException, ExecutionException { + assume().that(solverToUse()).isEqualTo(Solvers.MATHSAT5); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + BooleanFormula formula = gen.generate(8); + + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); + + Future task1 = + executor.submit( + () -> { + try { + // FIXME: Exception for MathSAT (bug #339) + // java.lang.StackOverflowError + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve + // (Native Method) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat + // (Mathsat5NativeApi.java:156) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat + // (Mathsat5AbstractProver.java:106) + // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable + // (ProverEnvironmentSubject.java:67) + // at .. + assertThat(prover).isUnsatisfiable(); + + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); + + assert task1.get() == null; + } + } + + @Test + public void fixedTest() throws InterruptedException, ExecutionException { + // Create the ProverEnvironment on the thread that uses it + assume().that(solverToUse()).isEqualTo(Solvers.MATHSAT5); + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + BooleanFormula formula = gen.generate(8); + + Future task1 = + executor.submit( + () -> { + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); + + assert task1.get() == null; + } +} From 9197ed1f849b630dab1bb746fa8bdcb57d1bbe19 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 03:48:01 +0100 Subject: [PATCH 15/46] Added a native version of the testcase for #339. --- .../mathsat5/Mathsat5NativeApiTest.java | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index d9021f64cd..291ac8dd6a 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -13,6 +13,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_config; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_env; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_shared_env; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_arity; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_name; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_config; @@ -26,10 +27,12 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_rational_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_enum_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_integer_type; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_and; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_asin; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_exp; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_leq; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_log; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_not; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_number; @@ -45,12 +48,17 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_pop_backtrack_point; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_push_backtrack_point; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_pi; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_repr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_equals; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.Future; import org.junit.AssumptionViolatedException; import org.junit.Before; import org.junit.BeforeClass; @@ -526,4 +534,49 @@ public void enumTypeTest() throws SolverException, InterruptedException { assertThat(msat_check_sat(env)).isFalse(); msat_pop_backtrack_point(env); } + + private final ExecutorService executor = Executors.newSingleThreadExecutor(); + + + @SuppressWarnings("unused") + private long createSharedEnv(long sibling) { + long cfg = msat_create_config(); + msat_set_option_checked(cfg, "dpll.ghost_filtering", "true"); + msat_set_option_checked(cfg, "theory.la.split_rat_eq", "false"); + + long prover = msat_create_shared_env(cfg, sibling); + msat_destroy_config(cfg); + + // FIXME: Bug #339 is caused by this line. Removing it will fix the test. + long hook = msat_set_termination_callback(prover, () -> false); + + return prover; + } + + private long makeLt(long e, long t1, long t2) { + return msat_make_not(e, msat_make_leq(e, t2, t1)); + } + + @Test + public void bug339Test() throws ExecutionException, InterruptedException { + long integerType = msat_get_integer_type(env); + + long varA = msat_make_variable(env, "A", integerType); + long varB = msat_make_variable(env, "B", integerType); + + long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA)); + + long prover = createSharedEnv(this.env); + msat_assert_formula(prover, formula); + + Future task1 = executor.submit(() -> { + try { + assertThat(msat_check_sat(prover)).isFalse(); + } catch (InterruptedException | SolverException pE) { + throw new RuntimeException(pE); + } + }); + + assert task1.get() == null; + } } From 74f4a255b3ea94ac859fc691c7acd897eb741dd9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 03:50:38 +0100 Subject: [PATCH 16/46] Fixed formating --- .../mathsat5/Mathsat5NativeApiTest.java | 17 ++-- .../sosy_lab/java_smt/test/Bug339Test.java | 2 +- .../java_smt/test/SolverThreadLocalTest.java | 84 ++++++++++--------- 3 files changed, 53 insertions(+), 50 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index 291ac8dd6a..a5f4118f69 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -537,7 +537,6 @@ public void enumTypeTest() throws SolverException, InterruptedException { private final ExecutorService executor = Executors.newSingleThreadExecutor(); - @SuppressWarnings("unused") private long createSharedEnv(long sibling) { long cfg = msat_create_config(); @@ -569,13 +568,15 @@ public void bug339Test() throws ExecutionException, InterruptedException { long prover = createSharedEnv(this.env); msat_assert_formula(prover, formula); - Future task1 = executor.submit(() -> { - try { - assertThat(msat_check_sat(prover)).isFalse(); - } catch (InterruptedException | SolverException pE) { - throw new RuntimeException(pE); - } - }); + Future task1 = + executor.submit( + () -> { + try { + assertThat(msat_check_sat(prover)).isFalse(); + } catch (InterruptedException | SolverException pE) { + throw new RuntimeException(pE); + } + }); assert task1.get() == null; } diff --git a/src/org/sosy_lab/java_smt/test/Bug339Test.java b/src/org/sosy_lab/java_smt/test/Bug339Test.java index 87f9506580..3c6f65c1f5 100644 --- a/src/org/sosy_lab/java_smt/test/Bug339Test.java +++ b/src/org/sosy_lab/java_smt/test/Bug339Test.java @@ -71,6 +71,6 @@ public void fixedTest() throws InterruptedException, ExecutionException { } }); - assert task1.get() == null; + assert task1.get() == null; } } diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 75977f01d9..9f6606dbce 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -218,36 +218,37 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation()) { T id1 = prover.push(f1); - Future task1 = executor.submit( - () -> { - try { - // FIXME: Exception for CVC5 - // java.lang.IllegalStateException: - // You tried to use push() on an CVC5 assertion stack illegally. - // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl - // (CVC5AbstractProver.java:89) - // at org.sosy_lab.java_smt.basicimpl.AbstractProver.push - // (AbstractProver.java:88) - // at .. - prover.push(f2); - - // FIXME: Exception for MathSAT (bug #339) - // java.lang.StackOverflowError - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve - // (Native Method) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat - // (Mathsat5NativeApi.java:156) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat - // (Mathsat5AbstractProver.java:106) - // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable - // (ProverEnvironmentSubject.java:67) - // at .. - assertThat(prover).isUnsatisfiable(); - - } catch (SolverException | InterruptedException pE) { - throw new RuntimeException(pE); - } - }); + Future task1 = + executor.submit( + () -> { + try { + // FIXME: Exception for CVC5 + // java.lang.IllegalStateException: + // You tried to use push() on an CVC5 assertion stack illegally. + // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl + // (CVC5AbstractProver.java:89) + // at org.sosy_lab.java_smt.basicimpl.AbstractProver.push + // (AbstractProver.java:88) + // at .. + prover.push(f2); + + // FIXME: Exception for MathSAT (bug #339) + // java.lang.StackOverflowError + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve + // (Native Method) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat + // (Mathsat5NativeApi.java:156) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat + // (Mathsat5AbstractProver.java:106) + // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable + // (ProverEnvironmentSubject.java:67) + // at .. + assertThat(prover).isUnsatisfiable(); + + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); assert task1.get() == null; @@ -271,19 +272,20 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi executor.awaitTermination(100, TimeUnit.MILLISECONDS); prover.pop(); - Future task3 = executor.submit( - () -> { - try { - prover.pop(); + Future task3 = + executor.submit( + () -> { + try { + prover.pop(); - prover.push(itp.get()); - prover.push(f2); + prover.push(itp.get()); + prover.push(f2); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException | ExecutionException pE) { - throw new RuntimeException(pE); - } - }); + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException | ExecutionException pE) { + throw new RuntimeException(pE); + } + }); assert task3.get() == null; } From bd81f544a54bec7f9b2a2e8fa8684aed6c524005 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 04:10:23 +0100 Subject: [PATCH 17/46] Added another version of the native test for #339 that fixes the bug. --- .../mathsat5/Mathsat5NativeApiTest.java | 41 ++++++++++++++++--- 1 file changed, 36 insertions(+), 5 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index a5f4118f69..ecd179bdbb 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -537,7 +537,7 @@ public void enumTypeTest() throws SolverException, InterruptedException { private final ExecutorService executor = Executors.newSingleThreadExecutor(); - @SuppressWarnings("unused") + private long createSharedEnv(long sibling) { long cfg = msat_create_config(); msat_set_option_checked(cfg, "dpll.ghost_filtering", "true"); @@ -546,9 +546,6 @@ private long createSharedEnv(long sibling) { long prover = msat_create_shared_env(cfg, sibling); msat_destroy_config(cfg); - // FIXME: Bug #339 is caused by this line. Removing it will fix the test. - long hook = msat_set_termination_callback(prover, () -> false); - return prover; } @@ -556,22 +553,56 @@ private long makeLt(long e, long t1, long t2) { return msat_make_not(e, msat_make_leq(e, t2, t1)); } + @SuppressWarnings("unused") @Test - public void bug339Test() throws ExecutionException, InterruptedException { + public void bug339BrokenTest() throws ExecutionException, InterruptedException { long integerType = msat_get_integer_type(env); long varA = msat_make_variable(env, "A", integerType); long varB = msat_make_variable(env, "B", integerType); long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA)); + long prover = createSharedEnv(this.env); + + // FIXME: Bug #339 is caused by this line. Removing it will fix the test. + long hook = msat_set_termination_callback(prover, () -> false); + + msat_assert_formula(prover, formula); + Future task1 = + executor.submit( + () -> { + try { + assertThat(msat_check_sat(prover)).isFalse(); + } catch (InterruptedException | SolverException pE) { + throw new RuntimeException(pE); + } + }); + + assert task1.get() == null; + } + + @SuppressWarnings("unused") + @Test + public void bug339FixedTest() throws ExecutionException, InterruptedException { + long integerType = msat_get_integer_type(env); + + long varA = msat_make_variable(env, "A", integerType); + long varB = msat_make_variable(env, "B", integerType); + + long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA)); long prover = createSharedEnv(this.env); + msat_assert_formula(prover, formula); Future task1 = executor.submit( () -> { try { + // FIXME: Bug #339 is not triggered if we add the callback on the thread that + // will do the calculation + long hook = msat_set_termination_callback(prover, () -> false); + assertThat(msat_check_sat(prover)).isFalse(); } catch (InterruptedException | SolverException pE) { throw new RuntimeException(pE); From 4464c90b8f07d37bae8c47e90b8b767910be44c5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 07:18:01 +0100 Subject: [PATCH 18/46] Bugfix for #339 --- .../mathsat5/Mathsat5AbstractProver.java | 45 ++++++++++++++----- .../mathsat5/Mathsat5InterpolatingProver.java | 2 +- .../mathsat5/Mathsat5NativeApiTest.java | 1 - 3 files changed, 35 insertions(+), 13 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 224d8516d8..6abf971c3a 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -30,6 +30,7 @@ import com.google.common.base.Preconditions; import com.google.common.base.Splitter; +import com.google.common.base.Throwables; import com.google.common.collect.ImmutableMap; import com.google.common.collect.Lists; import com.google.common.primitives.Longs; @@ -42,6 +43,7 @@ import java.util.Objects; import java.util.Optional; import java.util.Set; +import java.util.concurrent.Callable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; @@ -58,7 +60,6 @@ abstract class Mathsat5AbstractProver extends AbstractProver { protected final Mathsat5SolverContext context; protected final long curEnv; private final long curConfig; - private final long terminationTest; protected final Mathsat5FormulaCreator creator; private final ShutdownNotifier shutdownNotifier; @@ -72,7 +73,6 @@ protected Mathsat5AbstractProver( creator = pCreator; curConfig = buildConfig(pOptions); curEnv = context.createEnvironment(curConfig); - terminationTest = context.addTerminationTest(curEnv); shutdownNotifier = pShutdownNotifier; } @@ -98,29 +98,53 @@ private long buildConfig(Set opts) { /** add needed options into the given map. */ protected abstract void createConfig(Map pConfig); + private T exec(Callable closure) throws SolverException { + long hook = context.addTerminationTest(curEnv); + T value = null; + try { + value = closure.call(); + } catch (Throwable t) { + Throwables.propagateIfPossible(t, IllegalStateException.class, SolverException.class); + } finally { + msat_free_termination_callback(hook); + } + return value; + } + @Override - public boolean isUnsat() throws InterruptedException, SolverException { + public synchronized boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); boolean result; try { - result = !msat_check_sat(curEnv); - } catch (IllegalStateException pE) { + result = exec(() -> !msat_check_sat(curEnv)); + } catch (IllegalStateException e) { if (Objects.equals( - pE.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { + e.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { assert shutdownNotifier.shouldShutdown(); throw new InterruptedException(); } - throw pE; + throw e; } return result; } @Override - public boolean isUnsatWithAssumptions(Collection pAssumptions) + public synchronized boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); checkForLiterals(pAssumptions); - return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); + boolean result; + try { + result = exec(() -> !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions))); + } catch (IllegalStateException e) { + if (Objects.equals( + e.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { + assert shutdownNotifier.shouldShutdown(); + throw new InterruptedException(); + } + throw e; + } + return result; } private void checkForLiterals(Collection formulas) { @@ -226,7 +250,6 @@ public ImmutableMap getStatistics() { public void close() { if (!closed) { msat_destroy_env(curEnv); - msat_free_termination_callback(terminationTest); msat_destroy_config(curConfig); } super.close(); @@ -237,7 +260,7 @@ protected boolean isClosed() { } @Override - public T allSat(AllSatCallback callback, List important) + public synchronized T allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { Preconditions.checkState(!closed); checkGenerateAllSat(); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java index ea1fd42e2e..40ebc43196 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java @@ -152,7 +152,7 @@ public List getTreeInterpolants( } @Override - public T allSat(AllSatCallback callback, List important) { + public synchronized T allSat(AllSatCallback callback, List important) { // TODO how can we support allsat in MathSat5-interpolation-prover? // error: "allsat is not compatible wwith proof generation" throw new UnsupportedOperationException( diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index ecd179bdbb..9623028a20 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -537,7 +537,6 @@ public void enumTypeTest() throws SolverException, InterruptedException { private final ExecutorService executor = Executors.newSingleThreadExecutor(); - private long createSharedEnv(long sibling) { long cfg = msat_create_config(); msat_set_option_checked(cfg, "dpll.ghost_filtering", "true"); From 7adc7be52a9a0e68748b141a276c914fd7e419b1 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 07:21:00 +0100 Subject: [PATCH 19/46] Revert "Rewrote termination check for MathSAT to address the failed assertion from 4003c34b4489e4160b1b4c2938c7a2e13e3465e6." This reverts commit c8c7712f1f571c947301ea630f4909c0f8172860. --- lib/ivy.xml | 2 +- ...osy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c | 7 ++++++- .../java_smt/solvers/mathsat5/Mathsat5SolverContext.java | 6 +++++- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 4d2c401cb5..701c0cf037 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -158,7 +158,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c index ca912ab062..30831f2a1b 100644 --- a/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c +++ b/lib/native/source/libmathsat5j/org_sosy_1lab_java_1smt_solvers_mathsat5_Mathsat5NativeApi.c @@ -74,7 +74,12 @@ static int call_java_termination_callback(void *user_data) { } jboolean result = (*jenv)->CallBooleanMethod(jenv, helper->obj, helper->callback_method); - return result; + + if ((*jenv)->ExceptionCheck(jenv)) { + return 1; + } + + return result; } /* diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 39095a9161..6c356e10cf 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -122,7 +122,11 @@ private Mathsat5SolverContext( this.shutdownNotifier = shutdownNotifier; this.creator = creator; - terminationTest = shutdownNotifier::shouldShutdown; + terminationTest = + () -> { + shutdownNotifier.shutdownIfNecessary(); + return false; + }; } private static void logLicenseInfo(LogManager logger) { From 9162b20c74ec5d263d85f4b63b8ceabb354fb868 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 07:36:00 +0100 Subject: [PATCH 20/46] Revert "Added assertion to check if ShutdownNotifer was actually triggered when MathSat returns a "user-requested termination" error." This reverts commit 4003c34b4489e4160b1b4c2938c7a2e13e3465e6. --- .../mathsat5/Mathsat5AbstractProver.java | 27 ++----------------- 1 file changed, 2 insertions(+), 25 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 6abf971c3a..c2113c6c08 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -40,7 +40,6 @@ import java.util.LinkedHashMap; import java.util.List; import java.util.Map; -import java.util.Objects; import java.util.Optional; import java.util.Set; import java.util.concurrent.Callable; @@ -114,18 +113,7 @@ private T exec(Callable closure) throws SolverException { @Override public synchronized boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); - boolean result; - try { - result = exec(() -> !msat_check_sat(curEnv)); - } catch (IllegalStateException e) { - if (Objects.equals( - e.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { - assert shutdownNotifier.shouldShutdown(); - throw new InterruptedException(); - } - throw e; - } - return result; + return exec(() -> !msat_check_sat(curEnv)); } @Override @@ -133,18 +121,7 @@ public synchronized boolean isUnsatWithAssumptions(Collection pA throws SolverException, InterruptedException { Preconditions.checkState(!closed); checkForLiterals(pAssumptions); - boolean result; - try { - result = exec(() -> !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions))); - } catch (IllegalStateException e) { - if (Objects.equals( - e.getMessage(), "msat_solve returned \"unknown\": user-requested termination")) { - assert shutdownNotifier.shouldShutdown(); - throw new InterruptedException(); - } - throw e; - } - return result; + return exec(() -> !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions))); } private void checkForLiterals(Collection formulas) { From c41df5c250a4f1aa84eab116672f039ad6908537 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 07:43:34 +0100 Subject: [PATCH 21/46] Disabled failing tests for CVC5 --- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 9f6606dbce..9e1b9a6d91 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import java.util.List; @@ -23,6 +24,7 @@ import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.common.log.LogManager; import org.sosy_lab.java_smt.SolverContextFactory; +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.BooleanFormulaManager; @@ -51,6 +53,7 @@ public void allLocalTest() throws InterruptedException, SolverException { @Test public void nonlocalContext() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = @@ -103,6 +106,7 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S public void nonlocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = @@ -134,6 +138,7 @@ public void nonlocalFormulaTest() @Test public void nonlocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); BooleanFormula formula = gen.generate(8); @@ -208,6 +213,7 @@ public void localInterpolationTest() throws InterruptedException, SolverExce public void nonlocalInterpolationTest() throws InterruptedException, ExecutionException { requireIntegers(); requireInterpolation(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); ExecutorService executor = Executors.newFixedThreadPool(5); From e7fda3d66f3d0bdf68d3a6fd3777290c0a14c0b1 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 07:48:03 +0100 Subject: [PATCH 22/46] Added copyright header to Bug339Test.java --- src/org/sosy_lab/java_smt/test/Bug339Test.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/Bug339Test.java b/src/org/sosy_lab/java_smt/test/Bug339Test.java index 3c6f65c1f5..e679e1e5ea 100644 --- a/src/org/sosy_lab/java_smt/test/Bug339Test.java +++ b/src/org/sosy_lab/java_smt/test/Bug339Test.java @@ -1,3 +1,11 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2023 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + package org.sosy_lab.java_smt.test; import static com.google.common.truth.TruthJUnit.assume; From 63f8a94bb58620609fe0b5a551d7507a53433c8b Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 08:00:16 +0100 Subject: [PATCH 23/46] Fixed annotation for bug330BrokenTest: we expect this to fail --- .../java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index 9623028a20..c77a805de1 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -553,7 +553,7 @@ private long makeLt(long e, long t1, long t2) { } @SuppressWarnings("unused") - @Test + @Test(expected = StackOverflowError.class) public void bug339BrokenTest() throws ExecutionException, InterruptedException { long integerType = msat_get_integer_type(env); From ea5b9e733b5afdfa9d33ba15c881719c9b675a4b Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 08:09:04 +0100 Subject: [PATCH 24/46] Applied refaster patch --- src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 9e1b9a6d91..4f8e8bde33 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -11,7 +11,7 @@ import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; -import java.util.List; +import com.google.common.collect.ImmutableList; import java.util.concurrent.ExecutionException; import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; @@ -198,7 +198,7 @@ public void localInterpolationTest() throws InterruptedException, SolverExce assertThat(prover).isUnsatisfiable(); - BooleanFormula itp = prover.getInterpolant(List.of(id2)); + BooleanFormula itp = prover.getInterpolant(ImmutableList.of(id2)); checkInterpolant(f2, f1, itp); prover.pop(); @@ -261,7 +261,7 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi Future itp = executor.submit( () -> { - BooleanFormula interpol = prover.getInterpolant(List.of(id1)); + BooleanFormula interpol = prover.getInterpolant(ImmutableList.of(id1)); Future task2 = executor.submit( () -> { From 0436959c6d625e993abb3ea94ba7e5c52a9e929a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 08:33:34 +0100 Subject: [PATCH 25/46] Progage InterruptedExceptionin Mathsat5AbstractProver.exec() to fix seceral failed tests in TimoutTest.java --- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index c2113c6c08..68e5717291 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -97,13 +97,14 @@ private long buildConfig(Set opts) { /** add needed options into the given map. */ protected abstract void createConfig(Map pConfig); - private T exec(Callable closure) throws SolverException { + private T exec(Callable closure) throws SolverException, InterruptedException { long hook = context.addTerminationTest(curEnv); T value = null; try { value = closure.call(); } catch (Throwable t) { Throwables.propagateIfPossible(t, IllegalStateException.class, SolverException.class); + Throwables.propagateIfPossible(t, InterruptedException.class); } finally { msat_free_termination_callback(hook); } From dc5ee89ef7656c2f19c4b372e71d6ed5ec3f1e44 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 16:51:15 +0100 Subject: [PATCH 26/46] Cleaned up SolverThreadLocalTest class --- .../java_smt/test/SolverThreadLocalTest.java | 88 +++++++++---------- 1 file changed, 44 insertions(+), 44 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java index 4f8e8bde33..7f1bf6c2a1 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java @@ -36,6 +36,8 @@ import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class SolverThreadLocalTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { + ExecutorService executor = Executors.newFixedThreadPool(2); + @Test public void allLocalTest() throws InterruptedException, SolverException { requireIntegers(); @@ -53,9 +55,9 @@ public void allLocalTest() throws InterruptedException, SolverException { @Test public void nonlocalContext() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = executor.submit( () -> { @@ -106,9 +108,9 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S public void nonlocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - ExecutorService executor = Executors.newSingleThreadExecutor(); Future result = executor.submit( () -> { @@ -134,47 +136,58 @@ public void nonlocalFormulaTest() } } - @SuppressWarnings("resource") @Test public void nonlocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); + assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); BooleanFormula formula = gen.generate(8); - ExecutorService executor = Executors.newSingleThreadExecutor(); - Future task = - executor.submit( - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - // FIXME: Exception for CVC5 - // io.github.cvc5.CVC5ApiException: - // Given term is not associated with the node manager of this solver - // at io.github.cvc5.Solver.assertFormula - // (Native Method) - // at io.github.cvc5.Solver.assertFormula - // (Solver.java:1455) - // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.addConstraintImpl - // (CVC5AbstractProver.java:114) - // at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint - // (AbstractProver.java:108) - // at .. - prover.push(formula); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException pE) { - throw new RuntimeException(pE); - } - }); + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + Future task = + executor.submit( + () -> { + try { + // FIXME: Exception for CVC5 + // io.github.cvc5.CVC5ApiException: + // Given term is not associated with the node manager of this solver + // at io.github.cvc5.Solver.assertFormula + // (Native Method) + // at io.github.cvc5.Solver.assertFormula + // (Solver.java:1455) + // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.addConstraintImpl + // (CVC5AbstractProver.java:114) + // at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint + // (AbstractProver.java:108) + // at .. + prover.push(formula); - assert task.get() == null; + // FIXME: Exception for MathSAT (bug #339) + // java.lang.StackOverflowError + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve + // (Native Method) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat + // (Mathsat5NativeApi.java:156) + // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat + // (Mathsat5AbstractProver.java:106) + // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable + // (ProverEnvironmentSubject.java:67) + // at .. + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); + assert task.get() == null; + } } @Override - protected Logics logicToUse() { - return Logics.QF_LIA; - } + protected Logics logicToUse() { return Logics.QF_LIA; } + // Make sure that the solver returned a valid interpolant for the two formulas private void checkInterpolant( BooleanFormula formulaA, BooleanFormula formulaB, BooleanFormula itp) throws SolverException, InterruptedException { @@ -213,9 +226,8 @@ public void localInterpolationTest() throws InterruptedException, SolverExce public void nonlocalInterpolationTest() throws InterruptedException, ExecutionException { requireIntegers(); requireInterpolation(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - ExecutorService executor = Executors.newFixedThreadPool(5); + 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")); @@ -237,18 +249,6 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi // (AbstractProver.java:88) // at .. prover.push(f2); - - // FIXME: Exception for MathSAT (bug #339) - // java.lang.StackOverflowError - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve - // (Native Method) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat - // (Mathsat5NativeApi.java:156) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat - // (Mathsat5AbstractProver.java:106) - // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable - // (ProverEnvironmentSubject.java:67) - // at .. assertThat(prover).isUnsatisfiable(); } catch (SolverException | InterruptedException pE) { From 1e0319b6a36c7d3c457843d1d2fa7fb7d4762c27 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 16:52:30 +0100 Subject: [PATCH 27/46] Renamed SolverThreadLocalTest class to SolverThreadLocalityTest --- ...SolverThreadLocalTest.java => SolverThreadLocalityTest.java} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename src/org/sosy_lab/java_smt/test/{SolverThreadLocalTest.java => SolverThreadLocalityTest.java} (99%) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java similarity index 99% rename from src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java rename to src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 7f1bf6c2a1..3d6ae6254e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -35,7 +35,7 @@ import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.solvers.opensmt.Logics; -public class SolverThreadLocalTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { +public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { ExecutorService executor = Executors.newFixedThreadPool(2); @Test From 0b3c2b828a4fd57fa8cbc4cc93f712cd050b4756 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 18:16:41 +0100 Subject: [PATCH 28/46] Some clean-up --- .../test/SolverThreadLocalityTest.java | 24 +++++-------------- 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 3d6ae6254e..0d0b0deead 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -18,12 +18,7 @@ import java.util.concurrent.Future; import java.util.concurrent.TimeUnit; import org.junit.Test; -import org.sosy_lab.common.ShutdownManager; -import org.sosy_lab.common.ShutdownNotifier; -import org.sosy_lab.common.configuration.Configuration; import org.sosy_lab.common.configuration.InvalidConfigurationException; -import org.sosy_lab.common.log.LogManager; -import org.sosy_lab.java_smt.SolverContextFactory; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -53,7 +48,8 @@ public void allLocalTest() throws InterruptedException, SolverException { @SuppressWarnings("resource") @Test - public void nonlocalContext() throws ExecutionException, InterruptedException, SolverException { + public void nonlocalContextTest() + throws ExecutionException, InterruptedException, SolverException { requireIntegers(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); @@ -62,17 +58,7 @@ public void nonlocalContext() throws ExecutionException, InterruptedException, S executor.submit( () -> { try { - Configuration newConfig = - Configuration.builder() - .setOption("solver.solver", solverToUse().toString()) - .build(); - - LogManager newLogger = LogManager.createTestLogManager(); - ShutdownNotifier newShutdownNotifier = ShutdownManager.create().getNotifier(); - - SolverContextFactory newFactory = - new SolverContextFactory(newConfig, newLogger, newShutdownNotifier); - return newFactory.generateContext(); + return factory.generateContext(); } catch (InvalidConfigurationException e) { throw new RuntimeException(e); } @@ -185,7 +171,9 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException } @Override - protected Logics logicToUse() { return Logics.QF_LIA; } + protected Logics logicToUse() { + return Logics.QF_LIA; + } // Make sure that the solver returned a valid interpolant for the two formulas private void checkInterpolant( From 80ede24a73d585d8dcb0dd00bea8a9c92bf83c2e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 18:18:36 +0100 Subject: [PATCH 29/46] Added one more test to SolverThreadLocalityTest that checks what happeneds when formulas are used outside of their context. --- .../test/SolverThreadLocalityTest.java | 52 +++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 0d0b0deead..8fa2bffa68 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -27,6 +27,7 @@ import org.sosy_lab.java_smt.api.IntegerFormulaManager; import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.solvers.opensmt.Logics; @@ -284,4 +285,55 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi assert task3.get() == null; } } + + @SuppressWarnings("resource") + @Test + public void wrongContextTest() throws InterruptedException, SolverException { + assume() + .that(solverToUse()) + .isNoneOf( + Solvers.OPENSMT, + Solvers.MATHSAT5, + Solvers.SMTINTERPOL, + Solvers.Z3, + Solvers.PRINCESS, + Solvers.BOOLECTOR); + + // 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. + // Right now we get: + // OpenSMT claims the formula is satisfiable: + // expected to be : unsatisfiable + // but was : org.sosy_lab.java_smt.solvers.opensmt.OpenSmtTheoremProver@10d59286 + // which is : satisfiable + // which has model: + // MathSAT5 thows an IllegalStateExpression: + // msat_solve returned "unknown": polarity information is meaningful only for terms of + // type Bool + // SMTInterpol thows an de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: + // Asserted terms created with incompatible theory + // Z3 throws an com.microsoft.z3.Z3Exception: + // invalid argument + // Princess throws an java.util.NoSuchElementException: + // key not found: i@15 + // Boolector crashes with a segfault: + // boolector_assert: argument 'exp' belongs to different Boolector instance + + HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); + + // Boolector does not support integer, so we have to use two different versions for this test. + BooleanFormula formula = + solverToUse() == Solvers.BOOLECTOR ? bmgr.makeFalse() : gen.generate(8); + + try (SolverContext newContext = factory.generateContext()) { + try (BasicProverEnvironment prover = + newContext.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + // Trying to add a formula from our global context to the newly created solver context. + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } + } catch (InvalidConfigurationException e) { + throw new RuntimeException(e); + } + } } From 36919ed212984c63cf02080ff19025f1379c0131 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 18:19:35 +0100 Subject: [PATCH 30/46] Removed native API test for bug339 as it has been fixed. --- .../mathsat5/Mathsat5NativeApiTest.java | 76 ------------------- 1 file changed, 76 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index c77a805de1..3997f0d108 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -534,80 +534,4 @@ public void enumTypeTest() throws SolverException, InterruptedException { assertThat(msat_check_sat(env)).isFalse(); msat_pop_backtrack_point(env); } - - private final ExecutorService executor = Executors.newSingleThreadExecutor(); - - private long createSharedEnv(long sibling) { - long cfg = msat_create_config(); - msat_set_option_checked(cfg, "dpll.ghost_filtering", "true"); - msat_set_option_checked(cfg, "theory.la.split_rat_eq", "false"); - - long prover = msat_create_shared_env(cfg, sibling); - msat_destroy_config(cfg); - - return prover; - } - - private long makeLt(long e, long t1, long t2) { - return msat_make_not(e, msat_make_leq(e, t2, t1)); - } - - @SuppressWarnings("unused") - @Test(expected = StackOverflowError.class) - public void bug339BrokenTest() throws ExecutionException, InterruptedException { - long integerType = msat_get_integer_type(env); - - long varA = msat_make_variable(env, "A", integerType); - long varB = msat_make_variable(env, "B", integerType); - - long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA)); - long prover = createSharedEnv(this.env); - - // FIXME: Bug #339 is caused by this line. Removing it will fix the test. - long hook = msat_set_termination_callback(prover, () -> false); - - msat_assert_formula(prover, formula); - - Future task1 = - executor.submit( - () -> { - try { - assertThat(msat_check_sat(prover)).isFalse(); - } catch (InterruptedException | SolverException pE) { - throw new RuntimeException(pE); - } - }); - - assert task1.get() == null; - } - - @SuppressWarnings("unused") - @Test - public void bug339FixedTest() throws ExecutionException, InterruptedException { - long integerType = msat_get_integer_type(env); - - long varA = msat_make_variable(env, "A", integerType); - long varB = msat_make_variable(env, "B", integerType); - - long formula = msat_make_and(env, makeLt(env, varA, varB), makeLt(env, varB, varA)); - long prover = createSharedEnv(this.env); - - msat_assert_formula(prover, formula); - - Future task1 = - executor.submit( - () -> { - try { - // FIXME: Bug #339 is not triggered if we add the callback on the thread that - // will do the calculation - long hook = msat_set_termination_callback(prover, () -> false); - - assertThat(msat_check_sat(prover)).isFalse(); - } catch (InterruptedException | SolverException pE) { - throw new RuntimeException(pE); - } - }); - - assert task1.get() == null; - } } From d1e85eb41f6eee285fae2b862f0c9a7385503c9a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 18:21:02 +0100 Subject: [PATCH 31/46] Removed JavaSMT test class for bug339 as it has been fixed. --- .../sosy_lab/java_smt/test/Bug339Test.java | 84 ------------------- 1 file changed, 84 deletions(-) delete mode 100644 src/org/sosy_lab/java_smt/test/Bug339Test.java diff --git a/src/org/sosy_lab/java_smt/test/Bug339Test.java b/src/org/sosy_lab/java_smt/test/Bug339Test.java deleted file mode 100644 index e679e1e5ea..0000000000 --- a/src/org/sosy_lab/java_smt/test/Bug339Test.java +++ /dev/null @@ -1,84 +0,0 @@ -// This file is part of JavaSMT, -// an API wrapper for a collection of SMT solvers: -// https://github.com/sosy-lab/java-smt -// -// SPDX-FileCopyrightText: 2023 Dirk Beyer -// -// SPDX-License-Identifier: Apache-2.0 - -package org.sosy_lab.java_smt.test; - -import static com.google.common.truth.TruthJUnit.assume; -import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; - -import java.util.concurrent.ExecutionException; -import java.util.concurrent.ExecutorService; -import java.util.concurrent.Executors; -import java.util.concurrent.Future; -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.SolverException; - -public class Bug339Test extends SolverBasedTest0.ParameterizedSolverBasedTest0 { - private final ExecutorService executor = Executors.newSingleThreadExecutor(); - - @Test - public void brokenTest() throws InterruptedException, ExecutionException { - assume().that(solverToUse()).isEqualTo(Solvers.MATHSAT5); - - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - BooleanFormula formula = gen.generate(8); - - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push(formula); - - Future task1 = - executor.submit( - () -> { - try { - // FIXME: Exception for MathSAT (bug #339) - // java.lang.StackOverflowError - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve - // (Native Method) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat - // (Mathsat5NativeApi.java:156) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat - // (Mathsat5AbstractProver.java:106) - // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable - // (ProverEnvironmentSubject.java:67) - // at .. - assertThat(prover).isUnsatisfiable(); - - } catch (SolverException | InterruptedException pE) { - throw new RuntimeException(pE); - } - }); - - assert task1.get() == null; - } - } - - @Test - public void fixedTest() throws InterruptedException, ExecutionException { - // Create the ProverEnvironment on the thread that uses it - assume().that(solverToUse()).isEqualTo(Solvers.MATHSAT5); - - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - BooleanFormula formula = gen.generate(8); - - Future task1 = - executor.submit( - () -> { - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - prover.push(formula); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException pE) { - throw new RuntimeException(pE); - } - }); - - assert task1.get() == null; - } -} From 389af9f1464666c45538205e07854f151f6f2ddf Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 18:23:11 +0100 Subject: [PATCH 32/46] Removed unused imports. --- .../java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java | 8 -------- 1 file changed, 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index 3997f0d108..d9021f64cd 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -13,7 +13,6 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_config; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_env; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_shared_env; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_arity; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_name; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_config; @@ -27,12 +26,10 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_rational_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_enum_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_is_integer_type; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_and; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_asin; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_exp; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_leq; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_log; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_not; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_number; @@ -48,17 +45,12 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_pop_backtrack_point; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_push_backtrack_point; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_type; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_pi; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_repr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_equals; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr; -import java.util.concurrent.ExecutionException; -import java.util.concurrent.ExecutorService; -import java.util.concurrent.Executors; -import java.util.concurrent.Future; import org.junit.AssumptionViolatedException; import org.junit.Before; import org.junit.BeforeClass; From 010ddc23462d8508bbfa74983a8d39054a32d0cf Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 19:33:04 +0100 Subject: [PATCH 33/46] Remove use of "synchornized" in Mathsat5AbstractProver. Mathsat only support one thread per ProverEnvironment anyway. --- .../java_smt/solvers/mathsat5/Mathsat5AbstractProver.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 68e5717291..5facef977b 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -112,13 +112,13 @@ private T exec(Callable closure) throws SolverException, InterruptedExcep } @Override - public synchronized boolean isUnsat() throws InterruptedException, SolverException { + public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); return exec(() -> !msat_check_sat(curEnv)); } @Override - public synchronized boolean isUnsatWithAssumptions(Collection pAssumptions) + public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); checkForLiterals(pAssumptions); @@ -238,7 +238,7 @@ protected boolean isClosed() { } @Override - public synchronized T allSat(AllSatCallback callback, List important) + public T allSat(AllSatCallback callback, List important) throws InterruptedException, SolverException { Preconditions.checkState(!closed); checkGenerateAllSat(); From a28e7cd81063328a11065ed330f878e81bf76879 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 19:34:08 +0100 Subject: [PATCH 34/46] Remove use of "synchornized" in Mathsat5InterpolatingProver. --- .../java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java index 40ebc43196..ea1fd42e2e 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5InterpolatingProver.java @@ -152,7 +152,7 @@ public List getTreeInterpolants( } @Override - public synchronized T allSat(AllSatCallback callback, List important) { + public T allSat(AllSatCallback callback, List important) { // TODO how can we support allsat in MathSat5-interpolation-prover? // error: "allsat is not compatible wwith proof generation" throw new UnsupportedOperationException( From 24d16e651c0fe21dcb4f9dbc499dfe16ec96c86a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 19 Dec 2023 19:37:04 +0100 Subject: [PATCH 35/46] Remove comment about bug #339 from SolverThreadLocalityTest as the issues has been solved. --- .../java_smt/test/SolverThreadLocalityTest.java | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 8fa2bffa68..899b851381 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -150,18 +150,6 @@ public void nonlocalProverTest() throws InterruptedException, ExecutionException // (AbstractProver.java:108) // at .. prover.push(formula); - - // FIXME: Exception for MathSAT (bug #339) - // java.lang.StackOverflowError - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve - // (Native Method) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat - // (Mathsat5NativeApi.java:156) - // at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat - // (Mathsat5AbstractProver.java:106) - // at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable - // (ProverEnvironmentSubject.java:67) - // at .. assertThat(prover).isUnsatisfiable(); } catch (SolverException | InterruptedException pE) { throw new RuntimeException(pE); From 7b7082474cdf18a45bed40c8c643193a1e6a71e5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 16:34:06 +0100 Subject: [PATCH 36/46] Fixed resource leak in SolverThreadLocalityTest. See https://github.com/sosy-lab/java-smt/pull/345#discussion_r1432283000 --- .../java_smt/test/SolverThreadLocalityTest.java | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 899b851381..9378a15833 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -17,6 +17,8 @@ import java.util.concurrent.Executors; import java.util.concurrent.Future; import java.util.concurrent.TimeUnit; +import org.junit.After; +import org.junit.Before; import org.junit.Test; import org.sosy_lab.common.configuration.InvalidConfigurationException; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; @@ -32,7 +34,18 @@ import org.sosy_lab.java_smt.solvers.opensmt.Logics; public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { - ExecutorService executor = Executors.newFixedThreadPool(2); + private ExecutorService executor; + + @Before + public void makeThreads() { + executor = Executors.newFixedThreadPool(2); + } + + @After + public void releaseThreads() { + // All threads should have terminated by now as we always wait in the test cases + executor.shutdownNow(); + } @Test public void allLocalTest() throws InterruptedException, SolverException { From 7bde6ff6f862aa951b2947279416b0e38c0dd033 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 16:38:07 +0100 Subject: [PATCH 37/46] Fixed a bug in SolverThreadLocalityTest.nonlocalInterpolationTest where the test may fail if calculating interpolants took too long. --- .../java_smt/test/SolverThreadLocalityTest.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 9378a15833..8e887a6554 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -248,11 +248,11 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi assert task1.get() == null; - Future itp = + Future task2 = executor.submit( () -> { BooleanFormula interpol = prover.getInterpolant(ImmutableList.of(id1)); - Future task2 = + Future task3 = executor.submit( () -> { try { @@ -261,29 +261,29 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi throw new RuntimeException(pE); } }); - assert task2.get() == null; + assert task3.get() == null; return interpol; }); - executor.awaitTermination(100, TimeUnit.MILLISECONDS); + BooleanFormula itp = task2.get(); prover.pop(); - Future task3 = + Future task4 = executor.submit( () -> { try { prover.pop(); - prover.push(itp.get()); + prover.push(itp); prover.push(f2); assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException | ExecutionException pE) { + } catch (SolverException | InterruptedException pE) { throw new RuntimeException(pE); } }); - assert task3.get() == null; + assert task4.get() == null; } } From 0fa64d40594da601516dc13b6f0f5bde6fe907f5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 16:57:49 +0100 Subject: [PATCH 38/46] SolverThreadLocalityTest: Moved hard problem generator global for all tests. --- .../test/SolverThreadLocalityTest.java | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 8e887a6554..97dbb5a52d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -16,7 +16,6 @@ import java.util.concurrent.ExecutorService; import java.util.concurrent.Executors; import java.util.concurrent.Future; -import java.util.concurrent.TimeUnit; import org.junit.After; import org.junit.Before; import org.junit.Test; @@ -36,11 +35,19 @@ public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { private ExecutorService executor; + private HardIntegerFormulaGenerator hardProblem; + private final int DEFAULT_PROBLEM_SIZE = 8; + @Before public void makeThreads() { executor = Executors.newFixedThreadPool(2); } + @Before + public void initProblemGenerator() { + hardProblem = new HardIntegerFormulaGenerator(imgr, bmgr); + } + @After public void releaseThreads() { // All threads should have terminated by now as we always wait in the test cases @@ -51,8 +58,7 @@ public void releaseThreads() { public void allLocalTest() throws InterruptedException, SolverException { requireIntegers(); - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - BooleanFormula formula = gen.generate(8); + BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); try (BasicProverEnvironment prover = context.newProverEnvironment()) { prover.push(formula); @@ -65,7 +71,6 @@ public void allLocalTest() throws InterruptedException, SolverException { public void nonlocalContextTest() throws ExecutionException, InterruptedException, SolverException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); Future result = @@ -84,7 +89,8 @@ public void nonlocalContextTest() BooleanFormulaManager newBmgr = newMgr.getBooleanFormulaManager(); IntegerFormulaManager newImgr = newMgr.getIntegerFormulaManager(); - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(newImgr, newBmgr); + HardIntegerFormulaGenerator newHardProblem = + new HardIntegerFormulaGenerator(newImgr, newBmgr); // FIXME: Exception for CVC5 (related to bug #310?) // io.github.cvc5.CVC5ApiException: @@ -94,7 +100,7 @@ public void nonlocalContextTest() // at io.github.cvc5.Sort.getKind // (Sort.java:93) // at .. - BooleanFormula formula = gen.generate(8); + BooleanFormula formula = newHardProblem.generate(DEFAULT_PROBLEM_SIZE); try (BasicProverEnvironment prover = newContext.newProverEnvironment()) { prover.push(formula); @@ -108,14 +114,11 @@ public void nonlocalContextTest() public void nonlocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); Future result = executor.submit( () -> { - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - // FIXME: Exception for CVC5 (related to bug #310?) // io.github.cvc5.CVC5ApiException: // Invalid call to 'cvc5::SortKind cvc5::Sort::getKind() const', expected non-null @@ -125,7 +128,7 @@ public void nonlocalFormulaTest() // at io.github.cvc5.Sort.getKind // (Sort.java:93) // at .. - return gen.generate(8); + return hardProblem.generate(DEFAULT_PROBLEM_SIZE); }); BooleanFormula formula = result.get(); @@ -139,11 +142,9 @@ public void nonlocalFormulaTest() @Test public void nonlocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); - assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - BooleanFormula formula = gen.generate(8); + BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); try (BasicProverEnvironment prover = context.newProverEnvironment()) { Future task = @@ -216,7 +217,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")); @@ -320,11 +320,11 @@ public void wrongContextTest() throws InterruptedException, SolverException { // Boolector crashes with a segfault: // boolector_assert: argument 'exp' belongs to different Boolector instance - HardIntegerFormulaGenerator gen = new HardIntegerFormulaGenerator(imgr, bmgr); - // Boolector does not support integer, so we have to use two different versions for this test. BooleanFormula formula = - solverToUse() == Solvers.BOOLECTOR ? bmgr.makeFalse() : gen.generate(8); + solverToUse() == Solvers.BOOLECTOR + ? bmgr.makeFalse() + : hardProblem.generate(DEFAULT_PROBLEM_SIZE); try (SolverContext newContext = factory.generateContext()) { try (BasicProverEnvironment prover = From 4246d86a4a5c2e3b095d158d469772de66a69022 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 17:14:44 +0100 Subject: [PATCH 39/46] SolverThreadLocalityTest: Don't catch InvalidConfigurationExceptions when trying to create a new solver context. See https://github.com/sosy-lab/java-smt/pull/345#discussion_r1432283709 --- .../java_smt/test/SolverThreadLocalityTest.java | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 97dbb5a52d..5e5e06c2d7 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -73,15 +73,7 @@ public void nonlocalContextTest() requireIntegers(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); - Future result = - executor.submit( - () -> { - try { - return factory.generateContext(); - } catch (InvalidConfigurationException e) { - throw new RuntimeException(e); - } - }); + Future result = executor.submit(() -> factory.generateContext()); try (SolverContext newContext = result.get()) { FormulaManager newMgr = newContext.getFormulaManager(); @@ -289,7 +281,8 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi @SuppressWarnings("resource") @Test - public void wrongContextTest() throws InterruptedException, SolverException { + public void wrongContextTest() + throws InterruptedException, SolverException, InvalidConfigurationException { assume() .that(solverToUse()) .isNoneOf( @@ -333,8 +326,6 @@ public void wrongContextTest() throws InterruptedException, SolverException { prover.push(formula); assertThat(prover).isUnsatisfiable(); } - } catch (InvalidConfigurationException e) { - throw new RuntimeException(e); } } } From 57ca2f48f0777b047b0a68cf35840f0f8e48817e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 17:18:43 +0100 Subject: [PATCH 40/46] MathSAT5AbstractProver: Remove the helper method exec and install the termination test directly in isUnsat and isUnsatWithAssumptions. This was suggested in https://github.com/sosy-lab/java-smt/pull/345#discussion_r1432281088 --- .../mathsat5/Mathsat5AbstractProver.java | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 5facef977b..c7846bc74a 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -30,7 +30,6 @@ import com.google.common.base.Preconditions; import com.google.common.base.Splitter; -import com.google.common.base.Throwables; import com.google.common.collect.ImmutableMap; import com.google.common.collect.Lists; import com.google.common.primitives.Longs; @@ -42,7 +41,6 @@ import java.util.Map; import java.util.Optional; import java.util.Set; -import java.util.concurrent.Callable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; @@ -97,24 +95,18 @@ private long buildConfig(Set opts) { /** add needed options into the given map. */ protected abstract void createConfig(Map pConfig); - private T exec(Callable closure) throws SolverException, InterruptedException { + @Override + public boolean isUnsat() throws InterruptedException, SolverException { + Preconditions.checkState(!closed); + long hook = context.addTerminationTest(curEnv); - T value = null; + boolean result; try { - value = closure.call(); - } catch (Throwable t) { - Throwables.propagateIfPossible(t, IllegalStateException.class, SolverException.class); - Throwables.propagateIfPossible(t, InterruptedException.class); + result = !msat_check_sat(curEnv); } finally { msat_free_termination_callback(hook); } - return value; - } - - @Override - public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); - return exec(() -> !msat_check_sat(curEnv)); + return result; } @Override @@ -122,7 +114,15 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) throws SolverException, InterruptedException { Preconditions.checkState(!closed); checkForLiterals(pAssumptions); - return exec(() -> !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions))); + + long hook = context.addTerminationTest(curEnv); + boolean result; + try { + result = !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); + } finally { + msat_free_termination_callback(hook); + } + return result; } private void checkForLiterals(Collection formulas) { From c18121a29a639e90727a4ba686af985e493b9b4e Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 17:35:08 +0100 Subject: [PATCH 41/46] Fixed checkstyle warning --- src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 5e5e06c2d7..24acbfb9eb 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -36,7 +36,7 @@ public class SolverThreadLocalityTest extends SolverBasedTest0.ParameterizedSolv private ExecutorService executor; private HardIntegerFormulaGenerator hardProblem; - private final int DEFAULT_PROBLEM_SIZE = 8; + private static final int DEFAULT_PROBLEM_SIZE = 8; @Before public void makeThreads() { From 0f14370c40c3b1c51cfde7f45cb9d731ba3622ff Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 18:36:29 +0100 Subject: [PATCH 42/46] Try and fix the AppVeyor issue. --- .../sosy_lab/java_smt/test/SolverThreadLocalityTest.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 24acbfb9eb..f12e948dc7 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -50,8 +50,10 @@ public void initProblemGenerator() { @After public void releaseThreads() { - // All threads should have terminated by now as we always wait in the test cases - executor.shutdownNow(); + // All threads should have terminated by now as we always wait in the test + if (executor != null) { + executor.shutdownNow(); + } } @Test From 151c2ed6c0c35b038e7120632a6c5ba478dcb6c6 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 20 Dec 2023 18:48:03 +0100 Subject: [PATCH 43/46] Removed unnecessary "resource" annotations. --- src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index f12e948dc7..3206a9d480 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -68,7 +68,6 @@ public void allLocalTest() throws InterruptedException, SolverException { } } - @SuppressWarnings("resource") @Test public void nonlocalContextTest() throws ExecutionException, InterruptedException, SolverException { @@ -103,7 +102,6 @@ public void nonlocalContextTest() } } - @SuppressWarnings("resource") @Test public void nonlocalFormulaTest() throws InterruptedException, SolverException, ExecutionException { @@ -281,7 +279,6 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi } } - @SuppressWarnings("resource") @Test public void wrongContextTest() throws InterruptedException, SolverException, InvalidConfigurationException { From 9b1361c32b4e13a14c128030708cd192ad3438fb Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Tue, 26 Dec 2023 23:13:03 +0100 Subject: [PATCH 44/46] MathSAT: shorten some code and refactor callback-providing method. This commit unifies the level of abstraction for registering a shutdown-callback and removing the callback afterwards. --- .../solvers/mathsat5/Mathsat5AbstractProver.java | 13 +++++-------- .../solvers/mathsat5/Mathsat5SolverContext.java | 9 ++++++--- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index c7846bc74a..39ace99503 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -24,6 +24,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_pop_backtrack_point; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_push_backtrack_point; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_get_arg; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_boolean_constant; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_is_not; @@ -99,14 +100,12 @@ private long buildConfig(Set opts) { public boolean isUnsat() throws InterruptedException, SolverException { Preconditions.checkState(!closed); - long hook = context.addTerminationTest(curEnv); - boolean result; + final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { - result = !msat_check_sat(curEnv); + return !msat_check_sat(curEnv); } finally { msat_free_termination_callback(hook); } - return result; } @Override @@ -115,14 +114,12 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) Preconditions.checkState(!closed); checkForLiterals(pAssumptions); - long hook = context.addTerminationTest(curEnv); - boolean result; + final long hook = msat_set_termination_callback(curEnv, context.getTerminationTest()); try { - result = !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); + return !msat_check_sat_with_assumptions(curEnv, getMsatTerm(pAssumptions)); } finally { msat_free_termination_callback(hook); } - return result; } private void checkForLiterals(Collection formulas) { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java index 6c356e10cf..3eff520873 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5SolverContext.java @@ -17,7 +17,6 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_env; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_version; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_option_checked; -import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_set_termination_callback; import com.google.common.annotations.VisibleForTesting; import com.google.common.base.Preconditions; @@ -300,9 +299,13 @@ public void close() { } } - long addTerminationTest(long env) { + /** + * Get a termination callback for the current context. The callback can be registered upfront, + * i.e., before calling a possibly expensive computation in the solver to allow a proper shutdown. + */ + TerminationCallback getTerminationTest() { Preconditions.checkState(!closed, "solver context is already closed"); - return msat_set_termination_callback(env, terminationTest); + return terminationTest; } @Override From 85c6defe6c04112a8fb3003b6c349a3064137cc1 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 27 Dec 2023 00:05:53 +0100 Subject: [PATCH 45/46] Test: improve and extend some documentation. And fix a typo. --- .../test/SolverThreadLocalityTest.java | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index 3206a9d480..cbe0509c68 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -69,11 +69,12 @@ public void allLocalTest() throws InterruptedException, SolverException { } @Test - public void nonlocalContextTest() + 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()); try (SolverContext newContext = result.get()) { @@ -103,11 +104,12 @@ public void nonlocalContextTest() } @Test - public void nonlocalFormulaTest() + 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 = executor.submit( () -> { @@ -132,13 +134,14 @@ public void nonlocalFormulaTest() } @Test - public void nonlocalProverTest() throws InterruptedException, ExecutionException { + public void nonLocalProverTest() throws InterruptedException, ExecutionException { requireIntegers(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); try (BasicProverEnvironment prover = context.newProverEnvironment()) { + // generate a new prover in another thread, i.e., non-locally Future task = executor.submit( () -> { @@ -206,7 +209,7 @@ public void localInterpolationTest() throws InterruptedException, SolverExce @SuppressWarnings({"unchecked", "resource"}) @Test - public void nonlocalInterpolationTest() throws InterruptedException, ExecutionException { + public void nonLocalInterpolationTest() throws InterruptedException, ExecutionException { requireIntegers(); requireInterpolation(); assume().that(solverToUse()).isNotEqualTo(Solvers.CVC5); @@ -218,6 +221,7 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi (InterpolatingProverEnvironment) context.newProverEnvironmentWithInterpolation()) { T id1 = prover.push(f1); + // push a formula in another thread, i.e., non-locally Future task1 = executor.submit( () -> { @@ -240,6 +244,7 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi assert task1.get() == null; + // compute/check interpolants in different threads, i.e., non-locally Future task2 = executor.submit( () -> { @@ -260,6 +265,7 @@ public void nonlocalInterpolationTest() throws InterruptedException, Executi BooleanFormula itp = task2.get(); prover.pop(); + // use interpolants in another thread, i.e., non-locally Future task4 = executor.submit( () -> { @@ -311,6 +317,11 @@ public void wrongContextTest() // key not found: i@15 // Boolector crashes with a segfault: // boolector_assert: argument 'exp' belongs to different Boolector instance + // + // To fix this issue, we would need to track which formula was created in which context, + // which might result in quite some management and memory overhead. + // We might want to see this as very low priority, as there is no real benefit for the user, + // except having a nice error message. // Boolector does not support integer, so we have to use two different versions for this test. BooleanFormula formula = From 3ce732620d3017160568d9d8b56a8c031e34a845 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 29 Dec 2023 17:33:49 +0100 Subject: [PATCH 46/46] Fixed nonLocalProverTest: To trigger this specific bug in CVC5 we need to create the ProverEnvironment on the thread. The other version also fails, but for different reasons and this somehow got mixed up earlier. --- .../test/SolverThreadLocalityTest.java | 51 +++++++++---------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index cbe0509c68..71a02f8fd8 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -140,32 +140,31 @@ public void nonLocalProverTest() throws InterruptedException, ExecutionException BooleanFormula formula = hardProblem.generate(DEFAULT_PROBLEM_SIZE); - try (BasicProverEnvironment prover = context.newProverEnvironment()) { - // generate a new prover in another thread, i.e., non-locally - Future task = - executor.submit( - () -> { - try { - // FIXME: Exception for CVC5 - // io.github.cvc5.CVC5ApiException: - // Given term is not associated with the node manager of this solver - // at io.github.cvc5.Solver.assertFormula - // (Native Method) - // at io.github.cvc5.Solver.assertFormula - // (Solver.java:1455) - // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.addConstraintImpl - // (CVC5AbstractProver.java:114) - // at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint - // (AbstractProver.java:108) - // at .. - prover.push(formula); - assertThat(prover).isUnsatisfiable(); - } catch (SolverException | InterruptedException pE) { - throw new RuntimeException(pE); - } - }); - assert task.get() == null; - } + // generate a new prover in another thread, i.e., non-locally + Future task = + executor.submit( + () -> { + try (BasicProverEnvironment prover = context.newProverEnvironment()) { + // FIXME: Exception for CVC5 + // io.github.cvc5.CVC5ApiException: + // Given term is not associated with the node manager of this solver + // at io.github.cvc5.Solver.assertFormula + // (Native Method) + // at io.github.cvc5.Solver.assertFormula + // (Solver.java:1455) + // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.addConstraintImpl + // (CVC5AbstractProver.java:114) + // at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint + // (AbstractProver.java:108) + // at .. + prover.push(formula); + assertThat(prover).isUnsatisfiable(); + } catch (SolverException | InterruptedException pE) { + throw new RuntimeException(pE); + } + }); + + assert task.get() == null; } @Override