Reorder Features Check for Yices2
@@ -123,18 +123,15 @@ public class SolverOverviewTable {
// ignore, feature is not supported.
}
- // UnsatCore: throws UnsupportedOperationException if not available.
- try (ProverEnvironment prover =
- context.newProverEnvironment(ProverOptions.GENERATE_UNSAT_CORE)) {
- if (prover.getUnsatCore() != null) {
- features.add("UnsatCore");
- }
+ // We don't care about the return value, just that it doesn't throw an
+ // UnsupportedOperationException.
+ try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
+ try {
+ prover.isUnsatWithAssumptions(ImmutableList.of());
+ features.add("Assumptions");
} catch (UnsupportedOperationException e) {
// ignore, feature is not supported.
- } catch (Exception e) {
- // UnsatCore throws different Exceptions in some solvers because we use native Exceptions. As
- // long as its not UnsupportedOperationException UnsatCore is supported.
- features.add("UnsatCore");
+ }
}
// UnsatCoreOverAssumptions: throws NullPointerException if available.
@@ -147,19 +144,22 @@ public class SolverOverviewTable {
features.add("UnsatCore /w Assumption");
}
- // There is currently no good way of checking if a solver implements AllSat over our
- // implementation
-
- // We don't care about the return value, just that it doesn't throw an
- // UnsupportedOperationException.
- try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
- try {
- prover.isUnsatWithAssumptions(ImmutableList.of());
- features.add("Assumptions");
+ // UnsatCore: throws UnsupportedOperationException if not available.
+ try (ProverEnvironment prover =
+ context.newProverEnvironment(ProverOptions.GENERATE_UNSAT_CORE)) {
+ if (prover.getUnsatCore() != null) {
+ features.add("UnsatCore");
+ }
} catch (UnsupportedOperationException e) {
// ignore, feature is not supported.
+ } catch (Exception e) {
+ // UnsatCore throws different Exceptions in some solvers because we use native Exceptions. As
+ // long as its not UnsupportedOperationException UnsatCore is supported.
+ features.add("UnsatCore");
}
- }
+
+ // There is currently no good way of checking if a solver implements AllSat over our
+ // implementation
return features;
}
