Issues with NNF tactic and if-then-else terms

[PhilippWendler]

Consider the following test:

  @Test
  public void testNNF_IfThenElse() throws InterruptedException, SolverException {
    IntegerFormula ifThenElse =
        bmgr.ifThenElse(bmgr.makeVariable("a"), imgr.makeVariable("b"), imgr.makeVariable("c"));
    BooleanFormula atom = imgr.equal(ifThenElse, imgr.makeNumber(1));
    BooleanFormula nnf = mgr.applyTactic(atom, Tactic.NNF);
    assertThatFormula(nnf).isEquisatisfiableTo(atom);
    assertThat(nnf).isEqualTo(atom);
  }

This succeeds for all solvers except Z3, because Z3 rewrites the ITE into something else whereas all other solvers treat it as an atom. I would think it better it this is consistent across the solvers.

Furthermore, in order to do the rewriting, Z3 add a new variable named z3!name0. This could be unexpected.

In general, I think more tests should be added for the NNF tactic in JavaSMT, with more complex stuff like ITE. For example, for some solvers the condition of the ITE is rewritten and for some it is not:

  @Test
  public void testNNF_ComplexIfThenElse() throws InterruptedException, SolverException {
    BooleanFormula condition = bmgr.not(bmgr.and(bmgr.makeVariable("a"), bmgr.makeVariable("b")));
    IntegerFormula ifThenElse =
        bmgr.ifThenElse(condition, imgr.makeVariable("c"), imgr.makeVariable("d"));
    BooleanFormula atom = imgr.equal(ifThenElse, imgr.makeNumber(1));
    BooleanFormula nnf = mgr.applyTactic(atom, Tactic.NNF);
    assertThatFormula(nnf).isEquisatisfiableTo(atom);
    assertThat(nnf).isEqualTo(atom);
  }

Maybe there are even differences between ITE with 3 boolean operands and ITE with non-boolean operands, but I didn't check this.

[kfriedberger]

Z3 is the only solver that has its own implementation of tactics like NNF. For other solvers, we apply the tactic in JavaSMT directly. A NNF-result is not unique, i.e., there can be more than one formula representation for the same input.

I understand that a user might not expect temporary variables in formulas. However, we can not guarantee that a solver does not introduce them.