Skip to content

Commit

Permalink
MathSAT5AbstractProver: Remove the helper method exec and install the…
Browse files Browse the repository at this point in the history
… termination test directly in isUnsat and isUnsatWithAssumptions. This was suggested in #345 (comment)
  • Loading branch information
daniel-raffler authored and baierd committed Jan 3, 2024
1 parent a8f965c commit 1b5e72a
Showing 1 changed file with 16 additions and 16 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -97,32 +95,34 @@ private long buildConfig(Set<ProverOptions> opts) {
/** add needed options into the given map. */
protected abstract void createConfig(Map<String, String> pConfig);

private <T> T exec(Callable<T> 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
public boolean isUnsatWithAssumptions(Collection<BooleanFormula> 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<BooleanFormula> formulas) {
Expand Down

0 comments on commit 1b5e72a

Please sign in to comment.