Skip to content

Commit 5b64a3b

Browse files
author
BaierD
committed
Add Bitwuzla implementation for prover based shutdown
1 parent 19372c0 commit 5b64a3b

File tree

1 file changed

+12
-2
lines changed

1 file changed

+12
-2
lines changed

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
import java.util.Optional;
1818
import java.util.Set;
1919
import org.checkerframework.checker.nullness.qual.Nullable;
20+
import org.sosy_lab.common.ShutdownManager;
2021
import org.sosy_lab.common.ShutdownNotifier;
2122
import org.sosy_lab.java_smt.api.BooleanFormula;
2223
import org.sosy_lab.java_smt.api.Model;
@@ -38,7 +39,10 @@ class BitwuzlaTheoremProver extends AbstractProverWithAllSat<Void> implements Pr
3839
new Terminator() {
3940
@Override
4041
public boolean terminate() {
41-
return shutdownNotifier.shouldShutdown(); // shutdownNotifer is defined in the superclass
42+
return proverShutdownManager
43+
.getNotifier()
44+
.shouldShutdown(); // shutdownNotifer is defined in the
45+
// superclass
4246
}
4347
};
4448
private final Bitwuzla env;
@@ -119,7 +123,8 @@ private boolean readSATResult(Result resultValue) throws SolverException, Interr
119123
return false;
120124
} else if (resultValue == Result.UNSAT) {
121125
return true;
122-
} else if (resultValue == Result.UNKNOWN && shutdownNotifier.shouldShutdown()) {
126+
} else if (resultValue == Result.UNKNOWN
127+
&& proverShutdownManager.getNotifier().shouldShutdown()) {
123128
throw new InterruptedException();
124129
} else {
125130
throw new SolverException("Bitwuzla returned UNKNOWN.");
@@ -246,6 +251,11 @@ protected BitwuzlaModel getEvaluatorWithoutChecks() {
246251
Collections2.transform(getAssertedFormulas(), creator::extractInfo)));
247252
}
248253

254+
@Override
255+
protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
256+
return proverShutdownManager;
257+
}
258+
249259
public boolean isClosed() {
250260
return closed;
251261
}

0 commit comments

Comments
 (0)