Exact rationals in the real theory

[tiferrei]

Hi there,

I seem to have hit a bit of a wall using Smtml. I have some SMT problem over the rationals, for which I use the real theory. I understand that Z3 has exact precision support for rationals and algebraic irrationals. However, if I use the Smtml types, all real types are captured as floats.

I think for now I will have to make use of the Z3 library directly, and use the get_ratio methods. Is there perhaps another way to achieve this in Smtml?

Thank you!

Tiago

[joaomhmpereira]

Hi,

This is a known limitation, and we've been planning to refactor the numeric layer to avoid OCaml's built-in types entirely and switch to Zarith so that we can support exact rationals (and avoid the precision issues from using floats).

Would using Q.t from Zarith for reals instead of float work for your use case? If so, this is a fairly simple change and we can implement it quickly.

Thanks for the feedback!

[tiferrei]

Hi there, yes absolutely! Using Q.t would be great :) Perhaps there is a way to have a layered approach to the reals? I.e. instead of defaulting to float, going for Q.t, and if not rational, then float?

[filipeom]

Maybe we could have something like this?

(* value.ml *)

type real_val = 
  | Rat of Q.t 
  | Flt of float

type t = 
  | Real of real_val

It would allow us to return rational numbers and you'd be able to pattern match against it. It's a breaking change, but aside from real creation no further API would break.

However, there's a couple of issues with things like people mixing Rats with Flts. I.e.:

(* Comparisons are dangerous! *)
  let eq v1 v2 = 
    match v1, v2 with
    | Rat q1, Rat q2 -> Q.equal q1 q2
    | Flt f1, Flt f2 -> Float.equal f1 f2 (* Or use epsilon *)
    | Rat q, Flt f 
    | Flt f, Rat q   -> 
        (* Decide: Do you convert Rat to Float to compare? *)
        (* Or, do we raise an exception? *)
        Float.equal (Q.to_float q) f  

What would be our policy? Would we simply degrade Rat -> Flt or would we disallow combining Rat and Flt?

[tiferrei]

This is a great point. Here is how I see it: if I am using floats I already lost :)
I would argue even maybe for type real_val = Exact of Q.t | Approx of float. And then if we are doing a comparison between an exact and an approx, I would argue that it probably does not matter, as I am already dealing with imprecision.

Option 1: convert both to float means you lose the precision of the rat, but the premise
itself is imprecise, as a float is involved.

Option 2: convert the float to rat. One would argue this would be misleading, since the data itself is flawed.

PS: There is no rush on this! In practice I really only used Z3 locally, and wanted more to have different solver options in production. I can keep "developing" with the Z3 lib, and swap back to smtml once I need different solvers.

[filipeom]

I would argue even maybe for type real_val = Exact of Q.t | Approx of float

Okay, yes, I think it's more explicit this way.

Option 1: convert both to float means you lose the precision of the rat, but the premise
itself is imprecise, as a float is involved.

Maybe we can go with this option as a fallback behavior and provide some warning logs about the conversions we're doing to avoid surprises.

PS: There is no rush on this! In practice I really only used Z3 locally, and wanted more to have different solver options in production. I can keep "developing" with the Z3 lib, and swap back to smtml once I need different solvers.

We have our weekly release on Monday, so I wanted to try to do this quickly to have it by then. I also wanted to test using rationals in one of our tools to check if it's better.

[tiferrei]

Hi @filipeom,

Another thing I noticed when interacting directly with Z3 is that it will expose:

Arithmetic.Real.get_ratio : Expr.expr -> Q.t

which gives you (Z.t * Z.t) to represent the fraction. However, when creating a symbol, it exposes only:

Arithmetic.Real.mk_numeral_nd : context -> int -> int -> Expr.expr

meaning that at least when encoding constants, the precision is limited to int / int fractions instead of Z.t / Z.t. This is not ideal but I guess it's better than nothing.

PS: I have now encountered a simple instance over exact reals where Z3 takes >10h to solve while CVC5 seems to solve it in half a second. If you are still working on Smtml exact reals I'd be very happy to help pushing it across the finish line :)

[sim642]

The problem doesn't seem to be just rationals/reals but even with arbitrary-precision integers.
For example, Z3 can extract them to Zarith with Arithmetic.Integer.get_big_int: Expr.expr -> Z.t.