diff --git a/plugins/tptp/tptp_printer.ml b/plugins/tptp/tptp_printer.ml index dbaff7536856565bd7db54d1ccebf9912065d89f..f49ef2b12c082b54b2772f4626da220ed4425e79 100644 --- a/plugins/tptp/tptp_printer.ml +++ b/plugins/tptp/tptp_printer.ml @@ -63,6 +63,7 @@ let rec print_type info fmt ty = match ty.ty_node with let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = false; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml index 408b6ac7abc3d545e428251ef3dd0081baa1a8db..e7adeb94bbac3ff95801878e71a824dd39cd9699 100644 --- a/src/printer/alt_ergo.ml +++ b/src/printer/alt_ergo.ml @@ -117,6 +117,7 @@ let rec print_term info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/coq.ml b/src/printer/coq.ml index 9c158bf6b91aab24c30d40200e9e9be7716027d9..5a1fedcb75db89f16c17b8e92f35dd85dcf2cb9e 100644 --- a/src/printer/coq.ml +++ b/src/printer/coq.ml @@ -299,6 +299,7 @@ and print_tnode opl opr info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_custom "%s%%Z"; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/cvc3.ml b/src/printer/cvc3.ml index 6da22a3811ee66825f8d9efc127e086d38761929..377eecc99d626f5bea291c2675208fd9f93cd5dd 100644 --- a/src/printer/cvc3.ml +++ b/src/printer/cvc3.ml @@ -121,6 +121,7 @@ let rec print_term info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/gappa.ml b/src/printer/gappa.ml index 344de1897beea5d776855e920159677a8e8604a1..693d5fb9f370c1ba444ed185dc842cc23d23aa94 100644 --- a/src/printer/gappa.ml +++ b/src/printer/gappa.ml @@ -145,6 +145,7 @@ let print_ident fmt id = let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_default; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/mathematica.ml b/src/printer/mathematica.ml index 9fd5ceabe62a7e25051d644f5f80ace5f5b23eb8..bb15b1dbd6141bfd4dafe221bd7f4083b146ff2d 100644 --- a/src/printer/mathematica.ml +++ b/src/printer/mathematica.ml @@ -115,6 +115,7 @@ let print_ident fmt id = let print_const fmt c = let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_default; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/pvs.ml b/src/printer/pvs.ml index 0ccc31076a0709c50cf85229adbbf1eed5fcc7ab..237d5f56a4a0edf404dcf5ddeabd457d61964405 100644 --- a/src/printer/pvs.ml +++ b/src/printer/pvs.ml @@ -297,6 +297,7 @@ and print_tnode opl opr info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_custom "%s"; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/simplify.ml b/src/printer/simplify.ml index c3808672e36570ce0cdfbbcb6b2e1dea9db79437..1a56dcf8076d93d945cc34c782b3a4779309f100 100644 --- a/src/printer/simplify.ml +++ b/src/printer/simplify.ml @@ -38,6 +38,7 @@ let rec print_term info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = false; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/smtv1.ml b/src/printer/smtv1.ml index a3b2c6d8dde98cd5de212c39fb8283c51c654220..2cc9d49aa05161b03d087b8aef2b9b2c88c6d18b 100644 --- a/src/printer/smtv1.ml +++ b/src/printer/smtv1.ml @@ -63,6 +63,7 @@ let rec print_term info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = false; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml index da88d3d1bfea2637fd52407e1719e4819ad1019f..2bd2cd4a9162721f411f498910844b1afbc6b093 100644 --- a/src/printer/smtv2.ml +++ b/src/printer/smtv2.ml @@ -144,6 +144,7 @@ let rec print_term info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = false; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/printer/yices.ml b/src/printer/yices.ml index a5616886bba9f54c988cfa00873cd1b7d210d30d..3199c1e9c81ea87b50988d87adfcbcf8b0593939 100644 --- a/src/printer/yices.ml +++ b/src/printer/yices.ml @@ -125,6 +125,7 @@ let rec print_term info fmt t = match t.t_node with | Tconst c -> let number_format = { Number.long_int_support = true; + Number.extra_leading_zeros_support = true; Number.dec_int_support = Number.Number_default; Number.hex_int_support = Number.Number_unsupported; Number.oct_int_support = Number.Number_unsupported; diff --git a/src/util/number.ml b/src/util/number.ml index f41200bddfbdfa1aa34567c22c64c915c0e7c3b6..60883d4f7bbae5e9b59dfaafcee196d256330545 100644 --- a/src/util/number.ml +++ b/src/util/number.ml @@ -130,6 +130,7 @@ type integer_support_kind = integer_format number_support_kind type number_support = { long_int_support : bool; + extra_leading_zeros_support : bool; dec_int_support : integer_support_kind; hex_int_support : integer_support_kind; oct_int_support : integer_support_kind; @@ -185,24 +186,36 @@ let print_bin_int support fmt = (fun s i -> assert support.long_int_support; fprintf fmt s i) (fun i -> print_dec_int support fmt (any_to_dec 2 i)) +let remove_leading_zeros support s = + if support.extra_leading_zeros_support then s else + let len = String.length s in + let rec aux i = + if i+1 < len && s.[i] = '0' then aux (i+1) else i + in + let i = aux 0 in + String.sub s i (len - i) + let print_dec_real support fmt = check_support support.dec_real_support (Some (PrintDecReal ("%s.%s", "%s.%se%s"))) (fun (PrintDecReal (noexp,full)) i f e -> match e with - | None -> fprintf fmt noexp i f - | Some e -> fprintf fmt full i f e) - (check_support support.frac_real_support None + | None -> fprintf fmt noexp (remove_leading_zeros support i) f + | Some e -> fprintf fmt full + (remove_leading_zeros support i) f (remove_leading_zeros support e)) + (check_support support.frac_real_support None (fun (PrintFracReal (exp_zero, exp_pos, exp_neg)) i f e -> let f = if f = "0" then "" else f in let e = Opt.fold (fun _ -> int_of_string) 0 e in let e = e - String.length f in if e = 0 then - fprintf fmt exp_zero (i ^ f) + fprintf fmt exp_zero (remove_leading_zeros support (i ^ f)) else if e > 0 then - fprintf fmt exp_pos (i ^ f) ("1" ^ String.make e '0') + fprintf fmt exp_pos (remove_leading_zeros support (i ^ f)) + ("1" ^ String.make e '0') else - fprintf fmt exp_neg (i ^ f) ("1" ^ String.make (-e) '0')) + fprintf fmt exp_neg (remove_leading_zeros support (i ^ f)) + ("1" ^ String.make (-e) '0')) (force_support support.def_real_support (fun def i f e -> fprintf fmt def (sprintf "%s_%s_e%s" i f (match e with None -> "0" | Some e -> remove_minus e))) diff --git a/src/util/number.mli b/src/util/number.mli index 791430e0872a1a3d6c25aeb23e741372b1b1caf4..d629aadeb312a7ebd36b6dcc012e4970fee8d654 100644 --- a/src/util/number.mli +++ b/src/util/number.mli @@ -69,6 +69,7 @@ type integer_support_kind = integer_format number_support_kind type number_support = { long_int_support : bool; + extra_leading_zeros_support : bool; dec_int_support : integer_support_kind; hex_int_support : integer_support_kind; oct_int_support : integer_support_kind;