Clean-up assumption solving

[daniel-raffler]

Hello,

even after our recent change there are some cases were combining assumption solving with getModel, getUnsatCore or getInterpolant may lead to some unexpected results:

• If we use assumption solving to set a variable that does not also appear in the assertions, the model may or may not include the variable, depending on the solver:

@Test
  public void test_withAssumptions_getModel() throws InterruptedException, SolverException {
    try (var prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
      var a = bmgr.makeVariable("a");
      var b = bmgr.makeVariable("b");
      var c = bmgr.makeVariable("c");
      prover.addConstraint(bmgr.xor(a, b));

      assertThat(prover.isUnsatWithAssumptions(ImmutableSet.of(a, c))).isFalse();
      try (var model = prover.getModel()) {
        assertThat(model.asList()).hasSize(3);
        assertThat(model.evaluate(a)).isTrue();
        assertThat(model.evaluate(b)).isFalse();
        assertThat(model.evaluate(c)).isTrue();
      }

      assertThat(prover.isUnsatWithAssumptions(ImmutableSet.of(a, bmgr.not(c)))).isFalse();
      try (var model = prover.getModel()) {
        assertThat(model.asList()).hasSize(3);
        assertThat(model.evaluate(a)).isTrue();
        assertThat(model.evaluate(b)).isFalse();
        assertThat(model.evaluate(c)).isFalse();
      }
    }
  }

On MathSat the call to model.evaluate(c) will always return false (= the default value for undefined variables), even if c=true was part of the assumptions

• If we use getUnsatCore after solving with assumptions, the core may or may not include the assumptions:

  @Test
  public void test_withAssumptions_getUnsatCore() throws InterruptedException, SolverException {
    requireUnsatCore();
    try (var prover = context.newProverEnvironment(ProverOptions.GENERATE_UNSAT_CORE)) {
      var a = bmgr.makeVariable("a");
      prover.addConstraint(a);

      assertThat(prover.isUnsatWithAssumptions(ImmutableSet.of(bmgr.not(a)))).isTrue();
      var core = prover.getUnsatCore();
      System.out.println(core);
    }
  }

On Z3 the core is reported as [a, nil], which seems like a bug. While Yices fails the test and returns false for isUnsatWithAssumptions

• If we use getInterpolant after solving with assumptions, the interpolants appear to include the assumptions:

  @Test
  @SuppressWarnings("unchecked")
  public <T> void test_withAssumptions_getInterpolant()
      throws InterruptedException, SolverException {
    requireInterpolation();
    try (InterpolatingProverEnvironment<T> prover =
             (InterpolatingProverEnvironment<T>) context.newProverEnvironmentWithInterpolation()) {
      var a = bmgr.makeVariable("a");
      var f = prover.addConstraint(a);

      assertThat(prover.isUnsatWithAssumptions(ImmutableSet.of(bmgr.not(a)))).isTrue();
      var interpolant = prover.getInterpolant(ImmutableList.of(f));
      System.out.println(interpolant);
    }
  }

All solvers report false here, and not (not a)

We should decide how we want solvers to behave in these tests and then write it down in our documentation