remove `isUnsatWithAssumptions(...)` and `unsatCoreOverAssumptions(...)` from ProverEnvironment

[kfriedberger]

The two mentioned methods are superfluous, as a possible user can push/pop the assumptions himself easily. Additionally, their current implementation is not consistent for all solvers and this cannot be fixed easily.

The following example fails with all solvers except SMTInterpol and returns an empty model (i.e. no assignment for x). SMTInterpol is the only solver, where we implemented a lazy pop only for the special case of having isUnsatWithAssumptions(...). Even MathSat with its direct API-method msat_check_sat_with_assumptions does not return a valid model that fulfills the additional assumptions.

try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
      IntegerFormula x = imgr.makeVariable("x");
  boolean unsat = prover.isUnsatWithAssumptions(
            Collections.singleton(imgr.equal(x, imgr.makeNumber(12))));
  assertThat(unsat).isFalse();
  try (Model m = prover.getModel()) {
    assertThat(m.evaluate(x)).isEqualTo(BigInteger.valueOf(12));
  }
}

The result of an interpolation-query after calling isUnsatWithAssumptions is also undefined. Should the interpolants contains symbols from the assumption? I would also suggest to remove InterpolatingProverEnvironmentWithAssumptions completely (see also #59).

[kfriedberger]

And another problem: Z3 seems to not support arbitrary boolean formulas as assumptions, but only propositional variables. Otherwise it prints the message WARNING: an assumption must be a propositional variable or the negation of one on stderr. I have not looked deeper into the code of Z3, but this might confuse a user, as our API allows any kind of boolean formula.

[PhilippWendler]

Strictly speaking, the methods are redundant, yes, but apparently for some solvers they are more efficient than push+pop, that's why we wanted to add them. (At least MathSAT has this operation as well because it is more efficient.)

The bugs should be fixed, of course.

[cheshire]

1. We are definitely not removing assumptions support.
2. I'm not sure that methods are redundant, as I think the SMT solver has special treatment for assumptions.
3. I've never used interpolants and I really don't know how assumptions interact with interpolants.

Z3 seems to not support arbitrary boolean formulas as assumptions, but only propositional variables

That's just a limitation of the type system, something which has to be documented, but ultimately that's what user has to leave with.

[cheshire]

The following example fails with all solvers except SMTInterpol and returns an empty model

That's now how assumptions are meant to be used. A proper way would be to add b <=> (x == 12) to the original formula, and then solve with assumption b. Then we should be able to query for the truth value of b as well.

[cheshire]

Can I close this or rename to "interpolation with assumptions API"?

[kfriedberger]

This is not documented and is also not guaranteed by the current API. An assumption can be any kind of boolean formula and not only a literal. Someone should implement a very aggressive check/test for this, because users will use it the wrong way.

[cheshire]

An assumption can be any kind of boolean formula and not only a literal.

Yes, with an imperfect type system we can't guarantee everything.

Someone should implement a very aggressive check/test for this, because users will use it the wrong way.

My assumption (pardon the pun) for this is that people who would be using the "assumption" feature would know what the "assumption" is and how they are meant to behave. Visitors entail a rather hard performance penalty, so unfortunately I can not accept any checks which would try to perform introspection on the formula first. Do you have any good suggestion for documentation which basically should say "do not use it unless you know what an 'assumption' is"?

[kfriedberger]

This is not acceptable. As an example, just look at some code in CPAchecker. We had the intent to replace push(f);isUnsat();pop() with one call to isUnsatWithAssumptions(f). However following your explanation this would not work. Or at least it would work for only some solvers, namely those where an assumption can be any kind of formula.

I do not see the benefit of of isUnsatWithAssumptions, because

• they accept only a special formula, not every formula - as stated by the type-system.
• the implementation behaves differently for all solvers.
• the evaluation of the model is nondeterministic afterwards.
• from the solver's point of view: where is the difference between push(f);isUnsat();pop() and isUnsatWithAssumptions(f)? The only thing that is missing is a call to the solver's API.

btw, for InterpolationProverEnvironment, we have two separate interfaces (see #59) that are different in this exact method and we have a heavy wrapper-class around all solvers, that do not support this feature directly.

I am convinced, that the second method unsatCoreOverAssumptions should remain and can be implemented in a good, defined way.

[cheshire]

We had the intent to replace push(f);isUnsat();pop() with one call to isUnsatWithAssumptions(f)

It's probably not possible to use the assumptions feature correctly unless one understands how are they meant to be used. This can not be enforced with a type system, but can be documented.

they accept only a special formula, not every formula - as stated by the type-system.

We're doing Java, not Coq, the type system can not capture everything.

the implementation behaves differently for all solvers.

Implementation behaves differently for solvers where assumptions are emulated using push/pop, I don't think we can do much else there.

the evaluation of the model is nondeterministic afterwards.

Non-deterministic how specifically?

from the solver's point of view: where is the difference between push(f);isUnsat();pop() and isUnsatWithAssumptions(f)

They are two different systems for incrementality support with two different implementations. E.g. see http://stackoverflow.com/questions/15009599/z3-behaviour-changing-on-request-for-unsat-core Learning clauses also behaves differently for two http://stackoverflow.com/questions/11245992/efficiency-of-constraint-strengthening-in-smt-solvers

btw, for InterpolationProverEnvironment, we have two separate interfaces

As I've said, I do not know how assumptions interact with interpolation, and I would not be against dropping their support in InterpolationProverEnvironment.

[kfriedberger]

ok, I understand the importance of these methods now. Let's keep them as they are now.