Skip to content

Commit 49a71ea

Browse files
author
BaierD
committed
Add Yices2 implementation for prover based shutdown
1 parent 5e6784b commit 49a71ea

File tree

1 file changed

+17
-3
lines changed

1 file changed

+17
-3
lines changed

src/org/sosy_lab/java_smt/solvers/yices2/Yices2TheoremProver.java

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@
3232
import java.util.Set;
3333
import java.util.stream.Collectors;
3434
import org.checkerframework.checker.nullness.qual.Nullable;
35+
import org.sosy_lab.common.ShutdownManager;
3536
import org.sosy_lab.common.ShutdownNotifier;
3637
import org.sosy_lab.java_smt.api.BooleanFormula;
3738
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
@@ -124,9 +125,13 @@ public boolean isUnsat() throws SolverException, InterruptedException {
124125
int[] allConstraints = getAllConstraints();
125126
unsat =
126127
!yices_check_sat_with_assumptions(
127-
curEnv, DEFAULT_PARAMS, allConstraints.length, allConstraints, shutdownNotifier);
128+
curEnv,
129+
DEFAULT_PARAMS,
130+
allConstraints.length,
131+
allConstraints,
132+
proverShutdownManager.getNotifier());
128133
} else {
129-
unsat = !yices_check_sat(curEnv, DEFAULT_PARAMS, shutdownNotifier);
134+
unsat = !yices_check_sat(curEnv, DEFAULT_PARAMS, proverShutdownManager.getNotifier());
130135
if (unsat && stackSizeToUnsat == Integer.MAX_VALUE) {
131136
stackSizeToUnsat = size();
132137
// If sat check is UNSAT and stackSizeToUnsat waS not already set,
@@ -147,7 +152,11 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
147152
Preconditions.checkState(!closed);
148153
// TODO handle BooleanFormulaCollection / check for literals
149154
return !yices_check_sat_with_assumptions(
150-
curEnv, DEFAULT_PARAMS, pAssumptions.size(), uncapsulate(pAssumptions), shutdownNotifier);
155+
curEnv,
156+
DEFAULT_PARAMS,
157+
pAssumptions.size(),
158+
uncapsulate(pAssumptions),
159+
proverShutdownManager.getNotifier());
151160
}
152161

153162
@SuppressWarnings("resource")
@@ -209,4 +218,9 @@ public void close() {
209218
}
210219
super.close();
211220
}
221+
222+
@Override
223+
protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
224+
return proverShutdownManager;
225+
}
212226
}

0 commit comments

Comments
 (0)