]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/simple_test.ml
Improved backtracking in Simple
[fireball-separation.git] / ocaml / simple_test.ml
index 3ec4bb767f9f9a33829ba114a4c4462b80b2eaab..9e79ee9e46adec9badb50c9b8432a497eb7ee8f2 100644 (file)
@@ -36,33 +36,33 @@ let gen n vars =
 
 let rec repeat f n =
   print_endline "\n########################### NEW TEST ###########################";
-  f () ;
+  f n ;
   if n > 0 then repeat f (n-1)
 ;;
 
 let main =
   Random.self_init ();
-  let num = 100 in
-  let complex = 100 in
-  let no_bound_vars = 10 in
-  let vars = Array.to_list
-   (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) in
-
+  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 _ ->
+  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
     let str = " \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
     print_endline str;
     try
      (solve ++ problem_of ++ Parser.problem_of_string) ("$" ^ str)
-    with Simple.Fail _ as e ->
-     let str = "$ failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in
+    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 ;
-
   close_out oc;
   print_endline ("\n\n---- </TESTS> " ^ file);
   let filesize filename =