Getting unsat core from isUnsatWithAssumptions

[cheshire]

We need an API to get an unsat core from the satisfiability checking with assumptions. This is complicated, as we effectively get two "modes" for getting the unsat core.

1) Under the "normal" mode, ProverOptions.UNSAT_CORE is required. Constraints are tracked using an auxiliary data structure. Unsat core returned by the solver is resolved s.t. the user gets the subset of assertions which were added.

2) Under the "assumptions" mode, unsat core should be a subset of the requested assumptions.

Switching dynamically between mode (1) and mode (2) depending on what was the last call to prover environment is quite ugly. I'm tempted to just return both the unsat core and the satisfiability status from isUnsatWithAssumptions (e.g. with Optional<List<BooleanFormula>>, but that would give unsat core even to users who don't want them (yet it probably doesn't matter, since the calculation is usually almost free) and would clutter the interface.

[PhilippWendler]

Is an unsat core really an interesting result if you call isUnsatWithAssumptions()? After all, the "unsat" core that is returned could be empty, or even a satisfiable formula. Seems weird to call this "unsat core".

But if this is a relevant operation that we want to add, then I think it is either the current solution, or returning a custom object with isUnsat() and getUnsatCore() methods.

[cheshire]

@PhilippWendler I am not sure I get what you mean. Unsat cores in generic case require labelling provided by the user. We do labelling ourselves, one per added assertion or one per assumption. This creates two different modes of operations.

In any case, I think so far the current solution is acceptable.