Fix issue 926 (#931)

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:
```ocaml
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.

src/lib/reasoners/arith.ml

@@ -813,23 +813,25 @@ module Shostak
         cpt := Q.add Q.one (max_constant distincts !cpt);
         Some (term_of_cst (Q.to_string !cpt), true)
 
-
-
-  let pprint_const_for_model =
-    let pprint_positive_const c =
-      let num = Q.num c in
-      let den = Q.den c in
-      if Z.is_one den then Z.to_string num
-      else Format.sprintf "(/ %s %s)" (Z.to_string num) (Z.to_string den)
-    in
-    fun r ->
-      match P.is_const (embed r) with
-      | None -> assert false
-      | Some c ->
-        let sg = Q.sign c in
-        if sg = 0 then "0"
-        else if sg > 0 then pprint_positive_const c
-        else Format.sprintf "(- %s)" (pprint_positive_const (Q.abs c))
+  let pp_constant ppf r =
+    match P.is_const (embed r), X.type_info r with
+    | Some q, Ty.Tint ->
+      assert (Z.equal (Q.den q) Z.one);
+      let i = Q.num q in
+      if Z.sign i = -1 then
+        Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i)
+      else
+        Fmt.pf ppf "%a" Z.pp_print i
+    | Some q, Ty.Treal ->
+      if Z.equal (Q.den q) Z.one then
+        Fmt.pf ppf "%a.0" Z.pp_print (Q.num q)
+      else if Q.sign q = -1 then
+        Fmt.pf ppf "(/ (- %a) %a)"
+          Z.pp_print (Z.abs (Q.num q))
+          Z.pp_print (Q.den q)
+      else
+        Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q)
+    | _ -> assert false
 
   let choose_adequate_model t r l =
     if Options.get_debug_interpretation () then
@@ -854,6 +856,6 @@ module Shostak
         List.iter (fun (_,x) -> assert (X.equal x r)) l;
         r
     in
-    r, pprint_const_for_model r
+    r, Fmt.str "%a" pp_constant r
 
 end

src/lib/util/numbers.ml

@@ -58,6 +58,7 @@ module Z = struct
   let from_string s = Z.of_string s
   let to_string t   = Z.to_string t
   let print fmt z   = Format.fprintf fmt "%s" (to_string z)
+  let pp_print = Z.pp_print
 
   let my_gcd a b =
     if is_zero a then b

src/lib/util/numbers.mli

@@ -59,6 +59,7 @@ module Z : sig
   val from_int : int -> t
   val from_string : string -> t
   val to_string : t -> string
+  val pp_print : t Fmt.t
 
   (** convert to machine integer. returns None in case of overflow *)
   val to_machine_int : t -> int option

tests/issues/926.models.expected

@@ -0,0 +1,10 @@
+
+unknown
+(
+  (define-fun x1 () Int 5)
+  (define-fun x2 () Int (- 5))
+  (define-fun y1 () Real (/ 3 2))
+  (define-fun y2 () Real 4.0)
+  (define-fun y3 () Real (/ 16 5))
+  (define-fun y4 () Real (/ (- 3) 2))
+)

tests/issues/926.models.smt2

@@ -0,0 +1,16 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x1 Int)
+(declare-const x2 Int)
+(declare-const y1 Real)
+(declare-const y2 Real)
+(declare-const y3 Real)
+(declare-const y4 Real)
+(assert (= x1 5))
+(assert (= x2 (- 5)))
+(assert (= y1 (/ (- 3.0) (- 2.0))))
+(assert (= y2 (/ (- 4.0) (- 1.0))))
+(assert (= y3 3.2))
+(assert (= y4 (/ 3.0 (- 2.0))))
+(check-sat)
+(get-model)

tests/models/arith/arith10.optimize.expected

@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () Real 0)
-  (define-fun y () Real 10)
+  (define-fun x () Real 0.0)
+  (define-fun y () Real 10.0)
 )

tests/models/arith/arith11.optimize.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun x () Real 2)
+  (define-fun x () Real 2.0)
   (define-fun p1 () Bool false)
   (define-fun p2 () Bool true)
 )

tests/models/arith/arith5.optimize.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun x () Real (- (/ 1 18)))
-  (define-fun y () Real (- (/ 1 36)))
-  (define-fun z () Real (- (/ 7 9)))
+  (define-fun x () Real (/ (- 1) 18))
+  (define-fun y () Real (/ (- 1) 36))
+  (define-fun z () Real (/ (- 7) 9))
 )

tests/models/arith/arith7.optimize.expected

@@ -1,10 +1,10 @@
 
 unknown
 (
-  (define-fun x () Real 0)
+  (define-fun x () Real 0.0)
 )
 
 unknown
 (
-  (define-fun x () Real (- (/ 3 2)))
+  (define-fun x () Real (/ (- 3) 2))
 )

tests/models/arith/arith9.optimize.expected

@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () Real 4)
-  (define-fun y () Real 4)
+  (define-fun x () Real 4.0)
+  (define-fun y () Real 4.0)
 )