Fix issue 926

[Halbaroth]

This PR fixes the issue #926 about printing reals in models.

The current printer always displays positive reals as rational numbers of the
form (/ x y) where x and y are positive integers. Negative reals are
represented by the expression (/ (- x) y) where x and y are positive
integers. The printer simplifies the expression if the denominator is one.

Notice that by the current implementation of Zarith:

type t = {
    num: Z.t; (** Numerator. *)
    den: Z.t; (** Denominator, >= 0 *)
  }
(* Type of rationals.
   Invariants:
   - den is always >= 0;
   - num and den have no common factor;
   - if den=0, then num is -1, 0 or 1.
   - if num=0, then den is -1, 0 or 1.
 *)

Any rational number of the form 0/q satisfies q = -1 or q = 0 or q = 1.
Thus the printer will always output 0.0 in this case but for the case 0/0
which shouldn't occur.

[bclement-ocp]

It seems that AE (or Zarith?) replaces 0/0 by 0/1. It makes sense as the division by zero has no semantic in the SMT-LIB standard and asserting x = 0/0 means that x can have any value.

Alt-Ergo only uses Q.t to represent rationals, 0/0 should not happen.

[bclement-ocp]

Interestingly, the SMT-LIB theory of Reals (see the :values section) actually mandates that integers don't have the .0… which is what we were doing, but not what other solvers are doing!

Maybe we should say that we respect the SMT-LIB standard and that #926 is a Why3 bug, not an Alt-Ergo bug :)

The standard however also mandates that negative numbers be written (- n), not -n (for both reals and integers) which we don't do.

[Halbaroth]

I don't understand your last sentence. The printer will print (- n) if the input is -n where n is a positive integer.

[Halbaroth]

Or maybe, you mean we have to print (/ (- p) q) instead of (- (/ p q) for the number -p/q?

[bclement-ocp]

Ah, you are right — I misread the code. I does seem that Dolmen refuses integers as reals values in models however… but I am pretty sure the spec says it should accept them.

[bclement-ocp]

Or maybe, you mean we have to print (/ (- p) q) instead of (- (/ p q) for the number -p/q?

As a matter of fact, it looks like that would be the spec-compliant way of writing it, yeah.

[Gbury]

Ah, I guess you mean that 5.0 is a valid term of real type, not necessarily a value of real type.

Indeed, and also that any term of type real, which can be evaluated down to a value can be used in a model definition (which might be the surprising/important point actually).

[bclement-ocp]

Right, thanks for the clarifications! I was confused by the fact that the language spec mandates (page 65) that the result of get-value be a value term ("returns for each tᵢ a value term vᵢ") but relaxes that requirement for get-model ("The term t is expected, although not required, to be a value when f is a constant").

[Gbury]

Right, but even then for a get-value, I'd expect it to return a well-typed term that is a value.

In a context with the Reals_Ints theory, that would mean (define-fun a () Real 5.0), because (define-fun a () Real 5) would not be well-typed.

I think it's reasonable because, in my opinion, the main reason behind why the value specification of reals uses integers literals is to have three non-overlapping categories (integer literals, non-integer rationals, and irrationals; which would be harder to specify using decimal literals), and should not be understood as a syntactic restriction on the set of real values. Instead any term that trivially maps to one of these values, should be considered as a value term.

Lastly, and to further my point, the value specification does not really give any concrete way to express irrationals, and the current and planned way to solve that is to accept algebraic numbers using new primitives, so I don't think the value specification is really to be used with too strict an interpretation, otherwise it would make models impossible to express in some situations.

[bclement-ocp]

Right, but even then for a get-value, I'd expect it to return a well-typed term that is a value.

I would agree with you except for the footnote that states "Recall that value terms are particular ground terms defined in a logic for each sort (see Subsection 5.5.1)." and explicitly points to the "values" specification of the logic!

To clarify, I agree with what you are saying and am perfectly happy with ignoring that part of the spec and using well-typed ground terms in models, I am just explaining why I was confused by the wording in the spec.

[Gbury]

That's a good point, I'd be interested in knowing whether any solver actually respects that (and therefore outputs suspiciously-typed terms), or if it's something that really everyone ignores.

[bclement-ocp]

LGTM, feel free to do (/ (- p) q) if you prefer.