Fixes for real lits

src/languages/smtlib2/poly/print.ml

@@ -95,7 +95,9 @@ let num fmt s =
 let dec ~k fmt s =
   (* smtlib requires at least one digit before or after a `.` *)
   let s =
-    if String.length s >= 2 then
+    if not (String.contains s '.') then
+      s ^ ".0"
+    else if String.length s >= 2 then
       if s.[0] = '.'
       then "0" ^ s
       else if s.[String.length s - 1] = '.'
@@ -387,6 +389,15 @@ module Make
     | Var v -> Env.Term_var.bind env v
     | Constructor (_, l) -> List.fold_left Env.Term_var.bind env l
 
+  let extract_int_lit t =
+    match V.Term.view t with
+    | App (head, [], []) ->
+      begin match V.Term.Cst.builtin head with
+        | B.Integer s -> Some s
+        | _ -> None
+      end
+    | _ -> None
+
   let term_cst_chainable _env c =
     (* WARNING: this `blt` function should only be called with builtins that
        do not have payload (such as terms), since the polymorphic comparison
@@ -541,13 +552,18 @@ module Make
             | App (ah, []), App (bh, [])
               when (match V.Ty.Cst.builtin ah with B.Int -> true | _ -> false) &&
                    (match V.Ty.Cst.builtin bh with B.Real -> true | _ -> false) ->
-              if can_omit_to_real env then
-                match args with
+              begin match args with
+                | [t] when can_omit_to_real env -> term env fmt t
                 | [t] ->
-                  term env fmt t
-                | _ -> _cannot_print "bad application of coercion"
-              else
-                simple "to_real"
+                  if can_omit_to_real env then
+                    term env fmt t
+                  else
+                    begin match extract_int_lit t with
+                      | Some n -> aux (Dolmen_std.Id.create (Value Real) (N.simple n)) []
+                      | None -> simple "to_real"
+                    end
+                | _ -> simple "to_real"
+              end
 
             (* fallback *)
             | _ -> _cannot_print "unhandled builtin"

src/languages/smtlib2/v2.6/script/print.ml

@@ -392,6 +392,15 @@ module Make
     | Var v -> Env.Term_var.bind env v
     | Constructor (_, l) -> List.fold_left Env.Term_var.bind env l
 
+  let extract_int_lit t =
+    match V.Term.view t with
+    | App (head, [], []) ->
+      begin match V.Term.Cst.builtin head with
+        | B.Integer s -> Some s
+        | _ -> None
+      end
+    | _ -> None
+
   let term_cst_chainable _env c =
     (* WARNING: this `blt` function should only be called with builtins that
        do not have payload (such as terms), since the polymorphic comparison
@@ -546,13 +555,18 @@ module Make
             | App (ah, []), App (bh, [])
               when (match V.Ty.Cst.builtin ah with B.Int -> true | _ -> false) &&
                    (match V.Ty.Cst.builtin bh with B.Real -> true | _ -> false) ->
-              if can_omit_to_real env then
-                match args with
+              begin match args with
+                | [t] when can_omit_to_real env -> term env fmt t
                 | [t] ->
-                  term env fmt t
-                | _ -> _cannot_print "bad application of coercion"
-              else
-                simple "to_real"
+                  if can_omit_to_real env then
+                    term env fmt t
+                  else
+                    begin match extract_int_lit t with
+                      | Some n -> aux (Dolmen_std.Id.create (Value Real) (N.simple n)) []
+                      | None -> simple "to_real"
+                    end
+                | _ -> simple "to_real"
+              end
 
             (* fallback *)
             | _ -> _cannot_print "unhandled builtin"

tests/print/smtlib/poly/dune

@@ -18,6 +18,38 @@
   (action (diff poly.expected poly.full)))
 
 
+; Test for real_lit.smt2
+; Incremental test
+
+(rule
+   (target  real_lit.incremental)
+   (deps    (:input real_lit.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_lit.expected real_lit.incremental)))
+
+; Full mode test
+
+(rule
+   (target  real_lit.full)
+   (deps    (:input real_lit.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_lit.expected real_lit.full)))
+
+
 ; Test for unit_and_dec.ae
 ; Full mode test
 

tests/print/smtlib/poly/real_lit.expected

@@ -0,0 +1,6 @@
+Warning The logic used to typecheck the problem (ALL) is not minimal. The minimal logic actually is: QF_UFLRA
+(set-logic QF_UFLRA)
+(declare-fun p (Real) Bool)
+(assert (p 42.0))
+(check-sat)
+(exit)

tests/print/smtlib/poly/real_lit.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun p (Real) Bool)
+(assert (p (to_real 42)))
+(check-sat)
+(exit)

tests/print/smtlib/v2.6/dune

@@ -18,4 +18,36 @@
   (action (diff poly.expected poly.full)))
 
 
+; Test for real_lit.smt2
+; Incremental test
+
+(rule
+   (target  real_lit.incremental)
+   (deps    (:input real_lit.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_lit.expected real_lit.incremental)))
+
+; Full mode test
+
+(rule
+   (target  real_lit.full)
+   (deps    (:input real_lit.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff real_lit.expected real_lit.full)))
+
+
 ; Auto-generated part end

tests/print/smtlib/v2.6/real_lit.expected

@@ -0,0 +1,6 @@
+Warning The logic used to typecheck the problem (ALL) is not minimal. The minimal logic actually is: QF_UFLRA
+(set-logic QF_UFLRA)
+(declare-fun p (Real) Bool)
+(assert (p 42.0))
+(check-sat)
+(exit)

tests/print/smtlib/v2.6/real_lit.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun p (Real) Bool)
+(assert (p (to_real 42)))
+(check-sat)
+(exit)