]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Added tests with constants
authoracondolu <andrea.condoluci@unibo.it>
Thu, 7 Jun 2018 09:13:09 +0000 (11:13 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Thu, 7 Jun 2018 09:13:09 +0000 (11:13 +0200)
- Enabled with flag --with-const
- Stores failing problems in problems/ folder

ocaml/simple.mli
ocaml/simple_test.ml

index bdc632827889ffe4136c179ae95001f1f1854e92..fba247092a39b9074941eff9319e7c40038f67a7 100644 (file)
@@ -1,4 +1,5 @@
 type problem\r
+exception Fail of int * string\r
 val solve : problem -> unit\r
 val problem_of :\r
   string * Num.i_var option * Num.i_n_var list * Num.i_n_var list *\r
index 49ea28f78bc5a6d491768c975789b9892c9f2355..3ec4bb767f9f9a33829ba114a4c4462b80b2eaab 100644 (file)
@@ -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,8 +28,9 @@ 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 []
 ;;
 
 
@@ -43,13 +48,28 @@ let main =
   let vars = Array.to_list
    (Array.init no_bound_vars (fun x -> "x" ^ string_of_int x)) 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 _ ->
     let div, convs = gen complex vars in
-    let str = "$ random simple test \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
+    let str = " \nD " ^ div ^ String.concat "\nC " convs ^ "\n" in
     print_endline str;
-    let open Simple in
-    (solve ++ problem_of ++ Parser.problem_of_string) 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
+     Printf.fprintf oc "%s\n" str
   ) num ;
 
-  print_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))
 ;;