Z3 fails when given mixed integer-real arguments for division

[daniel-raffler]

Hello everyone,
there seems to be an issue with division in Z3 if one of the arguments is integer and the other is real:

@Test
public void divBugTest() throws SolverException, InterruptedException {
  requireRationals();

  RationalFormula f1 = rmgr.divide(imgr.makeNumber(1), rmgr.makeNumber(2));
  RationalFormula f2 = rmgr.divide(rmgr.makeNumber(1), imgr.makeNumber(2));

  System.out.println(f1);
  System.out.println(f2);

  try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
    prover.isUnsat();
    Model model = prover.getModel();
    assertThat(model.evaluate(f1)).isEqualTo(Rational.ofLongs(1, 2));
    assertThat(model.evaluate(f2)).isEqualTo(Rational.ofLongs(1, 2));
  }
}

The output while running the test for Z3 looks like this:

(div 1 (to_int 2.0))
(/ 1.0 (to_real 2))

Depending on the type of the first argument Z3 seems to be using either integer or rational division. The result for f1 on Z3 is therefore 0 and not 1/2 as expected. We should add some explicit casts to make sure that rational division is always used when either of the arguments is rational.

I did check the other operations in NumeralFormulaManager and this bug only seems to affect division.

[daniel-raffler]

I've written some more tests and mixed real-integer terms seem to be broken on other solvers as well:

In most of these cases the return type is wrong and operations like RationalFormulaManger.add will return integer formulas when both arguments are integer formulas. However, there are also some actual solver crashes.due to miss-matching types.

[kfriedberger]

There is nothing wrong with returning Integer (type Integer, IntegerFormula, etc) instead of Rational if the value is an Integer. All operations except DIV (and MOD?) can return an IntegerFormula as mathematical equivalent result. Only DIV (and MOD?) have internal rounding, such that they depend on the exact operation for Integer or Rational type.

We can insert type-conversion inside of the DIV method, depending on the calling NumericFormulaManager.

[daniel-raffler]

There is nothing wrong with returning Integer (type Integer, IntegerFormula, etc) instead of Rational if the value is an Integer.

I agree, but this assumes that the solver can somehow handle the conversions internally. For Z3 this seems to mostly work (with the exception of division), but other solvers crash when the types don't match precisely. For instance, this code

@Test
public void integerTest() throws SolverException, InterruptedException {
  RationalFormula f = rmgr.subtract(imgr.makeNumber(3), imgr.makeNumber(2));
  assertThatFormula(rmgr.equal(f, rmgr.makeNumber(1))).isSatisfiable();;
}

will crash on SMTInterpol, Princess and CVC5. SMTInterpol and Princess fail in subtract as they try to create a RationalFormula from a solver term of type integer, and CVC5 fails for the equation as the left side has type integer, but there is a rational value on the right.

On Z3 there is no crash, but the types don't match:

@Test
public void typeTest() throws SolverException, InterruptedException {
  RationalFormula f = rmgr.subtract(imgr.makeNumber(3), imgr.makeNumber(2));
  System.out.println(mgr.getFormulaType(f));
}

This code will print Integer on Z3, even though f is a RationalFormula, which does seems less than ideal.