X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple_test.ml;h=9e79ee9e46adec9badb50c9b8432a497eb7ee8f2;hb=1f8f8e52c38e1897e9b5ea106721d6a4dd88c284;hp=d5cb66b6b8abc11173b9f4129a352cf6c1b68a4a;hpb=71b9c490cad6115af378d01b5aaa06ff858b6243;p=fireball-separation.git

diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml
index d5cb66b..9e79ee9 100644
--- a/ocaml/simple_test.ml
+++ b/ocaml/simple_test.ml
@@ -1,6 +1,10 @@
 open Simple;;
 open Util;;
 
+let with_const =
+ List.mem "--with-const" (Array.to_list Sys.argv)
+ ;;
+
 let acaso l =
     let n = Random.int (List.length l) in
     List.nth l n
@@ -24,29 +28,48 @@ let gen n vars =
     else let inerts, lams = if Random.int 2 = 0
       then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams
       else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams
-    in aux (n-1) inerts lams
-  in aux (2*n) vars []
+    in aux (n-1) inerts lams in
+  let inerts = if with_const then "C" :: vars else vars in
+  aux (2*n) inerts []
 ;;
 
 
 let rec repeat f n =
-  prerr_endline "\n########################### NEW TEST ###########################";
-  f () ;
+  print_endline "\n########################### NEW TEST ###########################";
+  f n ;
   if n > 0 then repeat f (n-1)
 ;;
 
 let main =
   Random.self_init ();
-  let num = 100 in
-  let complex = 200 in
-  let no_bound_vars = 20 in
-  let vars = Array.to_list
-   (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) in
-
-  repeat (fun _ ->
+  let num = 1000 in
+  (*let complex = 100 in
+  let no_bound_vars = 10 in*)
+  let file = Filename.temp_file ~temp_dir:"./problems/" "simple.constants.auto." "" in
+  let oc = open_out file in
+  print_endline ("\n\n---- <TESTS> " ^ file) ;
+  repeat (fun x ->
+    let complex = 100 + x / 10 in
+    let no_bound_vars = Random.int 20 + 1 in
+    let vars = Array.to_list
+     (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) in
     let div, convs = gen complex vars in
-    Simple.run div convs
+    let str = " \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
+    print_endline str;
+    try
+     (solve ++ problem_of ++ Parser.problem_of_string) ("$" ^ str)
+    with Failure _ as e ->
+     let str = "$! failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in
+     Printf.fprintf oc "%s\n" str
+    | Unseparable _ -> ()
   ) num ;
-
-  prerr_endline "\n---- ALL TESTS COMPLETED ----"
+  close_out oc;
+  print_endline ("\n\n---- </TESTS> " ^ file);
+  let filesize filename =
+    let ic = open_in filename in
+    let size = in_channel_length ic in
+    close_in ic ; size in
+  if filesize file = 0
+   then (print_endline "---- All tests succeeded."; Sys.remove file )
+   else (print_endline ("---- Not all tests succeeded. See " ^ file))
 ;;