From 4464c90b8f07d37bae8c47e90b8b767910be44c5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 15 Dec 2023 07:18:01 +0100 Subject: [PATCH] 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");