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

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

Revision: 1625
          http://toss.svn.sourceforge.net/toss/?rev=1625&view=rev
Author:   lukaszkaiser
Date:     2011-11-10 01:26:59 +0000 (Thu, 10 Nov 2011)
Log Message:
-----------
Correcting and completing guarded types, merging WL with Distinguish and allowing to set method.

Modified Paths:
--------------
    trunk/Toss/Formula/Aux.ml
    trunk/Toss/Formula/Aux.mli
    trunk/Toss/Server/LearnGame.ml
    trunk/Toss/Server/LearnGameTest.ml
    trunk/Toss/Server/Picture.ml
    trunk/Toss/Server/Tests.ml
    trunk/Toss/Solver/Distinguish.ml
    trunk/Toss/Solver/Distinguish.mli
    trunk/Toss/Solver/DistinguishTest.ml

Removed Paths:
-------------
    trunk/Toss/Solver/WL.ml
    trunk/Toss/Solver/WL.mli
    trunk/Toss/Solver/WLTest.ml

Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Formula/Aux.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -348,6 +348,10 @@
     | [] -> [] in
   idemp (List.sort cmp l)
 
+let all_subsets ?max_size set =
+  let size = match max_size with Some i -> i | None -> List.length set in
+  [] :: (unique_sorted (List.map unique_sorted (all_ntuples set size)))
+
 let unique_append l1 l2 =
   List.fold_left (fun l2 e ->
     if List.mem e l2 then l2 else e::l2) l2 (List.rev l1)

Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Formula/Aux.mli	2011-11-10 01:26:59 UTC (rev 1625)
@@ -172,6 +172,9 @@
 (** An [n]th cartesian power of the list. Tail recursive. *)
 val all_ntuples : 'a list -> int -> 'a list list
 
+(** All subsets of a given [set] of size up to [max_size]. *)
+val all_subsets : ?max_size: int -> 'a list -> 'a list list
+
 (** Remove an occurrence of a value (uses structural equality). *)
 val remove_one : 'a -> 'a list -> 'a list
 

Modified: trunk/Toss/Server/LearnGame.ml
===================================================================
--- trunk/Toss/Server/LearnGame.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Server/LearnGame.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -19,7 +19,7 @@
 
 
 let winFormula winningStates notWinningStates =
-  WL.distinguish winningStates notWinningStates
+  Distinguish.distinguish winningStates notWinningStates
 
 let cleanStructure struc =
   let funs = List.map fst (Structure.StringMap.bindings (Structure.functions struc)) in

Modified: trunk/Toss/Server/LearnGameTest.ml
===================================================================
--- trunk/Toss/Server/LearnGameTest.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Server/LearnGameTest.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -76,8 +76,8 @@
 \"" ;]] in
       let res_game =
 "PLAYERS 1, 2
-REL Win1() = ex x1, x2 (Q(x2) and R(x2, x1))
-REL Win2() = ex x1, x2 (Q(x2) and R(x1, x2))
+REL Win1() = ex x0, x1 (Q(x1) and R(x1, x0))
+REL Win2() = ex x0, x1 (Q(x1) and R(x0, x1))
 RULE Mv1: 
 [1 | P:1 {}; Q:1 {}; R:2 {} | ] -> [1 | P (1); Q:1 {}; R:2 {} | ]
 emb R,Q,P pre not Win2()
@@ -107,7 +107,7 @@
 let bigtests = "LearnGame" >::: [
   "tic-tac-toe" >::
     (fun () ->
-      WL.set_debug_level 0; (* set to 1 to get some info printed out *)
+      Distinguish.set_debug_level 0; (* set to 1 to get some info printed out *)
       let partylist0 = [
         List.map struc_of_string [
 "[ | P:1 {}; Q:1 {} | ] \"

Modified: trunk/Toss/Server/Picture.ml
===================================================================
--- trunk/Toss/Server/Picture.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Server/Picture.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -258,12 +258,6 @@
   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)
@@ -368,7 +362,7 @@
       Format.eprintf "@[%a@]@ \n%!" Formula.fprint (Formula.And (basic :: mw));
     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 (Distinguish.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-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Server/Tests.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -17,7 +17,6 @@
   "AssignmentsTest", [AssignmentsTest.tests];
   "SolverTest",      [SolverTest.tests; SolverTest.bigtests];
   "ClassTest",       [ClassTest.tests; ClassTest.bigtests];
-  "WLTest",          [WLTest.tests; WLTest.bigtests];
   "DistinguishTest", [DistinguishTest.tests; DistinguishTest.bigtests];
 ]
 

Modified: trunk/Toss/Solver/Distinguish.ml
===================================================================
--- trunk/Toss/Solver/Distinguish.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Solver/Distinguish.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -3,6 +3,10 @@
 let debug_level = ref 0
 let set_debug_level i = (debug_level := i)
 
+type distinguish_method = Types | Guarded
+
+
+
 (* Helper functions to construct variables for indices. *)
 let varname i = "x" ^ string_of_int i
 let varnames k = List.map varname (Aux.range k)
@@ -19,7 +23,7 @@
       Assignments.assignments_of_list elems vars [tuple] in
   eval structure formula assignment <> AssignmentSet.Empty
 
-(* - Atoms - *)
+(* - Atoms and FO Types - *)
 
 (* The list of literals which hold for a tuple on a structure. *)
 let atoms struc tuple =
@@ -33,7 +37,26 @@
   ) (atoms @ (equalities (varnames k)))
 
 
+(* The [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+let rec ntype struc qr tuple =
+  if qr = 0 then Formula.flatten_sort (And (atoms struc tuple)) else
+    let prevtp i e = ntype struc (qr-1) (Aux.array_replace tuple i e) in
+    let elems = Structure.elements struc in
+    let conj_prev_ex i =
+      And (List.map (fun e -> Ex ([var i], prevtp i e)) elems) in
+    let all_prev_disj i =
+      All ([var i], Or (List.map (prevtp i) elems)) in
+    let next_ntype i = And [conj_prev_ex i; all_prev_disj i] in
+    let nexttp = And (List.map next_ntype (Aux.range (Array.length tuple))) in
+    Formula.flatten_sort (And [ntype struc (qr-1) tuple; nexttp])
 
+(* All types of rank [qr] of all [k]-tuples in [struc]. *)
+let ntypes struc ~qr ~k =
+  let elems = Structure.elements struc in
+  let tups = List.map Array.of_list (Aux.all_ntuples elems k) in
+  Aux.unique_sorted (List.rev_map (ntype struc qr) tups)
+
+
 (* - Guards and Guarded Types - *)
 
 (* Generate all guarded substitutions of [tuple] with the guards.
@@ -86,19 +109,32 @@
   if qr = 0 then Formula.flatten_sort (And (atoms struc tuple)) else
     let prevtp tup = guarded_type struc (qr-1) tup in
     let conj_prev_ex vars guard subst_tuples =
+      let subst_tuples = List.filter (fun tup -> tup <> tuple) subst_tuples in
       And (List.map (fun tup -> Ex (vars, prevtp tup)) subst_tuples) in
     let all_prev_disj vars guard subst_tuples =
       All (vars, Or ((Not guard) :: (List.map prevtp subst_tuples))) in
-    let next_gtype ((vs, g), ts) = 
+    let next_gtype vs (g, ts) = 
       And [conj_prev_ex vs g ts; all_prev_disj vs g ts] in
-    let (guards, subst_tuples) = List.split (
-      List.rev_map (fun (_, vs, t, _, f) -> (vs,f), t) (guards struc tuple)) in
-    let (guards, subst_tuples) = 
-      (Aux.unique_sorted guards, Aux.unique_sorted subst_tuples) in
-    let guarded_tups (_, f) = 
-      List.filter (fun tup -> check struc tup f) subst_tuples in
-    let guards_with_tups = List.map (fun g -> (g, guarded_tups g)) guards in
-    let nextf = And (List.map next_gtype guards_with_tups) in
+    let subst_tuples = Aux.unique_sorted (([], tuple) ::
+      List.rev_map (fun (_,vs,t,_,_) -> (vs, t)) (guards struc tuple)) in
+    let all_vars = varnames (Array.length tuple) in
+    let at_most_vs_tuples vs = List.concat (List.map (
+      fun vs -> Aux.assoc_all vs subst_tuples) (Aux.all_subsets vs)) in
+    let tuples_by_vs = List.map (fun vs -> (vs, at_most_vs_tuples vs))
+      (Aux.all_subsets (List.map var_of_string all_vars)) in
+    let all_guards= FormulaOps.atoms (Structure.rel_signature struc) all_vars in
+    let guards_to_tups (vs, tuples) =
+      let has_vs a = List.for_all (fun v -> Aux.array_mem (to_fo v) a) vs in
+      let is_vs_guard a = has_vs a && 
+	Aux.array_existsi (fun _ v -> not (List.mem (v :> var) vs)) a in
+      let is_vs_guard = function Rel (_, a) -> is_vs_guard a | _ -> false in
+      let vs_guards = List.filter is_vs_guard all_guards in
+      let guarded_tups g = List.filter (fun tup -> check struc tup g) tuples in
+      (vs, List.map (fun g -> (g, guarded_tups g)) vs_guards) in
+    let tups_with_guards = List.map guards_to_tups tuples_by_vs in
+    let tups_with_guards = List.filter (fun (vs,_)-> vs<>[]) tups_with_guards in
+    let next_gtype_vs (vs, gtups) = And (List.map (next_gtype vs) gtups) in
+    let nextf = And (List.map next_gtype_vs tups_with_guards) in
     Formula.flatten_sort (And [guarded_type struc (qr-1) tuple; nextf])
 
 (* All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
@@ -136,8 +172,11 @@
     | phi -> phi
 
 
-let distinguish_by_type ?(skip_outer_exists=false) ~qr ~k sPos sNeg=
-  let types s = guarded_types s ~qr ~k in
+let distinguish_by_type ?(how=Guarded) ?(skip_outer_exists=false) ~qr ~k
+    sPos sNeg =
+  let types s = match how with 
+    | Guarded -> guarded_types s ~qr ~k 
+    | Types -> ntypes s ~qr ~k in
   let (tpPos, tpNeg) = (List.map types sPos, List.map types sNeg) in
   (*let all_diff vars = Aux.map_some (
     function [x; y] -> if x < y then Some (Not (Eq (x, y))) else None| _ -> None
@@ -160,12 +199,12 @@
   if dtypes = [] then None else
     let is_ok f = fails_neg f && succ_pos [f] in
     let mintp = greedy_remove is_ok (Or dtypes) in
-    let fv = FormulaSubst.free_vars (Or dtypes) in
-    let t= FormulaOps.rename_quant_avoiding fv mintp in 
+    let fv = FormulaSubst.free_vars mintp in
+    let t = FormulaOps.rename_quant_avoiding fv mintp in 
     if skip_outer_exists then Some t else
       Some (Ex (List.sort Formula.compare_vars fv, t))
 
-let distinguish ?(skip_outer_exists=false) strucs1 strucs2 = 
+let distinguish ?(how=Guarded) ?(skip_outer_exists=false) strucs1 strucs2 = 
   if !debug_level > 0 then
     Printf.printf "distinguishing:\n\n%s\n\n and\n\n %s\n%!" 
       (String.concat "\n" (List.map Structure.str strucs1))
@@ -173,7 +212,7 @@
   let rec diff qr k =
     if qr > k then diff 0 (k+1) else (
       if !debug_level > 0 then Printf.printf "distinguish qr %i k %i\n%!" qr k;
-      match distinguish_by_type ~skip_outer_exists ~qr ~k strucs1 strucs2 with
+      match distinguish_by_type ~how ~skip_outer_exists ~qr ~k strucs1 strucs2 with
 	| Some f -> f
 	| None -> diff (qr+1) k
     ) in

Modified: trunk/Toss/Solver/Distinguish.mli
===================================================================
--- trunk/Toss/Solver/Distinguish.mli	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Solver/Distinguish.mli	2011-11-10 01:26:59 UTC (rev 1625)
@@ -1,12 +1,21 @@
 (** Distinguish sets of structures by formulas. *)
 
-(** {2 Atoms} *)
+type distinguish_method = Types | Guarded
 
+
+(** {2 Atoms and FO Types} *)
+
 (** 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 -> Formula.formula list
 
+(** The [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+val ntype: Structure.structure -> int -> int array -> Formula.formula
 
+(** All types of rank [qr] of all [k]-tuples in [struc]. *)
+val ntypes: Structure.structure -> qr: int -> k:int -> Formula.formula list
+
+
 (** {2 Guards and Guarded Types} *)
 
 (** Generate all guarded substitutions of [tuple] with the guards.
@@ -36,10 +45,11 @@
 
 (** {2 Distinguishing Structure Sets} *)
 
-val distinguish_by_type: ?skip_outer_exists: bool -> qr: int -> k: int ->
-  Structure.structure list -> Structure.structure list -> Formula.formula option
+val distinguish_by_type: ?how: distinguish_method -> ?skip_outer_exists: bool ->
+  qr: int -> k: int -> Structure.structure list -> Structure.structure list ->
+  Formula.formula option
     
-val distinguish: ?skip_outer_exists: bool -> 
+val distinguish: ?how: distinguish_method -> ?skip_outer_exists: bool ->
   Structure.structure list -> Structure.structure list -> Formula.formula
 
 

Modified: trunk/Toss/Solver/DistinguishTest.ml
===================================================================
--- trunk/Toss/Solver/DistinguishTest.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Solver/DistinguishTest.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -48,6 +48,45 @@
 	(Formula.And (atoms struc [|2; 3|]));
     );
 
+  "ntype" >::
+    ( fun () ->
+      let structure = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_eq ("R(x0, x1) and not R(x0, x0) and not x0=x1 and " ^
+		     "not R(x1, x0) and not R(x1, x1)") 
+	(Distinguish.ntype structure 0 [|1; 2|]);
+      formula_eq ("(R(x0,x1) and not R(x0,x0) and x0!=x1 and not R(x1,x0) and "^
+		     "not R(x1, x1) and ex x0 (R(x0, x1) and not R(x0, x0) " ^
+		     "and not x0 = x1 and not R(x1, x0) and not R(x1, x1)) " ^
+		     "and ex x0 (x0 = x1 and not R(x0, x0) and not R(x0, x1) " ^
+		     "and not R(x1,x0) and not R(x1,x1)) and ex x1(R(x0,x1) " ^ 
+		     "and not R(x0, x0) and not x0 = x1 and not R(x1, x0) " ^
+		     "and not R(x1,x1)) and ex x1 (x0=x1 and not R(x0, x0) " ^
+		     "and not R(x0, x1) and not R(x1, x0) and not R(x1, x1))" ^
+		     " and all x0 ((R(x0,x1) and not R(x0,x0) and x0!=x1 and " ^
+		     "not R(x1, x0) and not R(x1, x1)) or (x0 = x1 and " ^
+		     "not R(x0, x0) and not R(x0, x1) and not R(x1, x0) and " ^
+		     "not R(x1,x1))) and all x1 ((R(x0, x1) and not R(x0, x0)" ^
+		     " and not x0 = x1 and not R(x1, x0) and not R(x1, x1)) " ^
+		     "or (x0 = x1 and not R(x0, x0) and not R(x0, x1) " ^
+		     "and not R(x1, x0) and not R(x1, x1))))")
+	(Distinguish.ntype structure 1 [|1;2|]);
+    );
+
+  "ntypes" >::
+    (fun () ->
+      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      formula_list_eq
+	[("R(x0, x1) and not R(x0, x0) and not x0 = x1 and " ^ 
+	     "not R(x1, x0) and not R(x1, x1)");
+	 ("R(x1, x0) and not R(x0, x0) and not R(x0, x1) and " ^
+	     "not x0 = x1 and not R(x1, x1)");
+	 ("x0 = x1 and not R(x0, x0) and not R(x0, x1) and " ^
+	     "not R(x1, x0) and not R(x1, x1)");
+	 ("not R(x0, x0) and not R(x0, x1) and not x0 = x1 and " ^ 
+	     "not R(x1, x0) and not R(x1, x1)")]
+	(Distinguish.ntypes structure ~qr:0 ~k:2);
+    );
+
   "guards" >::
     (fun () ->
       let struc = struc_of_string "[ | R { (1, 2); (2, 3) } | ]" in
@@ -121,15 +160,24 @@
       let lits = "R(x0,x1) and not R(x0,x0) and not x0=x1 and not R(x1,x0) " ^ 
 	"and not R(x1,x1)" in
       formula_eq lits (guarded_type struc 0 [|1; 2|]);
-      formula_eq lits (guarded_type struc 1 [|1; 2|]); (* no guards *)
-      formula_eq lits (guarded_type struc 2 [|1; 2|]); (* no guards *)
+      formula_eq (lits ^ " and all x0 not R(x1, x0) and all x1 not R(x1, x0) " ^
+		    "and all x0 (not R(x0, x1) or (not R(x0, x0) and " ^ 
+		    "not x0 = x1 and not R(x1, x0) and not R(x1, x1))) and " ^
+		    "all x1 (not R(x0, x1) or (not R(x0, x0) and not x0 = x1" ^
+		    " and not R(x1, x0) and not R(x1, x1)))")
+	(guarded_type struc 1 [|1; 2|]);
 
       let struc = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
       formula_eq lits (guarded_type struc 0 [|1; 2|]);
-      formula_eq (lits ^ " and ex x0 (R(x1, x0) and not R(x0, x0) and " ^ 
-		    "not R(x0, x1) and not x0 = x1 and not R(x1, x1)) and " ^
-		    "all x0 (not R(x1, x0) or (not R(x0, x0) and not R(x0,x1)" ^
-		    " and not x0 = x1 and not R(x1, x1)))")
+      formula_eq (lits ^ " and all x1 not R(x1, x0) and " ^
+		    "ex x0 (R(x1, x0) and not R(x0, x0) and not R(x0, x1) and" ^
+		    " not x0 = x1 and not R(x1, x1)) and " ^
+		    "all x0 (not R(x0, x1) or (not R(x0, x0) and not x0 = x1" ^
+		    " and not R(x1, x0) and not R(x1, x1))) and " ^
+		    "all x0 (not R(x1, x0) or (not R(x0, x0) and not R(x0, x1)"^
+		    " and not x0 = x1 and not R(x1, x1))) and " ^
+		    "all x1 (not R(x0, x1) or (not R(x0, x0) and not x0 = x1" ^
+		    " and not R(x1, x0) and not R(x1, x1)))")
 	(guarded_type struc 1 [|1; 2|]);
     );
 
@@ -168,9 +216,12 @@
 	(Distinguish.distinguish_by_type ~qr:2 ~k:1 [struc1] [struc2]);
       formula_option_eq "None" (* we use guarded types - so None here *)
 	(Distinguish.distinguish_by_type ~qr:0 ~k:2 [struc1] [struc2]);
+      formula_option_eq "not R(x0, x1) and not x0 = x1 and not R(x1, x0)"
+	(Distinguish.distinguish_by_type ~how:Types ~skip_outer_exists:true
+	   ~qr:0 ~k:2 [struc1] [struc2]);
       formula_option_eq "None" (* we use guarded types - so None here *)
 	(Distinguish.distinguish_by_type ~qr:0 ~k:3 [struc1] [struc2]);
-      formula_option_eq "R(x0, x1) and ex x2 R(x1, x2)" 
+      formula_option_eq "R(x0, x1) and ex x2 R(x2, x0)"
 	(Distinguish.distinguish_by_type ~skip_outer_exists:true ~qr:1 ~k:2
 	   [struc1] [struc2]);
 
@@ -184,12 +235,27 @@
     (fun () ->
       let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
       let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
-      formula_eq "ex x0, x1 (R(x0, x1) and ex x2 R(x1, x2))"
+      formula_eq "ex x0, x1 (R(x0, x1) and ex x2 R(x2, x0))"
 	(Distinguish.distinguish [struc1] [struc2]);
 
       let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
       let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
       formula_eq "ex x0 P(x0)" (Distinguish.distinguish [struc1] [struc2]);
+
+      let struc1 = struc_of_string "[  |  |  ] \"
+	...
+	...
+	...
+	P..
+\"" in
+      let struc2 = struc_of_string "[  |  |  ] \"
+	...
+	P..
+	...
+	...
+\"" in
+      formula_eq "ex x0, x1 (P(x0) and C(x0, x1))" 
+	(Distinguish.distinguish [struc1] [struc2]);
     );
 ]
 
@@ -233,6 +299,7 @@
 	    "ex x2 (P(x2) and R(x2, x1)) and ex x2 (C(x1, x2) and not P(x2))")
 	(Distinguish.distinguish ~skip_outer_exists:true 
 	   [strucP] [strucN1; strucN2; strucN3]);
+      assert true;
     );
 
   "breakthrough" >::
@@ -272,9 +339,9 @@
 	   ...   ...   ...   W..
 	...   ...   ...   ...   
 	...W  ...   ...   ...   
-\"" in 
-      Distinguish.set_debug_level 1;
-      formula_eq "W(x2) and all x3 not C(x2, x3)"
+\"" in (* "W(x2) and all x3 not C(x2, x3)" *)
+      (* Distinguish.set_debug_level 1; *)
+      formula_eq "W(x0) and R(x0, x1) and all x2 not C(x1, x2)"
 	(Distinguish.distinguish ~skip_outer_exists:true [struc1] [struc2]);
     );
 ]

Deleted: trunk/Toss/Solver/WL.ml
===================================================================
--- trunk/Toss/Solver/WL.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Solver/WL.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -1,255 +0,0 @@
-open Formula
-
-let debug_level = ref 0
-let set_debug_level i = (debug_level := i)
-
-(* 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 the intersection and after this greedily unused elements if
-   the option [greedy_cleanup] is set. *)
-let rec separate ?(cmp = Pervasives.compare) ?(greedy_cleanup = true) a =
-  let nonempty_intersect l1 l2 = 
-    if l1 = [] then l2 else if l2 = [] then l1 else Aux.sorted_inter l1 l2 in
-  let no_intersect arr =
-    let sorted = Array.map Aux.unique_sorted arr in
-    let inter = Array.fold_left nonempty_intersect sorted.(0) sorted in
-    Array.map (fun x -> Aux.list_diff x inter) arr in
-  let cleanup arr = 
-    let suffices orig l i = Aux.array_for_alli (
-      fun j lst -> j = i || lst = orig ||
-	List.exists (fun x -> not (List.mem x a.(j))) l) arr in
-    let rec filter orig i acc rest =
-      if rest = [] || suffices orig acc i then acc else
-	filter orig i ((List.hd rest)::acc) (List.tl rest) in
-    Array.mapi (fun i l -> filter l i [] (List.sort cmp l)) arr in
-  let rec rec_cleanup arr = 
-    let new_arr = cleanup arr in 
-    if new_arr = arr then arr else rec_cleanup new_arr in
-  if Array.length a = 0 then a else
-    let b = no_intersect a in
-    if greedy_cleanup then rec_cleanup b else b
-    
-
-(* Call the separate function from above on an array of conjunctions. *)
-let separate_conjs greedy conjs = 
-  separate ~cmp:Formula.compare ~greedy_cleanup:greedy 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 =
-    (Solver.M.evaluate_partial structure assignment phi) in
-  let elems = Assignments.set_to_set_list (Structure.elems structure) in
-  let assignment = if tuple = [||] then AssignmentSet.Any else
-      Assignments.assignments_of_list elems
-	(Array.map fo_var_of_string variables) [tuple] in
-  eval structure formula assignment <> AssignmentSet.Empty
-
-(* The list of literals which hold for a tuple on a structure,
-   i.e. the atomic type of this tuple. *)
-let atoms structure tuple variables_in =
-  let variables = (Array.sub variables_in 0 (Array.length tuple)) in
-  let rec inequalities vars = match vars with
-    head::tail -> List.append (List.map (fun x -> Eq (`FO head,`FO x) ) tail) 
-      (inequalities tail)
-    | _ -> [] in
-  let listOfLiterals = FormulaOps.atoms (Structure.rel_signature structure)
-    (Array.to_list variables) in
-  List.map (fun literal ->
-    if check structure tuple variables literal then literal else (Not literal)
-  ) (List.append listOfLiterals (inequalities (Array.to_list variables)))
-
-let range k = Aux.range ~from:1 (k+1)
-
-(* The n-type from FO^k for the [tuple] in [structure]. *)
-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)) (range k)) in
-  if n=0 then 
-    Formula.flatten_sort (And (atoms structure tuple (Array.of_list variables)))
-  else
-    let elements = Structure.elements structure in
-    if m < k then (* tuple shorter than variables, append one *)
-      let x_new = `FO ("x"^(string_of_int((Array.length tuple)+1))) in
-      let conj_b_ex_xmplus1_typesN structure tuple k n =
-	And ( List.map (fun x -> 
-	  Ex ([x_new], ntype structure (Array.append tuple [|x|]) k n)
-	) elements) in
-      let all_xmplus1_disj_b_typesN structure tuple k n =
-	All ([x_new], (Or (List.map (fun x -> 
-	  ntype structure (Array.append tuple [|x|]) k n) elements ) )) in
-      Formula.flatten_sort (And [
-	(ntype structure tuple k (n-1));
-	(conj_b_ex_xmplus1_typesN structure tuple k (n-1));
-	(all_xmplus1_disj_b_typesN structure tuple k (n-1))])
-    else (* all variables already used, substitute *)
-      let indices = range k in
-      let substituted i e = (Aux.array_replace tuple (i-1) e) in
-      let conj_b_ex_xi_typesN_replace_ai_by_b structure tuple k n i =
-	And (List.map (fun x -> 
-	  Ex ([`FO ("x"^(string_of_int i))],
-	      (ntype structure (substituted i x) k n))
-	) elements) in
-      let all_xi_disj_b_typesN_replace_ai_by_b structure tuple k n i=
-	All ([`FO ("x"^(string_of_int i))],
-	     ( Or (List.map (fun x -> 
-	       (ntype structure (substituted i x) k n)) elements ))) in
-      Formula.flatten_sort (And [
-	(ntype structure tuple k (n-1));
-	(And ( (List.map (fun i ->
-	  (And [(conj_b_ex_xi_typesN_replace_ai_by_b structure tuple k (n-1) i);
-		(all_xi_disj_b_typesN_replace_ai_by_b structure tuple k (n-1) i)
-	       ])) indices )))])
-
-let rec all_ntypes_ktuples ?(acc_types=[]) ?(tuples=None) structure n k =
-  let elements = Structure.elements structure in
-  let tuples = match tuples with Some tp -> tp | None ->
-    List.map Array.of_list (Aux.all_ntuples elements k) in
-  match tuples with 
-    | head::tail ->
-      let ntyp = (ntype structure head k n) in
-      let vars = (List.map (fun i -> "x"^string_of_int i) (range k)) in
-      let check tuple = check structure tuple (Array.of_list vars) ntyp in
-      let filtered = List.filter (fun t -> not (check t)) tail in
-      (all_ntypes_ktuples ~acc_types:(ntyp::acc_types)
-	 ~tuples:(Some filtered) structure n k)
-    | _ -> acc_types 
-
-
-(* --- WITH SIMPLIFICATION --- *)
-
-let atoms_simplified ?(min=true) structure tuples variables =
-  let tlist = Array.map (fun tuple -> 
-    Aux.unique_sorted (atoms structure tuple variables)) tuples in
-  let tlistF = 
-    if min then separate_conjs (Array.length tuples < 80) tlist else tlist in
-  let tuplesTable = Hashtbl.create 7 in
-  Array.iteri (fun i tuple->  
-    Hashtbl.add tuplesTable tuple (Formula.flatten_sort (And (tlistF.(i))))
-  ) tuples;
-  tuplesTable
-
-let nextTypes ?(min=true) structure tuples variables types =
-  let conjuncts tuple = 
-    let indices = range (Array.length tuple) 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 all_diff i = Array.to_list (Aux.array_mapi_some (
-      fun j v -> if j = i then None else 
-	  Some (Not (Eq (fo_var_of_string variables.(i), fo_var_of_string variables.(j))))
-    ) variables) in
-    let all_eq i = List.map (function Not f-> f | _-> failwith "neq") (all_diff i) in
-    let conj_b_ex_xi_typesN_replace_ai_by_b structure tuple i =
-      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))], 
-		    And ( (Hashtbl.find types subst) :: (all_diff (i-1)))))
-      ) (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 ((all_eq (i-1)) @ 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 = if min then separate_conjs false tlist else tlist in
-  let tuplesTable = Hashtbl.create 7 in
-  Array.iteri (fun i tuple->  
-    Hashtbl.add tuplesTable tuple (Formula.flatten_sort (And (tlistF.(i))))
-  ) tuples;
-  tuplesTable
-
-let rec ntypesSimplified ?(min=true) ?cur_types tuples variables structure n k =
-  let x, types = match cur_types with 
-    | Some (step, typs) -> (step, typs) 
-    | None -> (0, atoms_simplified ~min structure tuples variables) in
-  if x >= n then types else 
-    ntypesSimplified 
-      ~cur_types:(x+1, nextTypes ~min structure tuples variables types)
-      tuples variables structure n k
-
-let rec all_ntypes_simplified ?(min=true) 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 (range k)) in
-  ntypesSimplified ~min 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 ?(min=true) ?(skip_outer_exists=false) ~qr ~k sPos sNeg=
-  let listht table = Hashtbl.fold (fun x y z -> y :: z) table [] in
-  let types s= Aux.unique_sorted (listht (all_ntypes_simplified ~min s qr k)) in
-  let (tpPos, tpNeg) = (List.map types sPos, List.map types sNeg) 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 fails_neg f = (* check whether f fails on all negative structs *)
-    let f = And (f :: (all_diff (FormulaSubst.free_vars f))) in
-    not (List.exists (fun s -> check s [||] [||] f) sNeg) in
-  let succ_pos fl = (* check whether disjunction of fl holds on all positives *)
-    let f = And ((Or fl) :: (all_diff (FormulaSubst.free_vars (Or fl)))) in
-    List.for_all (fun s -> check s [||] [||] f) sPos in
-  let candidates = List.rev_append (List.concat tpPos) 
-    (List.map (fun f -> Not f) (List.concat tpNeg)) in
-  let fail_neg = List.filter fails_neg (Aux.unique_sorted candidates) in
-  let phis = List.sort Formula.compare (Aux.unique_sorted fail_neg) in
-  let rec find_type acc = function
-    | [] -> []
-    | x :: xs -> if succ_pos (x::acc) then x :: acc else 
-	find_type (x::acc) xs in
-  let dtypes = find_type [] phis in
-  if dtypes = [] then None else
-    let is_ok f = fails_neg f && succ_pos [f] in
-    let mintp = greedy_remove is_ok (Or dtypes) in
-    let fv = FormulaSubst.free_vars (Or dtypes) 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))
-
-let distinguish ?(skip_outer_exists=false) strucs1 strucs2 = 
-  if !debug_level > 0 then
-    Printf.printf "distinguishing:\n\n%s\n\n and\n\n %s\n%!" 
-      (String.concat "\n" (List.map Structure.str strucs1))
-      (String.concat "\n" (List.map Structure.str strucs2));
-  let rec diff qr k =
-    if qr > k then diff 0 (k+1) else (
-      if !debug_level > 0 then Printf.printf "distinguish qr %i k %i\n%!" qr k;
-      match distinguish_by_type ~skip_outer_exists ~qr ~k strucs1 strucs2 with
-	| Some f -> f
-	| None -> match distinguish_by_type ~min:false ~skip_outer_exists 
-	    ~qr ~k strucs1 strucs2 with 
-	      | Some f -> f 
-	      | None -> diff (qr+1) k
-    ) in
-  diff 0 1

Deleted: trunk/Toss/Solver/WL.mli
===================================================================
--- trunk/Toss/Solver/WL.mli	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Solver/WL.mli	2011-11-10 01:26:59 UTC (rev 1625)
@@ -1,43 +0,0 @@
-(** 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 the intersection and after this greedily unused elements if
-    the option [greedy_cleanup] is set. *)
-val separate: ?cmp: ('a -> 'a -> int) -> ?greedy_cleanup: bool ->
-  '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 ->
-  Formula.formula list
-
-(** The n-type from FO^k for the given int tuple in the structure. *)
-val ntype: Structure.structure -> int array -> int -> int -> Formula.formula
-
-(** All n-types from FO^k for the given structure, with accumulators. *)
-val all_ntypes_ktuples: ?acc_types: Formula.formula list ->
-  ?tuples: int array list option ->
-  Structure.structure -> int -> int ->  Formula.formula list
-
-val atoms_simplified: ?min:bool -> Structure.structure -> int array array ->
-  string array -> (int array,Formula.formula) Hashtbl.t 
-
-val all_ntypes_simplified: ?min:bool -> Structure.structure -> int -> int -> 
-  (int array, Formula.formula) Hashtbl.t 
-
-(** Distinguish two structures using n-types from FO^k, a bit minimized. *)
-val distinguish_by_type: ?min:bool -> ?skip_outer_exists: bool ->
-  qr: int -> k: int ->
-  Structure.structure list -> Structure.structure list -> Formula.formula option
-
-(** Distinguish two structures. *)
-val distinguish: ?skip_outer_exists: bool -> 
-  Structure.structure list -> Structure.structure list -> Formula.formula
-
-
-(** {2 Debugging} *)
-
-val set_debug_level: int -> unit

Deleted: trunk/Toss/Solver/WLTest.ml
===================================================================
--- trunk/Toss/Solver/WLTest.ml	2011-11-08 09:44:53 UTC (rev 1624)
+++ trunk/Toss/Solver/WLTest.ml	2011-11-10 01:26:59 UTC (rev 1625)
@@ -1,244 +0,0 @@
-open OUnit
-
-let formula_of_string s = 
-  FormulaParser.parse_formula Lexer.lex (Lexing.from_string s)
-
-let struc_of_string s = 
-  StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
-
-let formula_eq ?(flatten_sort=true) phi1 phi2 =
-  if flatten_sort then 
-    assert_equal ~printer:(fun x -> Formula.sprint x)
-      (Formula.flatten_sort (formula_of_string phi1))
-      (Formula.flatten_sort phi2)
-  else
-    assert_equal ~printer:(fun x -> Formula.sprint x)
-      (formula_of_string phi1) phi2
-
-let formula_list_eq ?(flatten_sort=true) l1 l2 =
-  List.iter2 (formula_eq ~flatten_sort) l1 l2
-
-let formula_option_eq ?(flatten_sort=true) fopt1 fopt2 =
-  let fopt_str = function None -> "None" | Some f -> Formula.str f in
-  if fopt1 = "None" then 
-    assert_equal ~printer:fopt_str None fopt2 
-  else match fopt2 with
-    | 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]; [3] |]
-	(WL.separate [| [1;2]; [2;3] |]);
-      assert_equal ~printer:str [| [1]; [3] |]
-	(WL.separate [| [1;2]; [2;3] |]);
-      assert_equal ~printer:str [| [3;1]; [-3]; [-1] |]
-	(WL.separate [| [1;2;3;4]; [1;2;-3;4]; [-1;2;3;4] |]);
-      assert_equal ~printer:str [| [3;1]; [-3]; [-1] |]
-	(WL.separate [|[1;2;3;4]; [1;2;-3;4]; [-1;2;3;4]|]);
-    );
-
-  "atoms" >::
-    (fun () ->
-      let variables = ["x1";"x2"] in
-      let structure = struc_of_string "[ | R { (1, 2); (2, 3) } | ]" in
-      formula_eq
-        "(not R(x1, x1) and R(x1, x2) and not R(x2, x1) and not R(x2, x2) and not x1=x2)" 
-	(Formula.And (WL.atoms structure [|2; 3|] (Array.of_list variables)));
-    );
-
-  "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
-        ex x1 (x1 = x2 and not R(x1, x1) and not R(x1, x2) and not R(x2, x1) and not R(x2, x2)) and
-        ex x2 (R(x1, x2) and not R(x1, x1) and not x1 = x2 and not R(x2, x1) and not R(x2, x2)) and
-        ex x2 (x1 = x2 and not R(x1, x1) and not R(x1, x2) and not R(x2, x1) and not R(x2, x2)) and
-        all x1 ((R(x1, x2) and not R(x1, x1) and not x1 = x2 and not R(x2, x1) and not R(x2, x2)) or
-        (x1 = x2 and not R(x1, x1) and not R(x1, x2) and not R(x2, x1) and not R(x2, x2))) and
-        all x2 ((R(x1, x2) and not R(x1, x1) and not x1 = x2 and not R(x2, x1) and not R(x2, x2)) or
-        (x1 = x2 and not R(x1, x1) and not R(x1, x2) and not R(x2, x1) and not R(x2, x2))))"
-	(WL.ntype structure [|1;2|] 2 1);
-
-      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 x3 (R(x1, x2) and R(x1, x3) and x2 = x3 and not R(x1, x1) and not x1 = x2 and not x1 = x3 and not R(x2, x1) and not R(x2, x2) and not R(x2, x3) and not R(x3, x1) and not R(x3, x2) and not R(x3, x3)) and
-        ex x3 (R(x1, x2) and x1 = x3 and R(x3, x2) and not R(x1, x1) and not x1 = x2 and not R(x1, x3) and not R(x2, x1) and not R(x2, x2) and not R(x2, x3) and not x2 = x3 and not R(x3, x1) and not R(x3, x3)) and
-        all x3 ((R(x1, x2) and R(x1, x3) and x2 = x3 and not R(x1, x1) and not x1 = x2 and not x1 = x3 and not R(x2, x1) and not R(x2, x2) and not R(x2, x3) and not R(x3, x1) and not R(x3, x2) and not R(x3, x3)) or
-        (R(x1, x2) and x1 = x3 and R(x3, x2) and not R(x1, x1) and not x1 = x2 and not R(x1, x3) and not R(x2, x1) and not R(x2, x2) and not R(x2, x3) and not x2 = x3 and not R(x3, x1) and not R(x3, x3))))"
-	(WL.ntype structure [|1;2|] 3 1);
-    );
-
-  "all_ntypes" >::
-    (fun () ->
-      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
-      formula_list_eq
-	["(R(x2, x1) and not R(x1, x1) and not R(x1, x2) and not x1 = x2 and not R(x2, x2))";
-	 "(not R(x1, x1) and not R(x1, x2) and not R(x2, x1) and not R(x2, x2) and not x1=x2)";
-	 "(not R(x1, x1) and R(x1, x2) and not R(x2,x1) and not R(x2,x2) and not x1=x2)";
-         "(not R(x1,x1) and not R(x1,x2) and not R(x2,x1) and not R(x2,x2) and x1=x2)"]
-	(WL.all_ntypes_ktuples structure 0 2);
-    );
-
-  "atoms_simplified" >::
-    (fun () ->
-      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
-      hashtbl_eq structure 
-	[ ([|1;2|], "R(x1, x2)"); ([|3;3|], "x1 = x2") ]
-	(WL.atoms_simplified structure [| [| 1;2 |]; [|3;3|] |] [|"x1";"x2"|]);
-    );
-
-  "all_ntypes_simplified" >::
-    (fun () ->
-      let structure = (struc_of_string "[ | R { (1, 2) } | ]") in
-      hashtbl_eq structure 
-	[ ([|1;2|], "R(x1, x2)");
-	  ([|2;1|], "R(x2, x1)")]
-	(WL.all_ntypes_simplified structure 0 2);
-      let structure = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
-      hashtbl_eq structure 
-	[ ([|1;2|], "R(x1, x2)");
-	  ([|2;1|], "R(x2, x1)");
-	  ([|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)")]
-	(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 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 "not R(x1, x2) and not R(x2, x1)" 
-	(WL.distinguish_by_type ~skip_outer_exists:true ~qr:1 ~k:2
-	   [structure1] [structure2]);
-
-      let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
-      let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
-      formula_option_eq "ex x1 P(x1)" 
-	(WL.distinguish_by_type ~min:false ~qr:0 ~k:1 [struc1] [struc2]);
-    );
-
-  "distinguish" >::
-    (fun () ->
-      let structure1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
-      let structure2 = (struc_of_string "[ | R { (1, 2) } | ]") in
-      formula_eq "ex x1, x2 (not R(x1, x2) and not R(x2, x1))"
-	(WL.distinguish [structure1] [structure2]);
-
-      let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
-      let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
-      formula_eq "ex x1 P(x1)" (WL.distinguish [struc1] [struc2]);
-    );
-]
-
-let bigtests = "WLBig" >::: [
-  "distinguish" >::
-    (fun () ->
-      let strucN1 = struc_of_string "[  |  |  ] \"
-	...   ...
-	...   P..
-	   ...   
-	   P..   
-	...   ...
-	...P  ...
-\"" in
-      let strucN2 = struc_of_string "[  |  |  ] \"
-	...   ...
-	...P  ...
-	   ...   
-	   ...   
-	...   ...
-	...P  ...
-\"" in
-      let strucN3 = struc_of_string "[  |  |  ] \"
-	...   ...
-	...P  ...
-	   ...   
-	   P..   
-	...   ...
-	...   ...
-\"" in
-      let strucP = struc_of_string "[  |  |  ] \"
-	...   ...
-	...P  ...
-	   ...   
-	   P..   
-	...   ...
-	...P  ...
-\"" in
-      formula_eq 
-	"P(x2) and ex x3 (P(x3) and C(x2, x3)) and ex x3 (P(x3) and C(x3, x2))"
-	(WL.distinguish ~skip_outer_exists:true 
-	   [strucP] [strucN1; strucN2; strucN3]);
-
-      let struc1 = struc_of_string "[  |  |  ] \"
-	   ...   ...   ...   ...
-	   ...   W..   ...B  ...
-	...   ...   ...   ...   
-	...   ...   ...   B..   
-	   ...   ...   ...   ...
-	   ...   ...   ...   ...
-	...   ...   ...   ...   
-	...   ...   ...   ...   
-	   ...   ...   ...   ...
-	   ...   ...   ...   ...
-	...   ...   ...   ...   
-	...   ...   ...   ...   
-	   ...   ...   ...   ...
-	   ...   ...   ...   W..
-	...   ...   ...   ...   
-	...W  ...   ...   ...   
-\"" in
-      let struc2 = struc_of_string "[  |  |  ] \"
-	   ...   ...   ...   ...
-	   ...   ...   ...B  ...
-	...   ...   ...   ...   
-	...   ...W  ...   B..   
-	   ...   ...   ...   ...
-	   ...   ...   ...   ...
-	...   ...   ...   ...   
-	...   ...   ...   ...   
-	   ...   ...   ...   ...
-	   ...   ...   ...   ...
-	...   ...   ...   ...   
-	...   ...   ...   ...   
-	   ...   ...   ...   ...
-	   ...   ...   ...   W..
-	...   ...   ...   ...   
-	...W  ...   ...   ...   
-\"" in assert true;
-    formula_eq "W(x2) and all x3 not C(x2, x3)"
-      (WL.distinguish ~skip_outer_exists:true [struc1] [struc2]);
-    );
-]

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