Formula with same string representation compares as unequal

[PhilippWendler]

The following test fails with Z3:

    BooleanFormula var1 = bmgr.makeVariable("var1");
    BooleanFormula var2 = bmgr.makeVariable("var2");
    BooleanFormula var3 = bmgr.makeVariable("var3");
    BooleanFormula var4 = bmgr.makeVariable("var4");
    assertThat(bmgr.and(bmgr.and(var1, var2), bmgr.and(var3, var4)))
        .isEqualTo(bmgr.and(var1, var2, var3, var4));

(It also fails with some other solvers because JavaSMT is missing simplifications, but this is a different issue.)

The problem with Z3 is that both bmgr.and(bmgr.and(var1, var2), bmgr.and(var3, var4)) and bmgr.and(var1, var2, var3, var4) create the same formula, specifically (and var1 var2 var3 var4), but that equals() on these two instances returns false. Objects representing the same syntactic formula should compare as equal.

(This even works in other cases. If I call bmgr.and(bmgr.and(var1, var2), bmgr.and(var3, var4)) twice, I do get formula instances that compare as equal, just in the above case not.)

[baierd]

On a broader note: we should have tests for this and some other basic cases. @rsoegtrop can you take a look at this issue and add some tests that cover this and some other basic cases?

[RSoegtrop]

@baierd I looked into it and found: equals in Z3Formula uses Native.isEqAst which returns true, if the long representation of the AST's are equal. bmgr.and(bmgr.and(var1, var2), bmgr.and(var3, var4)) and bmgr.and(var1, var2, var3, var4) yield the same string representation but a different long representation, due to the way they are generated. So equals in Z3Formula does not follow the description given in Formula. I fixed it by also checking the string representation for equality, which solves the issue but seems a bit sketchy.

I added some tests, but as it was mentioned above, simplification is missing, so they fail for every solver, except Z3 and SMTInterpol.

[kfriedberger]

Formula::toString can be exponentially (!) bad in runtime and memory consumption. This is no acceptable solution.

[kfriedberger]

Just as reminder, please take a look at the JavaDoc for Formula::equals : https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/api/Formula.java#L28

 /**
   * checks whether the other object is a formula of the same structure. Does not apply an expensive
   * SAT-check to check equisatisfiability.
   *
   * <p>Two formulas that are structured in the same way, are determined as "equal". Due to
   * transformations and simplifications, two equisatisfiable formulas with different structure
   * might not be determined as "equal".
   */
  @Override
  boolean equals(Object other);

Is it really true that JavaSMT does violate this rule for the given formulas?

If really urgently required, we can use a FormulaVisitor to traverse formulas for equality in structure.

[PhilippWendler]

Is it really true that JavaSMT does violate this rule for the given formulas?

I would say yes. The formulas have "the same structure" as we can see when we print them. I would also expect that traversing them yields the same structure (but I have not checked this).

I would suggest to check why the usual memoization of formulas does not happen as expected inside Z3 here, and potentially file a bug for Z3, if it violates its promises.