[Toss-devel-svn] SF.net SVN: toss:[1602] trunk/Toss

[<luk...@us...>]

Revision: 1602
          http://toss.svn.sourceforge.net/toss/?rev=1602&view=rev
Author:   lukaszkaiser
Date:     2011-10-18 23:44:49 +0000 (Tue, 18 Oct 2011)
Log Message:
-----------
Corrections to WL and next steps in Picture integration tests.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/Server/Picture.ml
    trunk/Toss/Server/Tests.ml
    trunk/Toss/Solver/WL.ml
    trunk/Toss/Solver/WL.mli
    trunk/Toss/Solver/WLTest.ml

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-10-18 15:37:54 UTC (rev 1601)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-10-18 23:44:49 UTC (rev 1602)
@@ -12,7 +12,11 @@
 (** Delete top-most quantification of [vs] in the formula. *)
 val del_vars_quant : var list -> formula -> formula
 
+(** Rename quantified variables avoiding the ones from [avs],
+    and the above-quantified ones. Does not go into real_expr. *)
+val rename_quant_avoiding : var list -> formula -> formula
 
+
 (** {2 Relation sign} *)
 
 (** Find all positively and negatively occurring relations. *)

Modified: trunk/Toss/Server/Picture.ml
===================================================================
--- trunk/Toss/Server/Picture.ml	2011-10-18 15:37:54 UTC (rev 1601)
+++ trunk/Toss/Server/Picture.ml	2011-10-18 23:44:49 UTC (rev 1602)
@@ -258,6 +258,12 @@
   let tp = postp left crels delems in
   if !debug_level > -1 then
     Format.eprintf "@[%a@]@ \n%!" Formula.fprint (Formula.And tp);
+  if !debug_level > -1 then (
+    let nofluent_left = Structure.clear_rels left (fun r -> List.mem r drels) in
+    let tbl = WL.all_ntypes_simplified nofluent_left 1 2 in
+    Format.eprintf "@[%a@]@ \n%!" Formula.fprint 
+      (Hashtbl.find tbl (Array.of_list delems));
+  );
   let cut s = List.fold_left Structure.del_elem s
     (List.filter (fun e -> not (List.mem e delems)) (Structure.elements s)) in
   (cut left, cut right, tp)
@@ -360,9 +366,9 @@
     let mw = List.map minimize w in
     if !debug_level > -1 then 
       Format.eprintf "@[%a@]@ \n%!" Formula.fprint (Formula.And (basic :: mw));
-    (*if !debug_level > -1 then 
+    if !debug_level > -1 then 
       Format.eprintf "@[%a@]@ \n%!" Formula.fprint 
-	(Aux.unsome (WL.distinguish_by_type ~qr:1 ~k:2 right wrong));*)
+	(Aux.unsome (WL.distinguish_by_type ~qr:1 ~k:2 right wrong));
     Formula.flatten (Formula.Ex (ex_vars, Formula.And (basic :: mw)))
   )
 

Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml	2011-10-18 15:37:54 UTC (rev 1601)
+++ trunk/Toss/Server/Tests.ml	2011-10-18 23:44:49 UTC (rev 1602)
@@ -17,7 +17,7 @@
   "AssignmentsTest", [AssignmentsTest.tests];
   "SolverTest",      [SolverTest.tests; SolverTest.bigtests];
   "ClassTest",       [ClassTest.tests; ClassTest.bigtests];
-  "WLTest",          [WLTest.tests];
+  "WLTest",          [WLTest.tests; WLTest.bigtests];
 ]
 
 let arena_tests = "Arena", [

Modified: trunk/Toss/Solver/WL.ml
===================================================================
--- trunk/Toss/Solver/WL.ml	2011-10-18 15:37:54 UTC (rev 1601)
+++ trunk/Toss/Solver/WL.ml	2011-10-18 23:44:49 UTC (rev 1602)
@@ -1,5 +1,39 @@
 open Formula
 
+(* Given an array of lists, i.e. a.(i) is a list, find an array b of the same
+   size of sub-lists (b.(i) subset a.(i)) such that if there was an element
+   distinguishing a.(i) from a.(j) then one separates b.(i) from b.(j).
+   This can be done in many ways (is it NP-complete to get the shortest b?),
+   we remove common intersections and branch on [select]-ed elements. 
+   To branches not containing the element append [neg] of the element. *)
+let min_select l = 
+  match Aux.unique_sorted l with [] -> None | x -> Some (List.hd x)
+let rec separate ?(select = min_select) ?(neg = fun e -> []) a =
+  let no_intersect arr =
+    let sorted = Array.map Aux.unique_sorted arr in
+    let nonempty_intersect l1 l2 = 
+      if l1 = [] then l2 else if l2 = [] then l1 else Aux.sorted_inter l1 l2 in
+    let inter = Array.fold_left nonempty_intersect sorted.(0) sorted in
+    Array.map (fun x -> Aux.list_diff x inter) arr in
+  let elems arr = List.concat (Array.to_list arr) in
+  if Array.length a = 0 then a else
+    let b = no_intersect a in
+    match select (elems b) with None -> b | Some e ->
+      let b0 = Array.map (fun l -> if List.mem e l then l else []) b in
+      let b1 = Array.map (fun l -> if List.mem e l then [] else l) b in
+      let (min0, min1) = (separate ~select ~neg b0, separate ~select ~neg b1) in
+      let c = Array.mapi (fun i _ -> if b.(i) = [] then [] else
+	  if b0.(i) = [] then (neg e) @ min1.(i) else e :: min0.(i)) b in
+      Array.map Aux.unique_sorted c
+
+(* Call the separate function from above on an array of conjunctions. *)
+let separate_conjs conjs = 
+  let select_f phis =
+    match List.sort Formula.compare phis with 
+      | [] | [_] -> None | x::__ -> Some x in
+  separate ~select:select_f ~neg:(function Not f -> [f] | f -> [Not f]) conjs
+
+
 (* Helper function: check if a formula holds for a tuple on a structure. *)
 let check structure tuple variables formula = 
   let eval structure phi assignment =
@@ -26,8 +60,9 @@
 
 
 (* The n-type from FO^k for the [tuple] in [structure]. *)
-let rec ntype structure tuple k n =
-  let m = (Array.length tuple) in
+let rec ntype structure tuple k_in n =
+  let m = Array.length tuple in
+  let k = max k_in m in
   let variables = (List.map (fun i -> "x"^string_of_int(i)) (Aux.range k)) in
   if n=0 then 
     Formula.flatten_sort (And (atoms structure tuple (Array.of_list variables)))
@@ -80,95 +115,106 @@
     | _ -> acc_types 
 
 
-let atomsSimplified structure tuples variables =
+(* --- WITH SIMPLIFICATION --- *)
+
+let atoms_simplified structure tuples variables =
   let tlist = Array.map (fun tuple -> 
     Aux.unique_sorted (atoms structure tuple variables)) tuples in
-  let tlistIntersect = Array.fold_left 
-    Aux.sorted_inter (Array.get tlist 0) tlist in
-  let tlistF = Array.map
-    (fun x-> Aux.list_diff x tlistIntersect ) tlist in
-  let tuplesTable = Hashtbl.create 1 in
+  let tlistF = separate_conjs tlist in
+  let tuplesTable = Hashtbl.create 7 in
   Array.iteri (fun i tuple->  
-    Hashtbl.add tuplesTable tuple (And (tlistF.(i)))) tuples;
+    Hashtbl.add tuplesTable tuple (Formula.flatten_sort (And (tlistF.(i))))
+  ) tuples;
   tuplesTable
 
 let nextTypes structure tuples variables types =
   let conjuncts tuple = 
     let indices = Aux.range (Array.length tuple) in
-    let substituted i e = (Aux.array_replace tuple (i-1) e) in
+    let substituted i e = Aux.array_replace tuple (i-1) e in
+    let sorted tp = Array.of_list (Aux.unique_sorted (Array.to_list tp)) in
     let conj_b_ex_xi_typesN_replace_ai_by_b structure tuple i =
-      Aux.unique_sorted (List.map (fun x -> 
-        Ex ([`FO ("x"^(string_of_int i))],
-            (Hashtbl.find types  (substituted i x)))
+      Aux.unique_sorted (Aux.map_some (fun x ->
+	let subst = substituted i x in
+	if Array.length (sorted subst) < Array.length tuple then None else
+          Some (Ex ([`FO ("x"^(string_of_int i))], (Hashtbl.find types subst)))
       ) (Structure.elements structure)) in
     let all_xi_disj_b_typesN_replace_ai_by_b structure tuple i=
       All ([`FO ("x"^(string_of_int i))],
-           ( Or (Aux.unique_sorted(List.map (fun x -> 
-             (Hashtbl.find types (substituted i x))) (Structure.elements
-             structure) )))) in
-    Aux.unique_sorted 
-      ((Hashtbl.find types tuple)::
-      (List.flatten (List.map (fun i ->
-        (all_xi_disj_b_typesN_replace_ai_by_b structure tuple i)::
-          (conj_b_ex_xi_typesN_replace_ai_by_b structure tuple i))
-      indices ))) in
-  let tlist = Array.map (fun tuple ->
-    Aux.unique_sorted (conjuncts tuple)) tuples in
-  let tlistIntersect = Array.fold_left 
-    Aux.sorted_inter (Array.get tlist 0) tlist in
-  let tlistF = Array.map
-    (fun x-> Aux.list_diff x tlistIntersect ) tlist in
-  let tuplesTable = Hashtbl.create 1 in
+           (Or (Aux.unique_sorted (Aux.map_some (
+	     fun x -> 
+	       let subst = substituted i x in
+	       if Array.length (sorted subst) < Array.length tuple then None
+	       else Some (Hashtbl.find types (substituted i x))
+	    ) (Structure.elements structure) )))) in
+    ((Hashtbl.find types tuple)::
+	(List.flatten (List.map (fun i ->
+          (all_xi_disj_b_typesN_replace_ai_by_b structure tuple i)::
+            (conj_b_ex_xi_typesN_replace_ai_by_b structure tuple i)
+	 ) indices ))) in
+  let tlist = Array.map conjuncts tuples in
+  let tlistF = separate_conjs tlist in
+  let tuplesTable = Hashtbl.create 7 in
   Array.iteri (fun i tuple->  
-    Hashtbl.add tuplesTable tuple (And (tlistF.(i)))) tuples;
+    Hashtbl.add tuplesTable tuple (Formula.flatten_sort (And (tlistF.(i))))
+  ) tuples;
   tuplesTable
 
-let rec ntypesSimplified ?(types=None) ?(tuples=None) ?(variables=None)
-?(current=None) structure n k =
-  let tuples = match tuples with Some tp -> tp 
-    | None -> Array.of_list (List.map Array.of_list 
-      (Aux.all_ntuples (Structure.elements structure) k)) in
-  let variables = match variables with Some x -> x
-    | None -> (Array.map (fun i -> "x"^string_of_int(i)) (Array.of_list
-      (Aux.range k))) in
-  let types = match types with Some x -> x | None -> (atomsSimplified
-  structure tuples variables) in
-  match current with 
-  None -> ntypesSimplified 
-    ~types:(Some types) 
-    ~tuples:(Some tuples )
-    ~variables:(Some variables)
-    ~current:(Some 0) structure n k 
-  | Some x -> if x>= n then types
-    else (ntypesSimplified 
-      ~types:(Some (nextTypes structure tuples variables types))
-      ~tuples:(Some tuples)
-      ~variables:(Some variables)
-      ~current:(Some (x+1)) structure n k)
-  
+let rec ntypesSimplified ?cur_types tuples variables structure n k =
+  let x, types = match cur_types with 
+    | Some (step, typs) -> (step, typs) 
+    | None -> (0, atoms_simplified structure tuples variables) in
+  if x >= n then types else 
+    ntypesSimplified 
+      ~cur_types:(x+1, nextTypes structure tuples variables types)
+      tuples variables structure n k
 
+let rec all_ntypes_simplified structure n k =
+  let rec no_rept l = List.length l = List.length (Aux.unique_sorted l) in
+  let tuples = 
+    Array.of_list (List.map Array.of_list (List.filter no_rept (
+      Aux.all_ntuples (Structure.elements structure) k))) in
+  let variables = 
+    Array.map (fun i -> "x"^string_of_int(i)) (Array.of_list (Aux.range k)) in
+  ntypesSimplified tuples variables structure n k
+
+(* Helper function: remove atoms from a formula if [cond] is still satisfied.
+   Note that this is just a greedy heuristic, only And/Or and into Ex/All. *)
+let rec greedy_remove cond phi =
+  let rec greedy_remove_list constructor acc = function
+    | [] -> acc 
+    | x :: xs -> 
+      let rest = acc @ xs in
+      if cond (constructor rest) then greedy_remove_list constructor acc xs else
+	let minx = greedy_remove (fun y -> cond (constructor (y :: rest))) x in
+	greedy_remove_list constructor (minx::acc) xs in
+  match phi with
+    | And fl -> And (greedy_remove_list (fun l -> And l) [] (List.rev fl))
+    | Or fl -> Or (greedy_remove_list (fun l -> Or l) [] (List.rev fl))
+    | Not f -> Not (greedy_remove (fun x -> cond (Not x)) f)
+    | Ex (vs, f) -> Ex (vs, greedy_remove (fun x -> cond (Ex (vs, x))) f)
+    | All (vs, f) -> All (vs, greedy_remove (fun x -> cond (All (vs, x))) f)
+    | phi -> phi
+
+
 let distinguish_by_type ?(skip_outer_exists=false) ~qr ~k struct1 struct2 =
-  let makeList table =
-    Hashtbl.fold (fun x y z -> [y]@z) table [] in
-  let types1 = Aux.unique_sorted (makeList (ntypesSimplified struct1 qr k)) in
-  let types2 = Aux.unique_sorted (makeList (ntypesSimplified struct2 qr k)) in
-  if types1 = types2 then None else
-    let diff1 = (List.filter (fun x -> not (List.mem x types2)) types1) in
-    let dtype = if List.length diff1 > 0 then List.hd diff1 else
-	List.hd (List.filter (fun x -> not (List.mem x types1)) types2) in
-    let distinguishes f = (* check whether f distinguishes the two structures *)
-      let (v1, v2) = (check struct1 [||] [||] f, check struct2 [||] [||] f) in
-      (not v1 && v2) || (not v2 && v1) in
-    let rec minimize acc = function (* greedy heuristic to minimize the type *)
-      | [] -> acc | x :: xs -> 
-	if distinguishes (And (acc @ xs)) then 
-	  minimize acc xs
-	else minimize (x::acc) xs in
-    let minimized_type = match dtype with
-      | And fl -> And (minimize [] (List.rev fl))
-      | phi -> phi in
-    if skip_outer_exists then Some minimized_type else
-      let fv = FormulaSubst.free_vars minimized_type in
-      Some (Ex (List.sort Formula.compare_vars fv, minimized_type))
+  let listht table = Hashtbl.fold (fun x y z -> y :: z) table [] in
+  let types1= Aux.unique_sorted (listht (all_ntypes_simplified struct1 qr k)) in
+  let types2= Aux.unique_sorted (listht (all_ntypes_simplified struct2 qr k)) in
+  let all_diff vars = Aux.map_some (
+    function [x; y] -> if x < y then Some (Not (Eq (x, y))) else None| _ -> None
+  ) (Aux.all_ntuples (List.map to_fo vars) 2) in
+  let distinguishes f = (* check whether f distinguishes the two structures *)
+    let f = And (f :: (all_diff (FormulaSubst.free_vars f))) in
+    let (v1, v2) = (check struct1 [||] [||] f, check struct2 [||] [||] f) in
+    (not v1 && v2) || (not v2 && v1) in
+  let phis = List.sort Formula.compare (Aux.unique_sorted (types1 @ types2)) in
+  try
+    let dtype = List.find distinguishes phis in
+    let mintp = greedy_remove distinguishes dtype in
+    let fv = FormulaSubst.free_vars dtype in
+    let t= FormulaOps.rename_quant_avoiding ((var_of_string "x0")::fv) mintp in 
+    if skip_outer_exists then Some t else
+      Some (Ex (List.sort Formula.compare_vars fv, t))
+  with Not_found -> None
 
 

Modified: trunk/Toss/Solver/WL.mli
===================================================================
--- trunk/Toss/Solver/WL.mli	2011-10-18 15:37:54 UTC (rev 1601)
+++ trunk/Toss/Solver/WL.mli	2011-10-18 23:44:49 UTC (rev 1602)
@@ -1,5 +1,14 @@
 (* The WL algorithm and related tests. *)
 
+(** Given an array of lists, i.e. a.(i) is a list, find an array b of the same
+    size of sub-lists (b.(i) subset a.(i)) such that if there was an element
+    distinguishing a.(i) from a.(j) then one separates b.(i) from b.(j).
+    This can be done in many ways (is it NP-complete to get the shortest b?),
+    we remove common intersections and branch on [select]-ed elements. 
+    To branches not containing the element, we append [neg] of the elem. *)
+val separate: ?select: ('a list -> 'a option) -> ?neg: ('a -> 'a list) ->
+  'a list array -> 'a list array
+
 (** The list of literals which hold for a tuple on a structure,
    i.e. the atomic type of this tuple. *)
 val atoms: Structure.structure -> int array -> string array ->
@@ -17,11 +26,7 @@
 val distinguish_by_type: ?skip_outer_exists: bool -> qr: int -> k: int ->
   Structure.structure -> Structure.structure -> Formula.formula option
 
-val atomsSimplified: Structure.structure -> int array array -> string array -> (int array,Formula.formula) Hashtbl.t 
+val atoms_simplified: Structure.structure -> int array array -> string array -> (int array,Formula.formula) Hashtbl.t 
 
-val ntypesSimplified: ?types:(int array, Formula.formula) Hashtbl.t option ->
-           ?tuples:int array array option ->
-           ?variables:string array option ->
-           ?current:int option ->
-           Structure.structure ->
-           int -> int -> (int array, Formula.formula) Hashtbl.t 
+val all_ntypes_simplified: Structure.structure -> int -> int -> 
+  (int array, Formula.formula) Hashtbl.t 

Modified: trunk/Toss/Solver/WLTest.ml
===================================================================
--- trunk/Toss/Solver/WLTest.ml	2011-10-18 15:37:54 UTC (rev 1601)
+++ trunk/Toss/Solver/WLTest.ml	2011-10-18 23:44:49 UTC (rev 1602)
@@ -26,8 +26,37 @@
     | None -> assert_equal ~printer:(fun x -> x) fopt1 "None"
     | Some f -> formula_eq ~flatten_sort fopt1 f
 
+let hashtbl_eq struc list ht =
+  let str_pair (tuple, phi) = 
+    (Structure.tuple_str struc tuple) ^ "->" ^ (Formula.str phi) in
+  let str ps = String.concat "; " (List.map str_pair ps) in
+  let hashtbl_to_list ht = 
+    let res = ref [] in
+    Hashtbl.iter (fun k v -> res := (k, v) :: !res) ht; !res in
+  let lst = List.map (fun (tp, fs) -> (tp, formula_of_string fs)) list in
+  let simp l = List.sort Pervasives.compare 
+    (List.map (fun (t, f) -> (t, Formula.flatten f)) l) in
+  assert_equal ~printer:str (simp lst) (simp (hashtbl_to_list ht))
 
+let array_list_str f a = "[| [" ^ (String.concat "]; [" (
+  List.map (fun l -> String.concat ";" (List.map f l))
+    (Array.to_list a))) ^ "] |]"
+
+
 let tests = "WL" >::: [
+  "separate" >::
+    (fun () ->
+      let str = array_list_str string_of_int in
+      assert_equal ~printer:str [| [1]; [] |]
+	(WL.separate [| [1;2]; [2;3] |]);
+      assert_equal ~printer:str [| [1]; [-1] |]
+	(WL.separate ~neg:(fun e -> [-e]) [| [1;2]; [2;3] |]);
+      assert_equal ~printer:str [| []; [-3]; [-1] |]
+	(WL.separate [| [1;2;3;4]; [1;2;-3;4]; [-1;2;3;4] |]);
+      assert_equal ~printer:str [| [1;3]; [-3]; [-1;3] |]
+	(WL.separate ~neg:(fun e-> [-e]) [|[1;2;3;4]; [1;2;-3;4]; [-1;2;3;4]|]);
+    );
+
   "atoms" >::
     (fun () ->
       let variables = ["x1";"x2"] in
@@ -40,6 +69,8 @@
   "ntype" >::
     ( fun () ->
       let structure = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_eq ("R(x1,x2) and not R(x1,x1) and not x1=x2 and not R(x2, x1)" ^
+		     " and not R(x2, x2)") (WL.ntype structure [|1;2|] 1 0);
       formula_eq
 	"(R(x1, x2) and not R(x1, x1) and not x1 = x2 and not R(x2, x1) and not R(x2, x2) and
         ex x1 (R(x1, x2) and not R(x1, x1) and not x1 = x2 and not R(x2, x1) and not R(x2, x2)) and
@@ -72,20 +103,46 @@
 	(WL.all_ntypes_ktuples structure 0 2);
     );
 
-  "distinguish" >::
+  "atoms_simplified" >::
     (fun () ->
+      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      hashtbl_eq structure 
+	[ ([|1;2|], "R(x1, x2)"); ([|3;3|], "not R(x1, x2)") ]
+	(WL.atoms_simplified structure [| [| 1;2 |]; [|3;3|] |] [|"x1";"x2"|]);
+    );
+
+  "all_ntypes_simplified" >::
+    (fun () ->
+      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      hashtbl_eq structure 
+	[ ([|1;2|], "R(x1, x2)");
+	  ([|2;1|], "R(x2, x1) and not R(x1, x2)");
+	  ([|1;3|], "not R(x1, x2) and not R(x2, x1)");
+	  ([|3;1|], "not R(x1, x2) and not R(x2, x1)");
+	  ([|2;3|], "R(x1, x2)");
+	  ([|3;2|], "R(x2, x1) and not R(x1, x2)")]
+	(WL.all_ntypes_simplified structure 0 2);
+    );
+
+  "distinguish_by_type" >::
+    (fun () ->
       let structure1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
       let structure2 = (struc_of_string "[ | R { (1, 2) } | ]") in
       formula_option_eq "None" 
 	(WL.distinguish_by_type ~qr:2 ~k:1 structure1 structure2);
-      formula_option_eq "ex x1, x2 (not R(x1, x2) and not x1 = x2 and not R(x2, x1))" 
+      formula_option_eq "ex x1, x2 (not R(x1, x2) and not R(x2, x1))" 
 	(WL.distinguish_by_type ~qr:0 ~k:2 structure1 structure2);
       formula_option_eq "ex x1, x2, x3 (R(x1, x2) and R(x2, x3))"
 	(WL.distinguish_by_type ~qr:0 ~k:3 structure1 structure2);
-      formula_option_eq "(R(x1, x2) and not x1 = x2 and not R(x2, x1) and
- ex x1 (R(x2, x1) and not R(x1, x2) and not x1 = x2))"
+      formula_option_eq "not R(x1, x2) and not R(x2, x1)" 
 	(WL.distinguish_by_type ~skip_outer_exists:true ~qr:1 ~k:2
 	   structure1 structure2);
+    );
+]
+
+let bigtests = "WLBig" >::: [
+  "distinguish_by_type" >::
+    (fun () ->
       let struc1 = struc_of_string "[  |  |  ] \"
 	   ...   ...   ...   ...
 	   B..   W..   ...   ...
@@ -122,34 +179,8 @@
 	...   ...   ...   ...   
 	...W  ...   ...   ...   
 \"" in
-      formula_option_eq "None"
-	(WL.distinguish_by_type ~qr:1 ~k:2 struc1 struc2);
+      formula_option_eq "W(x1) and not ex x3 C(x1, x3)"
+	(WL.distinguish_by_type ~skip_outer_exists:true ~qr:1 ~k:2 
+	   struc1 struc2);
     );
-
-  (*"atomsSimplified" >::
-    (fun () ->
-      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
-
-      Hashtbl.iter
-      (fun x z-> 
-        print_endline (Array.fold_left (fun y r ->
-          y^""^(string_of_int r)) "" x);
-        print_endline (Formula.sprint z) ;
-        print_endline "" )
-      (WL.atomsSimplified structure [| [| 1;2 |]; [|3;3|]|] [|"x1";"x2"|]);
-      assert_equal "a" "a";
-    );*)
-
-  "ntypesSimplified" >::
-    (fun () ->
-      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
-      (*Hashtbl.iter
-      (fun x z-> 
-        print_endline (Array.fold_left (fun y r ->
-          y^""^(string_of_int r)) "" x);
-        print_endline (Formula.sprint z) ;
-        print_endline "" )
-      (WL.ntypesSimplified structure 1 2);*)
-      assert_equal "a" "a";
-    );
 ]

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.