Fix a bug when converting floats into polka rationals.

Actually, I've replaced a particularly horrible chunk
of code that was buggy (I knew it, but i am lazy...).

examples/lutin/C/Makefile

@@ -10,7 +10,7 @@ CFLAGS = \
 LIBS = -lluc4c_nc -llucky_nc -lgmp -lm -ldl -lstdc++ 
 LUT2C=../../../bin/lutin$(EXE) --2c-4c -seed 42
 LUT2CSOCK=../../../bin/lutin$(EXE) --2c-4c-socks 127.0.0.1 -seed 42
-CALLVIASOCKET=../../../bin/call-via-socket -addr 127.0.0.1 -port 2002
+CALLVIASOCKET=../../../bin/call-via-socket -addr 127.0.0.1 -port 2004
 LUTIN=../../../bin/lutin$(EXE)  -seed 42 -only-outputs 
 
 ifeq ($(HOSTTYPE),mac)

examples/lutin/crazy-rabbit/Makefile

@@ -23,7 +23,7 @@ clean:
 
 test.rif:$(EXPDIR) rabbit.cmxs
 	rm -f test.rif0 .lurette_rc
-	$(LURETTETOP) -go  --output test.rif0  -seed 3306566  \
+	$(LURETTETOP) -go  --output test.rif0  -seed 33  \
 	  -rp "sut:ocaml:rabbit.cmxs:" \
 	  -rp 'env:lutin:rabbit.lut:-main:rabbit:-L:libm.so:-loc' && \
 	grep -v "lurette chronogram" test.rif0  | \

examples/lutin/ldbg/choice.lut

@@ -10,7 +10,7 @@ node main () returns ( x : int) =
   within(0,x,10) fby
   within(0,x,10) and px = pre x fby
     assert (px = pre x and ppx = pre px) in
-     loop [100] {
+     loop [1000] {
         | 100:  within(px,x, ppx)
         | 100:  within(ppx,x, px)
         | 1:  within(0,x,10) 

examples/lutin/ldbg/test4.ml

@@ -31,10 +31,10 @@ break ""
 *)
 
 time_travel true;;
-ckpt_rate:=200;;
+ckpt_rate:=500;;
 let e = run ();;
 
-let e = nexti e 105;;
+let e = nexti e 500;;
 
 let e = back e ;;
 

source/Lurettetop/ldbg_utils.ml

@@ -276,9 +276,9 @@ let (dump_profile_info : unit -> string) =
         ("|---------+-------------+------+------------------------------------------+------------+ \n")
 
 (******************************************************************)
-(* Going backwards *)
+(* A rather naive time travel mechanism  *)
 
-let ckpt_rate = ref 10
+let ckpt_rate = ref 100
 
 let ckpt_tbl = Hashtbl.create 100
 
@@ -353,8 +353,12 @@ let (back : Event.t -> Event.t) =
     let e = rev_cond e stop in
       e
 
+
 let (goto : Event.t -> int -> Event.t) =
   fun e i -> 
     if i > e.nb then goto_i e i else if e.nb = i then e else
-      rev_cond e (fun e -> e.nb = i)
+      let x = ((e.nb-1) / !ckpt_rate ) in
+      let e = Hashtbl.find ckpt_tbl x in
+        Event.set_nb e.nb;
+        rev_cond e (fun e -> e.nb = i)
 

source/Lutin/autoGen.ml

@@ -918,8 +918,9 @@ let config2ttree (it:t) (cfg: config) = (
 		);
 		tt
 	) with Not_found -> (
-		Verbose.exe ~level:2  (fun () -> Printf.printf "##config2ttree: \"%s\" = %s\n" 
-                               ix (CoTraceExp.dumps e));
+		Verbose.exe ~level:2
+        (fun () -> Printf.printf "##config2ttree: \"%s\" = %s\n" 
+           ix (CoTraceExp.dumps e));
      	match ( gentrans it.source_code data e) with
      	(* match ( gentrans_old it.source_code e) with *)
      	Some tt -> (

source/Makefile

@@ -34,6 +34,10 @@ CAML_OPT=
 ifeq ($(shell $(OCAMLC) -version| cut -f1,2 -d.),3.12)
 CAML_OPT=caml
 endif
+# in ocaml 4 also...
+ifeq ($(shell $(OCAMLC) -version| cut -f1 -d.),4)
+CAML_OPT=caml
+endif
 
 
 # C'est le meme que le liblurette_nc, mais sans libasmrun car il est

source/common/polyhedron.ml

@@ -89,56 +89,6 @@ let number_of_ending_zero str =
   let l = (String.length str) - 1 in
     l - (aux str l)
 
-(* Polka constraint parser only parses rationals, therefore
-   i need to translate floats into rats... *)
-let (rat_of_float : float -> int * int) =
-  fun f0 ->
-    try
-      (* XXX i am not particularly proud of that function ... *)
-      let sof = my_string_of_float in
-      let f = float_of_string (sof f0) in
-      let (f_frac, f_integral) = modf (abs_float f) in
-      let f_frac_str = (sof f_frac) in
-      let c = (String.length f_frac_str) - 2 in
-      let f_integral_str = string_of_int (int_of_float f_integral) in
-      let exp = if f_frac = 0. then 0 else
-	     c - (number_of_ending_zero f_frac_str)
-      in
-      let d = power 10 exp in
-      let n_str = (
-        (if f > 0. then "" else "-") ^
-          f_integral_str ^(String.sub (sof f_frac) 2 exp)
-      )
-      in
-      let n = 
-        try int_of_string n_str 
-        with _  -> 
-          Printf.eprintf "Fail to convert into an int the string '%s'.\n" n_str;
-          Printf.eprintf "Hint: use bounds when declaring output or local ";
-          Printf.eprintf "vars (e.g., 'x : real [-10000.;10000]')\n";
-          flush stderr;
-          exit 2
-      in
-      let new_f = (float_of_int n) /. (float_of_int d) in
-        (* runtime check that this crazy code is ok... *)
-        if
-	       ((abs_float ((f  -. new_f))) > 0.1) (* 0.001*f ? *)
-        then
-          let msg = Printf.sprintf 
-            "*** The conversion error is %f (%f = %i/%d)\n"
-	         (abs_float (f -. new_f)) f0 n d
-          in
-	         failwith msg
-        else 
-          (n, d)
-    with e  -> 
-      failwith (
-	     "*** Error when converting the float "^
-	       (string_of_float f0 )^" into a rational number:\n" ^
-	       (Printexc.to_string e) ^ "\n"
-      )
-
-
 
 (* We need to translaste expressions into a string of the format used
    by Polka to parse constraints *)
@@ -147,11 +97,11 @@ let rec (ineq_to_polka_string : Constraint.ineq -> string) =
     let str =
       match f with
 	     | Constraint.GZ(ne)   ->
-	         ((Ne.to_string_gen (nv_to_string) "+" ne) ^ " > 0 ")
+	       ((Ne.to_string_gen (nv_to_string) "+" ne) ^ " > 0 ")
 	     | Constraint.GeqZ(ne) ->
-	         ((Ne.to_string_gen (nv_to_string) "+" ne) ^ " >= 0 ")
+	       ((Ne.to_string_gen (nv_to_string) "+" ne) ^ " >= 0 ")
     in
-      str
+    str
 and
     (constraint_to_string : Constraint.t -> string) =
   fun f ->
@@ -160,33 +110,43 @@ and
 	     | Constraint.Bv(var)  -> (Var.name var)
 	     | Constraint.Ineq(ineq) -> ineq_to_polka_string ineq
 	     | Constraint. EqZ(ne)  ->
-	         ((Ne.to_string_gen (nv_to_string) "" ne) ^ " = 0 ")
+	       ((Ne.to_string_gen (nv_to_string) "" ne) ^ " = 0 ")
     in
-      str
+    str
 and
     (nv_to_string : Value.num -> string) =
   fun n ->
     match n with
 	   | I(i) -> Num.string_of_num i
-      | F(f) -> float_to_string f
+      | F(f) -> float_to_polka_string f
 and
     (int_to_string : int -> string) =
   fun i ->
     ((if i >= 0 then "+" else "-") ^ (string_of_int (abs i)))
 and
-    (float_to_string : float -> string) =
+    (* I need to convert the float '5236.2556' into '+52362556/10000' for polka *)
+    (float_to_polka_string : float -> string) =
   fun f ->
-    let (n, d) = rat_of_float f in
-      ((if n >= 0 then "+" else "-") ^
-         (if  n = 0 then
-	         "0"
-	       else if d = 1 then
-	         (string_of_int (abs n))
-	       else
-	         (string_of_int (abs n)) ^ "/" ^ (string_of_int d)))
-
-
-
+    let res =
+      match f with
+        | 0.0 -> "+0"
+        | 1.0 -> "+1"
+        | -1.0 -> "-1"
+        | _ ->
+          let sign = if f >= 0.0 then "+" else "-" in
+          let f = abs_float f in
+          let str = my_string_of_float f in
+          let dot_index = String.index str '.' in
+          let l = String.length str in
+          let card_zero_denom = l-dot_index-1 in
+          let denom = "1"^ (String.make card_zero_denom '0') in
+          let numerator = 
+          (* remove the "." from str *)
+            (String.sub str 0 (dot_index)) ^  (String.sub str (dot_index+1) (card_zero_denom))
+          in
+          sign ^ numerator ^ "/" ^ denom 
+    in
+    res
 
 
 

source/common/util.ml

@@ -1005,7 +1005,7 @@ let overflow_msg str =
 let int_of_string str =
   try int_of_string str 
   with _  -> 
-    let msg =   Printf.sprintf "Fail to convert into an int the string '%s'.\n" str in
+    let msg = Printf.sprintf "Fail to convert into an int the string '%s'.\n" str in
       overflow_msg msg;
       exit 2