Project

General

Profile

Revision ef598ac3

View differences:

src/backends/EMF/EMF_common.ml
210 210
    
211 211
(******** Other print functions *)
212 212

  
213
let pp_emf_list ?(eol:('a, formatter, unit) Pervasives.format="") pp fmt l =
213
let pp_emf_list ?(eol:('a, formatter, unit) Stdlib.format="") pp fmt l =
214 214
  match l with
215 215
    [] -> ()
216 216
  | _ -> fprintf fmt "@[";
src/plugins/salsa/salsaDatatypes.ml
116 116
    | LT.Const_real r -> (* TODO: this is incorrect. We should rather
117 117
				  compute the error associated to the float *)
118 118
       (* let f = float_of_string s in *)
119
       let n = Real.to_num r in
120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_num n)
119
       let n = Real.to_q r in
120
       Salsa.Builder.mk_cst (Salsa.Float.Domain.inject_q n)
121 121
       
122 122
       (* let r = Salsa.Prelude.r_of_f_aux r in *)
123 123
       (* Salsa.Builder.mk_cst (Float.Domain.nnew r r) *)
src/real.ml
1 1
(* (a, b, c) means a * 10^-b. c is the original string *)
2
type t = Num.num * int * string 
2
type t = Q.t * int * string 
3 3

  
4 4
let pp fmt (c, e, s) =
5 5
    Format.fprintf fmt "%s%s"
......
7 7
      (if String.get s (-1 + String.length s) = '.' then "0" else "")
8 8

  
9 9
let pp_ada fmt (c, e, s) =
10
  Format.fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
10
  Format.fprintf fmt "%s.0*1.0e-%i" (Q.to_string c) e
11 11
  
12
let create m e s = Num.num_of_string m, e, s
13
let create_num n s = n, 0, s
12
let create m e s = Q.of_string m, e, s
13

  
14
let create_q q s = q, 0, s
14 15
                   
16
(*
15 17
let to_num (c, e, s) =
16 18
  let num_10 = Num.num_of_int 10 in
17 19
  Num.(c // (num_10 **/ (num_of_int e)))
18

  
20
 *)
21
                 
19 22
let rec to_q (c, e, s) =
20 23
  if e = 0 then
21
        Q.of_string (Num.string_of_num c)
24
    c
22 25
  else
23 26
    if e > 0 then Q.div (to_q (c,e-1,s)) (Q.of_int 10)
24 27
    else (* if exp<0 then *)
......
26 29
        (to_q (c,e+1,s))
27 30
        (Q.of_int 10)
28 31

  
32
let to_num = to_q
33
           
29 34
let to_string (_, _, s) = s
30 35
                        
31 36
let eq r1 r2 =
32
  Num.eq_num (to_num r1) (to_num r2)
37
  Q.equal (to_q r1) (to_q r2)
33 38
  
34 39
  
35 40
let num_binop op r1 r2 =
......
38 43
  
39 44
let arith_binop op r1 r2 =
40 45
  let r = num_binop op r1 r2 in
41
  create_num r (Num.string_of_num r)
46
  create_q r (Q.to_string r)
42 47
  
43
let add   = arith_binop (Num.(+/))
44
let minus = arith_binop (Num.(-/))
45
let times = arith_binop (Num.( */))
46
let div   = arith_binop (Num.(//)) 
48
let add   = arith_binop Q.add
49
let minus = arith_binop Q.sub
50
let times = arith_binop Q.mul
51
let div   = arith_binop Q.div 
47 52

  
48
let uminus (c, e, s) = Num.minus_num c, e, "-" ^ s
53
let uminus (c, e, s) = Q.neg c, e, "-" ^ s
49 54

  
50
let lt = num_binop (Num.(</))
51
let le = num_binop (Num.(<=/))
52
let gt = num_binop (Num.(>/))
53
let ge = num_binop (Num.(>=/))
54
let diseq = num_binop (Num.(<>/))
55
let eq = num_binop (Num.(=/))
55
let lt = num_binop (Q.(<))
56
let le = num_binop (Q.(<=))
57
let gt = num_binop (Q.(>))
58
let ge = num_binop (Q.(>=))
59
let diseq = num_binop (Q.(<>))
60
let eq = num_binop (Q.(=))
56 61

  
57
let zero = Num.num_of_int 0, 0, "0.0"
62
let zero = Q.zero, 0, "0.0"
58 63

  
59
let is_zero r = Num.eq_num (to_num r) (Num.num_of_int 0)
60
let is_one r = Num.eq_num (to_num r) (Num.num_of_int 1)
64
let is_zero r = Q.equal (to_num r) Q.zero
65
let is_one r = Q.equal (to_num r) Q.one
src/real.mli
2 2
val pp: Format.formatter -> t -> unit
3 3
val pp_ada: Format.formatter -> t -> unit
4 4
val create: string -> int -> string -> t
5
val create_num: Num.num -> string -> t
5
(*val create_num: Num.num -> string -> t*)
6
val create_q: Q.t -> string -> t
6 7

  
7 8
val add: t -> t -> t
8 9
val minus: t -> t -> t
......
17 18
val eq: t -> t -> bool
18 19
val diseq: t -> t -> bool
19 20
  
20
val to_num: t -> Num.num
21
(*val to_num: t -> Num.num*)
21 22
val to_q: t -> Q.t
22 23
val to_string: t -> string
23 24
val eq: t -> t -> bool
src/tools/seal/seal_extract.ml
165 165
        if Z3.Expr.is_numeral ze then
166 166
          let e =
167 167
            if Z3.Arithmetic.is_real ze then
168
              let num =  Num.num_of_ratio (Z3.Arithmetic.Real.get_ratio ze) in
169 168
              let s = Z3.Arithmetic.Real.numeral_to_string ze in
169
              (* Use to return a Num.ratio. Now Q.t *)
170
              let ratio = Z3.Arithmetic.Real.get_ratio ze in
171
              (*let num =  Num.num_of_ratio ratio in
172
              let real = Real.create_num num s in*)
173
              let real = Real.create_q ratio s in
170 174
              mkexpr
171 175
                Location.dummy_loc
172 176
                (Expr_const
173
                   (Const_real
174
                      (Real.create_num num s)))
177
                   (Const_real real))
175 178
            else if Z3.Arithmetic.is_int ze then
176 179
              mkexpr
177 180
                Location.dummy_loc
178 181
                (Expr_const
179
                   (Const_int
180
                      (Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int ze))))
182
                   (Const_int 
183
                      (Z.to_int (Z3.Arithmetic.Integer.get_big_int ze))))
181 184
            else if Z3.Expr.is_const ze then
182 185
              match Z3.Expr.to_string ze with
183 186
              | "true" -> mkexpr Location.dummy_loc
src/tools/zustre/zustre_cex.ml
58 58
      let args = Z3.Expr.get_args conj in
59 59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
60 60
        (* Should be done with get_int but that function vanished from the opam Z3 API *)
61
	let id = Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) in
61
	let id = Z.to_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) in
62 62
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
63 63
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
64 64
	(id, (input_values, output_values))::main, funs

Also available in: Unified diff