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

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

Revision: 1640
          http://toss.svn.sourceforge.net/toss/?rev=1640&view=rev
Author:   lukaszkaiser
Date:     2012-01-16 14:23:37 +0000 (Mon, 16 Jan 2012)
Log Message:
-----------
Tidy up: moving learning things to Learn.

Modified Paths:
--------------
    trunk/Toss/Makefile
    trunk/Toss/Server/ReqHandler.ml
    trunk/Toss/Server/Tests.ml

Added Paths:
-----------
    trunk/Toss/Learn/Distinguish.ml
    trunk/Toss/Learn/Distinguish.mli
    trunk/Toss/Learn/DistinguishTest.ml
    trunk/Toss/Learn/LearnGame.ml
    trunk/Toss/Learn/LearnGame.mli
    trunk/Toss/Learn/LearnGameTest.ml

Removed Paths:
-------------
    trunk/Toss/Server/LearnGame.ml
    trunk/Toss/Server/LearnGame.mli
    trunk/Toss/Server/LearnGameTest.ml
    trunk/Toss/Solver/Distinguish.ml
    trunk/Toss/Solver/Distinguish.mli
    trunk/Toss/Solver/DistinguishTest.ml

Copied: trunk/Toss/Learn/Distinguish.ml (from rev 1639, trunk/Toss/Solver/Distinguish.ml)
===================================================================
--- trunk/Toss/Learn/Distinguish.ml	                        (rev 0)
+++ trunk/Toss/Learn/Distinguish.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -0,0 +1,269 @@
+open Formula
+
+let debug_level = ref 0
+let set_debug_level i = (debug_level := i)
+
+type logic = FO | GuardedFO
+
+
+(* Helper functions to construct variables for indices. *)
+let varname i = "x" ^ string_of_int i
+let varnames k = List.map varname (Aux.range k)
+let var i = var_of_string (varname i)
+let fo_var i = fo_var_of_string (varname i)
+
+(* Helper function: check if a formula holds for a tuple on a structure. *)
+let check structure tuple 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 vars =Array.map fo_var (Array.of_list (Aux.range (Array.length tuple))) in
+  let assignment = if tuple = [||] then AssignmentSet.Any else
+      Assignments.assignments_of_list elems vars [tuple] in
+  eval structure formula assignment <> AssignmentSet.Empty
+
+(* - Atoms and FO Types - *)
+
+(* The list of literals which hold for a tuple on a structure. *)
+let atoms struc tuple =
+  let k = Array.length tuple in
+  let rec equalities = function
+    | [] -> []
+    | v :: vs -> (List.map (fun x -> Eq (`FO v,`FO x)) vs) @ (equalities vs) in
+  let atoms = FormulaOps.atoms (Structure.rel_signature struc) (varnames k) in
+  List.map (
+    fun atom -> if check struc tuple atom then atom else (Not atom)
+  ) (atoms @ (equalities (varnames k)))
+
+
+(* The [qr]-type in [length of tuple]-variables of [tuple] in [struc].
+   In [mem] we memorize the results for [qr] and [tuple], but *not* [struc]. *)
+let rec ntype_memo struc mem qr tuple =
+  try Hashtbl.find mem (qr, tuple) with Not_found ->
+    if qr = 0 then (
+      let res = Formula.flatten_sort (And (atoms struc tuple)) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    ) else (
+      let prevtp i e = 
+	ntype_memo struc mem (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
+      let res = Formula.flatten_sort (
+	And [ntype_memo struc mem (qr-1) tuple; nexttp]) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    )
+
+(* The [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+let ntype struc qr tuple = ntype_memo struc (Hashtbl.create 7) qr tuple
+
+
+(* 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
+  let mem = Hashtbl.create 63 in
+  Aux.unique_sorted (List.rev_map (ntype_memo struc mem qr) tups)
+
+
+(* - Guards and Guarded Types - *)
+
+(* Generate all guarded substitutions of [tuple] with the guards.
+   A subst-tuple is a substitution of [tuple] if it has the same length.
+   A subst-tuple is a guarded substitution of [tuple] if a permuted
+   sub-tuple of subst-tuple containig at least one element of
+   the original [tuple] is in some relation R in the structure [struc].
+   The guard for subst-tuple is then the atomic formula R(x_i1, ..., x_iK)
+   such that a = (subst-tuple_i1, ..., subst-tuple_iK) and R(a) holds.
+   For every subst-tuple as above we return the quintuple:
+   <new elems in subst-tuple, their indices as vars, subst-tuple, a, guard>. 
+   We do not generate subst-tuples with repeated new elements. *)
+let guards struc tuple =
+  let in_tuple e = Aux.array_mem e tuple in
+  let tuple = Array.to_list tuple in
+  let all_incident = List.concat (List.map (Structure.incident struc) tuple) in
+  let subst_tuples a = (* all subst-tuples for which [a] witnesses a guard *)
+    let new_in = 
+      Aux.unique_sorted (Aux.array_find_all (fun x -> not (in_tuple x)) a) in
+    let subst_tups = Aux.product (
+      List.map (fun e->if List.mem e new_in then new_in else e::new_in) tuple)in
+    let is_complete subst = 
+      List.for_all (fun e -> List.mem e subst) (Array.to_list a) in
+    let complete_new_once subst = is_complete subst && List.for_all (
+      fun n -> List.length (List.filter (fun x -> x = n) subst) = 1
+    ) new_in in
+    List.rev_map Array.of_list (List.filter complete_new_once subst_tups) in
+  let make_guard rel a stp =
+    let new_els = List.filter (fun x -> not (in_tuple x)) (Array.to_list stp) in
+    let sindex e = Aux.array_argfind (fun x -> x = e) stp in
+    let guard = Rel (rel, Array.map (fun e -> fo_var (sindex e)) a) in
+    let ret_els = Aux.unique_sorted new_els in
+    (ret_els, List.map (fun e -> var (sindex e)) ret_els, stp, a, guard) in
+  let make_guard rel a = List.rev_map (make_guard rel a) (subst_tuples a) in
+  let make_guard (rel, tps) = List.concat (List.rev_map (make_guard rel) tps) in
+  let guards = List.filter (fun (e,_,_,_,_) -> e <> []) 
+    (List.concat (List.rev_map make_guard all_incident)) in
+  Aux.unique_sorted guards
+
+(* Print a guard tuple, as returned above, to string. *)
+let guard_tuple_str (new_elems, vars, tup, a, atom) =
+  "< " ^ (String.concat ", " (List.map string_of_int new_elems)) ^ " | " ^
+    (String.concat ", " (List.map var_str vars)) ^ " | " ^
+    (String.concat ", " (List.map string_of_int (Array.to_list tup))) ^ " | " ^
+    (String.concat ", " (List.map string_of_int (Array.to_list a))) ^ " | " ^
+    (Formula.str atom) ^ " >"
+
+
+(* Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. 
+   In [mem] we memorize the results for [qr] and [tuple], but *not* [struc]. *)
+let rec guarded_type_memo struc mem qr tuple =
+  try Hashtbl.find mem (qr, tuple) with Not_found ->
+    if qr = 0 then (
+      let res = Formula.flatten_sort (And (atoms struc tuple)) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    ) else (
+      let prevtp tup = guarded_type_memo struc mem (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) = 
+	And [conj_prev_ex vs g ts; all_prev_disj vs g ts] in
+      let subst_tuples = 
+	List.rev_map (fun (_,vs,t,_,_) -> (vs, t)) (guards struc tuple) in
+      let subst_tuples = Aux.unique_sorted (([], tuple) :: subst_tuples) 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
+      let res = Formula.flatten_sort (
+	And [guarded_type_memo struc mem (qr-1) tuple; nextf]) in
+      Hashtbl.add mem (qr, tuple) res;
+      res
+    )
+
+(* Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+let guarded_type struc qr tuple = 
+  guarded_type_memo struc (Hashtbl.create 7) qr tuple
+
+
+(* All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
+let guarded_types struc ~qr ~k =
+  let tups = List.map (Structure.incident struc) (Structure.elements struc) in
+  let tups = List.concat (List.map snd (List.concat tups)) in
+  let tups = List.filter (fun tup -> Array.length tup >= k) tups in
+  let k_subtuples tup = 
+    List.map Array.of_list (Aux.all_ntuples (Array.to_list tup) k) in
+  let ktups = List.rev_map k_subtuples (Aux.unique_sorted tups) in
+  let ktups = Aux.unique_sorted (List.concat ktups) in
+  let mem = Hashtbl.create 63 in
+  Aux.unique_sorted (List.rev_map (guarded_type_memo struc mem qr) ktups)
+
+
+
+(* - Distinguishing Structure Sets - *)
+
+
+(* 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 ?(pos=false) 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 -> if pos then Or fl else
+	Or (greedy_remove_list (fun l -> Or l) [] (List.rev fl))
+    | Not f -> if pos then Not f else 
+	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
+
+(* Order on types that we use to select the minimal one. *)
+let compare_types tp1 tp2 = 
+  let tp_lits = function And fl -> List.filter Formula.is_literal fl | _-> [] in
+  let c = Formula.compare (And (tp_lits tp1)) (And (tp_lits tp2)) in
+  if c <> 0 then c else Formula.compare tp1 tp2
+
+let compare_types = ref compare_types
+
+(* Find the minimal [logic]-type of [struc] not included in [neg_types]
+   and with at most [qr] quantifiers and [k] variables. *)
+let min_type_omitting ?(logic = GuardedFO) ~qr ~k neg_types struc =
+  let pos_types = match logic with 
+    | GuardedFO -> guarded_types struc ~qr ~k 
+    | FO -> ntypes struc ~qr ~k in
+  let ok_types = List.filter (fun f -> not (List.mem f neg_types)) pos_types in
+  let ok_types = List.sort !compare_types ok_types in
+  if ok_types = [] then None else Some (List.hd ok_types)
+
+(* Find a [logic]-formula with at most [qr] quantifiers and [k] variables
+   which holds on all [pos_strucs] and on no [neg_strucs]. *)
+let distinguish_upto ?(logic = GuardedFO) ~qr ~k pos_strucs neg_strucs =
+  let types s = match logic with 
+    | GuardedFO -> guarded_types s ~qr ~k 
+    | FO -> ntypes s ~qr ~k in
+  let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
+  let fails_on_negs f = not (List.exists (fun s-> check s [||] f) neg_strucs) in
+  let extend_by_pos acc struc =
+    if check struc [||] (Or acc) then acc else 
+      match min_type_omitting ~logic ~qr ~k neg_tps struc with
+	| None -> raise Not_found
+	| Some f -> (greedy_remove ~pos:true fails_on_negs f) :: acc in
+  let pos_formulas = 
+    try List.fold_left extend_by_pos [] pos_strucs with Not_found -> [] in
+  let pos_formulas = Aux.unique_sorted ~cmp:!compare_types pos_formulas in
+  if pos_formulas = [] then None else
+    let succ_pos fl = List.for_all (fun s -> check s [||] (Or fl)) pos_strucs in
+    let is_ok f = fails_on_negs f && succ_pos [f] in
+    let minimized = greedy_remove is_ok (Or pos_formulas) in
+    let fv = FormulaSubst.free_vars minimized in
+    Some (FormulaOps.rename_quant_avoiding fv minimized)
+
+
+(* Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
+   Leaves free variables (existential) if [skip_outer_exists] is set. *)
+let distinguish ?(how=GuardedFO) ?(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_upto ~logic:how ~qr ~k strucs1 strucs2 with
+	| Some f -> 
+	  if skip_outer_exists then Some f else 
+	    Some (Ex (FormulaSubst.free_vars f, f))
+	| None -> diff (qr+1) k
+    ) in
+  diff 0 1

Copied: trunk/Toss/Learn/Distinguish.mli (from rev 1639, trunk/Toss/Solver/Distinguish.mli)
===================================================================
--- trunk/Toss/Learn/Distinguish.mli	                        (rev 0)
+++ trunk/Toss/Learn/Distinguish.mli	2012-01-16 14:23:37 UTC (rev 1640)
@@ -0,0 +1,71 @@
+(** Distinguish sets of structures by formulas. *)
+
+type logic = FO | GuardedFO
+
+
+(** {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.
+    A subst-tuple is a substitution of [tuple] if it has the same length.
+    A subst-tuple is a guarded substitution of [tuple] if a permuted
+    sub-tuple a of subst-tuple containig at least one element of
+    the original [tuple] is in some relation R in the structure [struc].
+    The guard for subst-tuple is then the atomic formula R(x_i1, ..., x_iK)
+    such that a = (subst-tuple_i1, ..., subst-tuple_iK) and R(a) holds.
+    For every subst-tuple as above we return the quintuple:
+    <new elems in subst-tuple, their indices as vars, subst-tuple, a, guard>. 
+    We do not generate subst-tuples with repeated new elements. *)
+val guards: Structure.structure -> int array -> 
+  (int list * Formula.var list * int array * int array * Formula.formula) list
+
+(** Print a guard tuple, as returned above, to string. *)
+val guard_tuple_str:
+  (int list * Formula.var list * int array * int array * Formula.formula) -> 
+  string
+
+(** Guarded [qr]-type in [length of tuple]-variables of [tuple] in [struc]. *)
+val guarded_type: Structure.structure -> int -> int array -> Formula.formula
+
+(** All guarded types of rank [qr] of guarded [k]-tuples in [struc]. *)
+val guarded_types: Structure.structure -> qr: int -> k:int -> 
+  Formula.formula list
+
+
+(** {2 Distinguishing Structure Sets} *)
+
+(** Order on types that we use to select the minimal ones. *)
+val compare_types : (Formula.formula -> Formula.formula -> int) ref
+
+(** Find the minimal [logic]-type of [struc] not included in [neg_types]
+    and with at most [qr] quantifiers and [k] variables. *)
+val min_type_omitting: ?logic: logic -> qr: int -> k: int ->
+  Formula.formula list -> Structure.structure -> Formula.formula option
+
+(** Find a [logic]-formula with at most [qr] quantifiers and [k] variables
+    which holds on all [pos_strucs] and on no [neg_strucs].
+    Leaves free variables which are implicitly quantified existentially. *)
+val distinguish_upto: ?logic: logic -> qr: int -> k: int ->
+  Structure.structure list -> Structure.structure list -> Formula.formula option
+
+(** Find a [logic]-formula holding on all [pos_strucs] and on no [neg_strucs].
+    Leaves free variables (existential) if [skip_outer_exists] is set. *)
+val distinguish: ?how: logic -> ?skip_outer_exists: bool ->
+  Structure.structure list -> Structure.structure list -> Formula.formula option
+
+
+(** {2 Debugging} *)
+
+val set_debug_level: int -> unit

Copied: trunk/Toss/Learn/DistinguishTest.ml (from rev 1639, trunk/Toss/Solver/DistinguishTest.ml)
===================================================================
--- trunk/Toss/Learn/DistinguishTest.ml	                        (rev 0)
+++ trunk/Toss/Learn/DistinguishTest.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -0,0 +1,342 @@
+open OUnit
+open Distinguish
+
+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 guards_eq res guards =
+  let guards_str gl = String.concat "\n" (List.map guard_tuple_str gl) in
+  assert_equal ~printer:(fun s -> s) res (guards_str guards)
+
+let formula_list_eq ?(flatten_sort=true) l1 l2 =
+  if List.length l1 = List.length l2 then
+    List.iter2 (formula_eq ~flatten_sort) l1 l2
+  else 
+    let lstr l = "Length " ^ (string_of_int (List.length l)) ^ 
+      " [ " ^ (String.concat " | " l) ^ " ]" in
+    assert_equal ~printer:lstr l1 (List.map Formula.str 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 tests = "Distinguish" >::: [
+  "atoms" >::
+    (fun () ->
+      let struc = struc_of_string "[ | R { (1, 2); (2, 3) } | ]" in
+      formula_eq
+        ("(not R(x0, x0) and R(x0, x1) and not R(x1, x0) " ^ 
+	    "and not R(x1, x1) and not x0=x1)")
+	(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
+      guards_eq "< 3 | x0 | 3, 2 | 2, 3 | R(x1, x0) >" (guards struc [|1; 2|]);
+      guards_eq ("< 2 | x0 | 2, 1 | 1, 2 | R(x1, x0) >\n" ^ 
+		    "< 2 | x1 | 1, 2 | 1, 2 | R(x0, x1) >")
+	(guards struc [|1; 1|]);
+      guards_eq ("< 1 | x0 | 1, 2 | 1, 2 | R(x0, x1) >\n" ^
+		    "< 1 | x1 | 2, 1 | 1, 2 | R(x1, x0) >\n" ^
+		    "< 3 | x0 | 3, 2 | 2, 3 | R(x1, x0) >\n" ^
+		    "< 3 | x1 | 2, 3 | 2, 3 | R(x0, x1) >")
+	(guards struc [|2; 2|]);
+      guards_eq ("< 2 | x0 | 2, 3 | 2, 3 | R(x0, x1) >\n" ^ 
+		    "< 2 | x1 | 1, 2 | 1, 2 | R(x0, x1) >")
+	(guards struc [|1; 3|]);
+      guards_eq ("< 2 | x0 | 2, 1 | 1, 2 | R(x1, x0) >\n" ^ 
+		    "< 2 | x1 | 3, 2 | 2, 3 | R(x1, x0) >")
+	(guards struc [|3; 1|]);
+      guards_eq "" (guards struc [|1|]);
+      guards_eq "" (guards struc [|2|]);
+      guards_eq "" (guards struc [|3|]);
+      guards_eq "" (guards struc [|1; 2; 3|]);
+
+      let struc = struc_of_string "[ | R { (1, 2); (2, 4) } | ]" in
+      guards_eq ("< 4 | x0 | 4, 2, 3 | 2, 4 | R(x1, x0) >\n" ^ 
+		    "< 4 | x2 | 1, 2, 4 | 2, 4 | R(x1, x2) >")
+	(guards struc [|1; 2; 3|]);
+
+      let struc = struc_of_string "[ | R { (1, 2, 2) } | ]" in
+      guards_eq ("< 2 | x0 | 2, 1 | 1, 2, 2 | R(x1, x0, x0) >\n" ^
+		    "< 2 | x1 | 1, 2 | 1, 2, 2 | R(x0, x1, x1) >")
+	(guards struc [|1; 1|]);
+
+      let struc = struc_of_string "[ | R { (1, 2, 3) } | ]" in
+      guards_eq "" (guards struc [|1; 1|]);
+      guards_eq "" (guards struc [|1; 2; 3|]);
+      guards_eq ("< 3 | x0 | 3, 1, 2 | 1, 2, 3 | R(x1, x2, x0) >\n" ^
+		    "< 3 | x1 | 1, 3, 2 | 1, 2, 3 | R(x0, x2, x1) >")
+	(guards struc [|1; 1; 2|]);
+      guards_eq ("< 2 | x0 | 2, 1, 3 | 1, 2, 3 | R(x1, x0, x2) >\n" ^
+		    "< 2 | x1 | 1, 2, 3 | 1, 2, 3 | R(x0, x1, x2) >")
+	(guards struc [|1; 1; 3|]);
+      guards_eq ("< 1 | x0 | 1, 2, 3 | 1, 2, 3 | R(x0, x1, x2) >\n" ^
+		    "< 1 | x2 | 3, 2, 1 | 1, 2, 3 | R(x2, x1, x0) >")
+	(guards struc [|3; 2; 3|]);
+      guards_eq ("< 1, 3 | x0, x1 | 1, 3, 2 | 1, 2, 3 | R(x0, x2, x1) >\n" ^
+		    "< 1, 3 | x0, x2 | 1, 2, 3 | 1, 2, 3 | R(x0, x1, x2) >\n" ^
+		    "< 1, 3 | x1, x0 | 3, 1, 2 | 1, 2, 3 | R(x1, x2, x0) >\n" ^
+		    "< 1, 3 | x1, x2 | 2, 1, 3 | 1, 2, 3 | R(x1, x0, x2) >\n" ^
+		    "< 1, 3 | x2, x0 | 3, 2, 1 | 1, 2, 3 | R(x2, x1, x0) >\n" ^
+		    "< 1, 3 | x2, x1 | 2, 3, 1 | 1, 2, 3 | R(x2, x0, x1) >")
+	(guards struc [|2; 2; 2|]);
+      
+      let struc = struc_of_string "[  |  |  ] \"
+	...   ...
+	...   P..
+	   ...   
+	   P..   
+	...   ...
+	...P  ...
+\"" in 
+      guards_eq ("< 3 | x0 | 3, 2 | 2, 3 | R(x1, x0) >\n" ^ 
+		    "< 4 | x1 | 1, 4 | 1, 4 | C(x0, x1) >\n" ^ 
+		    "< 5 | x0 | 5, 2 | 2, 5 | C(x1, x0) >") 
+	(guards struc [|1; 2|]);
+    );
+
+  "guarded_type" >::
+    (fun () ->
+      let struc = (struc_of_string "[ | R { (1, 2) } | ]") in
+      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 ^ " 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 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|]);
+    );
+
+  "guarded_types" >::
+    (fun () ->
+      let struc = (struc_of_string "[ | R { (1, 2) } | ]") 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))") ]
+        (Distinguish.guarded_types struc ~qr:0 ~k:2);
+      assert_equal ~printer:string_of_int 4
+	(List.length (Distinguish.guarded_types struc ~qr:1 ~k:2));
+
+      let struc = (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))") ]
+        (Distinguish.guarded_types struc ~qr:0 ~k:2);
+      assert_equal ~printer:string_of_int 7
+	(List.length (Distinguish.guarded_types struc ~qr:1 ~k:2));
+    );
+
+  "distinguish_upto" >::
+    (fun () ->
+      let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_option_eq "None" 
+	(Distinguish.distinguish_upto ~qr:2 ~k:1 [struc1] [struc2]);
+      formula_option_eq "None" (* we use guarded types - so None here *)
+	(Distinguish.distinguish_upto ~qr:0 ~k:2 [struc1] [struc2]);
+      formula_option_eq "not R(x0, x1) and not x0 = x1 and not R(x1, x0)"
+	(Distinguish.distinguish_upto ~logic:FO ~qr:0 ~k:2 [struc1] [struc2]);
+      formula_option_eq "None" (* we use guarded types - so None here *)
+	(Distinguish.distinguish_upto ~qr:0 ~k:3 [struc1] [struc2]);
+      formula_option_eq "R(x0, x1) and ex x2 R(x2, x0)"
+	(Distinguish.distinguish_upto ~qr:1 ~k:2 [struc1] [struc2]);
+
+      let struc1 = (struc_of_string "[ | P { (1) }; R:1 {} | ]") in
+      let struc2 = (struc_of_string "[ | P:1 {}; R { (1) } | ]") in
+      formula_option_eq "P(x0)" 
+	(Distinguish.distinguish_upto ~qr:0 ~k:1 [struc1] [struc2]);
+    );
+
+  "distinguish" >::
+    (fun () ->
+      let struc1 = (struc_of_string "[ | R { (1, 2); (2, 3) } | ]") in
+      let struc2 = (struc_of_string "[ | R { (1, 2) } | ]") in
+      formula_option_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_option_eq "ex x0 P(x0)" 
+	(Distinguish.distinguish [struc1] [struc2]);
+
+      let struc1 = struc_of_string "[  |  |  ] \"
+	...
+	...
+	...
+	P..
+\"" in
+      let struc2 = struc_of_string "[  |  |  ] \"
+	...
+	P..
+	...
+	...
+\"" in
+      formula_option_eq "ex x0, x1 (P(x0) and C(x0, x1))" 
+	(Distinguish.distinguish [struc1] [struc2]);
+    );
+]
+
+let bigtests = "DistinguishBig" >::: [
+  "semi-tic-tac-toe" >::
+    (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_option_eq 
+    "P(x0) and P(x1) and C(x0, x1) and ex x2 (P(x2) and C(x2, x0))"
+    (Distinguish.distinguish ~skip_outer_exists:true 
+       [strucP] [strucN1; strucN2; strucN3]);
+    );
+
+  "breakthrough" >::
+    (fun () ->
+      let struc1 = struc_of_string "[  |  |  ] \"
+	   ...   ...   ...   ...
+	   ...   W..   ...B  ...
+	...   ...   ...   ...   
+	...   ...   ...   B..   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   W..
+	...   ...   ...   ...   
+	...W  ...   ...   ...   
+\"" in
+      let struc2 = struc_of_string "[  |  |  ] \"
+	   ...   ...   ...   ...
+	   ...   ...   ...B  ...
+	...   ...   ...   ...   
+	...   ...W  ...   B..   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   W..
+	...   ...   ...   ...   
+	...W  ...   ...   ...   
+\"" in (* Distinguish.set_debug_level 1; *)
+      formula_option_eq "W(x1) and all x0 not C(x1, x0)"
+	(Distinguish.distinguish ~skip_outer_exists:true [struc1] [struc2]);
+    );
+]

Copied: trunk/Toss/Learn/LearnGame.ml (from rev 1639, trunk/Toss/Server/LearnGame.ml)
===================================================================
--- trunk/Toss/Learn/LearnGame.ml	                        (rev 0)
+++ trunk/Toss/Learn/LearnGame.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -0,0 +1,119 @@
+(* Learning games from examples. *)
+
+let debug_level = ref 0
+let set_debug_level i = (debug_level := i)
+
+let rec evens ?(acc=[0]) k =
+  let last = (List.hd (List.rev acc)) in
+  if (List.hd (List.rev acc))> k then
+    (List.rev (List.tl ( List.rev acc)))
+  else 
+    evens ~acc:(acc@[(last+2)]) k 
+let odds k =
+  evens ~acc:[1] k 
+
+
+let winFormula winningStates notWinningStates =
+  if !debug_level > 0 then
+    print_endline (
+      "Searching WIN:\n" ^ 
+	(String.concat "\n" (List.map Structure.str winningStates)) ^ "\nNOT\n"^
+	(String.concat "\n" (List.map Structure.str notWinningStates)));
+  FormulaOps.tnf_fv
+    (Aux.unsome (Distinguish.distinguish winningStates notWinningStates))
+
+let cleanStructure struc =
+  let funs = ref [] in
+  let append_fun f _ = funs := f :: !funs in
+  Structure.StringMap.iter append_fun (Structure.functions struc);
+  let struc = StructureParser.parse_structure Lexer.lex (Lexing.from_string  (Structure.str struc)) in
+  Structure.replace_names (List.fold_left
+    (fun x y ->
+      Structure.clear_fun x y)
+    struc !funs) Structure.StringMap.empty
+  Structure.IntMap.empty 
+
+
+let move struct1 struct2 =
+  let changed = (Aux.unique_sorted 
+    ( List.map fst  
+      (Structure.diff_elems struct1 struct2 )) )  in
+  let strucBefore = 
+    fst (Structure.del_elems struct1 
+      (Aux.list_diff 
+        (Aux.unique_sorted (Structure.elements struct1))
+        changed )) in
+  let strucAfter =
+    fst (Structure.del_elems struct2 
+      (Aux.list_diff 
+        (Aux.unique_sorted (Structure.elements struct2))
+        changed ))  in
+  ((cleanStructure strucBefore) , (cleanStructure strucAfter))
+  
+let movesi i partylist =
+  Aux.unique_sorted
+    ~cmp: (fun (s1,s2) (t1,t2) -> 
+      let c = ( Structure.compare s1 t1) in
+      if c != 0 then c
+      else (Structure.compare s2 t2))
+    (List.fold_left
+     (fun acc party -> 
+       List.append acc 
+         (List.fold_left
+           (fun prev i -> 
+             if (i < ((List.length party)-1)) then
+               let m = move (List.nth party i) (List.nth party (i+1)) in
+               (List.append prev [m])
+             else
+               (List.append prev []))
+           [] (evens ~acc:[i] (List.length party)) ) )
+     [] partylist)
+
+let learnFromParties ~win0 ~win1 ~tie ~wrong =
+  let win0f = winFormula 
+    (List.map (fun x -> List.hd (List.rev x)) win0)
+    (List.flatten ((List.map (fun x->  List.tl (List.rev x))
+		      win0) @ win1)) in
+  let win1f = winFormula 
+    (List.map (fun x -> List.hd (List.rev x)) win1)
+    (List.flatten ((List.map (fun x->  List.tl (List.rev x))
+		      win1) @ win0)) in
+  
+  let moves0 = movesi 0 (win0 @ win1) in
+  let moves1 = movesi 1 (win0 @ win1) in
+
+  "PLAYERS 1, 2\n"^
+  "REL Win1() = "^ (Formula.sprint win0f) ^"\n"^
+  "REL Win2() = "^ (Formula.sprint win1f) ^"\n"^
+  "RULE Mv1: " ^
+  (List.fold_left 
+     (fun old x-> 
+       old ^ "\n"^
+	 (Structure.str (fst x))^" -> "^(Structure.str
+      (snd x)) ^ 
+     "\nemb "^(String.concat "," (List.map fst (Structure.rel_signature
+     (fst x)) )) ^ " " ^
+     "pre not Win2()" )
+    "" moves0) ^"\n"^
+  "RULE Mv2: " ^
+  (List.fold_left 
+    (fun old x-> 
+      old^"\n"^
+      (Structure.str (fst x))^" -> "^(Structure.str
+   (snd x)) ^ 
+     "\nemb "^(String.concat "," (List.map fst (Structure.rel_signature
+     (fst x)) )) ^ " " ^
+     "pre not Win1()" )
+    "" moves1) ^"\n"^
+  "LOC 0 { 
+  PLAYER 1 { PAYOFF : (Win1()) - :(Win2())
+               MOVES [Mv1 -> 1]}
+  PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) }
+}
+LOC 1{
+  PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) }
+  PLAYER 2 { PAYOFF :(Win2()) - :(Win1())
+             MOVES [Mv2 -> 0] }
+}" ^"\n" ^
+  "MODEL "^(Structure.str (List.hd (List.hd win0)))
+

Copied: trunk/Toss/Learn/LearnGame.mli (from rev 1639, trunk/Toss/Server/LearnGame.mli)
===================================================================
--- trunk/Toss/Learn/LearnGame.mli	                        (rev 0)
+++ trunk/Toss/Learn/LearnGame.mli	2012-01-16 14:23:37 UTC (rev 1640)
@@ -0,0 +1,21 @@
+(** Module for learning games from examples. *)
+
+val move: Structure.structure -> Structure.structure ->
+  Structure.structure * Structure.structure
+
+(** Learn a two-player win-lose-or-tie game given 4 sets of plays of another
+    game [source]: [wins0] which are now supposed to be won by Player 0,
+    [wins1] - now won by Player 1, [tie] - now a tie, and [wrong] which
+    are not correct plays of the newly constructed game. The plays are given
+    as lists of ids to be retrieved from DB, result is a toss game string. *)
+val learnFromParties:
+  win0: Structure.structure list list -> 
+  win1: Structure.structure list list -> 
+  tie: Structure.structure list list -> 
+  wrong: Structure.structure list list -> string
+
+
+(** {2 Debugging} *)
+
+(* At higher debug levels we prints out diagnostic information. *)
+val set_debug_level: int -> unit

Copied: trunk/Toss/Learn/LearnGameTest.ml (from rev 1639, trunk/Toss/Server/LearnGameTest.ml)
===================================================================
--- trunk/Toss/Learn/LearnGameTest.ml	                        (rev 0)
+++ trunk/Toss/Learn/LearnGameTest.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -0,0 +1,340 @@
+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 tests = "LearnGame" >::: [
+  "simple test game" >::
+    (fun () ->
+      let partylist0 = [
+        List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  
+.  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  
+.  P  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  
+Q  P  
+\"" ;]] in
+      let partylist1 = [
+        List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  
+.  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  
+P  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  
+P  Q  
+\"" ;]] in
+      let res_game =
+"PLAYERS 1, 2
+REL Win1() = ex x1 (Q(x1) and ex x0 R(x1, x0))
+REL Win2() = ex x1 (Q(x1) and ex x0 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()
+RULE Mv2: 
+[1 | P:1 {}; Q:1 {}; R:2 {} | ] -> [1 | P:1 {}; Q (1); R:2 {} | ]
+emb R,Q,P pre not Win1()
+LOC 0 { 
+  PLAYER 1 { PAYOFF : (Win1()) - :(Win2())
+               MOVES [Mv1 -> 1]}
+  PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) }
+}
+LOC 1{
+  PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) }
+  PLAYER 2 { PAYOFF :(Win2()) - :(Win1())
+             MOVES [Mv2 -> 0] }
+}
+MODEL [ | P:1 {}; Q:1 {} | ] R R \"
+	      
+	.  .  
+\"" in
+      assert_equal ~printer:(fun x -> x)  res_game
+	((LearnGame.learnFromParties ~win0:partylist0 ~win1:partylist1 
+	    ~tie:[] ~wrong:[]));
+    );
+]
+
+
+let bigtests = "LearnGame" >::: [
+  "tic-tac-toe" >::
+    (fun () ->
+      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 {} | ] \"
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+P  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  Q  .  
+.  .  .  
+P  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  Q  .  
+.  .  .  
+P  P  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  Q  Q  
+.  .  .  
+P  P  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\""; 
+      ];  List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  P  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  P  .  
+.  .  .  
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"";
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  P  .  
+.  .  .  
+Q  P  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"";
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  P  .  
+.  .  .  
+Q  P  .  
+.  .  .  
+Q  .  .  
+.  .  .  
+\"";]
+      ] in
+let partylist1 = [
+        List.map struc_of_string [ 
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+P  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  .  
+.  .  .  
+.  .  .  
+P  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  .  
+.  .  .  
+.  .  .  
+P  P  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  Q  
+.  .  .  
+.  .  .  
+P  P  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  P  
+.  .  .  
+.  Q  Q  
+.  .  .  
+.  .  .  
+P  P  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  Q  P  
+.  .  .  
+.  Q  Q  
+.  .  .  
+.  .  .  
+P  P  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  Q  P  
+.  .  .  
+.  Q  Q  
+.  .  .  
+.  .  .  
+P  P  P  
+\"";
+      ];  List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+\"" ;
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+P  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  .  
+.  .  .  
+.  .  .  
+P  .  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  .  
+.  .  .  
+.  .  .  
+P  P  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  Q  
+.  .  .  
+.  .  .  
+P  P  .  
+\""; 
+"[ | P:1 {}; Q:1 {} | ] \"
+Q  .  .  
+.  .  .  
+.  Q  Q  
+.  .  .  
+.  .  .  
+P  P  P  
+\""; 
+      ]
+      ; List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+.  .  .  
+P  P  P  
+\"";]
+      ; List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  .  
+.  P  .  
+.  .  .  
+.  P  .  
+.  .  .  
+.  P  .  
+\"";]
+      ; List.map struc_of_string [
+"[ | P:1 {}; Q:1 {} | ] \"
+.  .  .  
+.  .  P  
+.  .  .  
+.  P  .  
+.  .  .  
+P  .  .  
+\"";]
+        ] in
+assert_equal ~printer:(fun x -> x)  ""
+  ((LearnGame.learnFromParties ~win0:partylist0 ~win1:partylist1
+      ~tie:[] ~wrong:[]));
+    );
+
+]

Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Makefile	2012-01-16 14:23:37 UTC (rev 1640)
@@ -46,8 +46,9 @@
 SolverINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim
 ArenaINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver
 PlayINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena
+LearnINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena
 GGPINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play
-ServerINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play,GGP
+ServerINC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play,GGP,Learn
 .INC=Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play,GGP,Server
 
 %.native: %.ml caml_extensions/pa_let_try.cmo
@@ -125,6 +126,14 @@
 	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
 		./TossServer -fulltest GGP -v
 
+# Learn tests
+LearnTests: TossServer
+	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
+		./TossServer -fulltest Learn
+LearnTestsVerbose: TossServer
+	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
+		./TossServer -fulltest Learn -v
+
 # Server tests
 ServerTests: TossServer
 	OCAMLRUNPARAM=b; export OCAMLRUNPARAM; \
@@ -153,4 +162,5 @@
 clean:
 	ocamlbuild -clean
 	rm -f *.cmx *.cmi *.o *.cmo *.a *.cmxa *.cma *.annot *~ TossServer
+	rm -f Formula/*~ Solver/*~ Arena/*~ Learn/*~ Play/*~ GGP/*~ Server/*~
 	rm -f caml_extensions/*.cmo caml_extensions/*.cmi

Deleted: trunk/Toss/Server/LearnGame.ml
===================================================================
--- trunk/Toss/Server/LearnGame.ml	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Server/LearnGame.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -1,149 +0,0 @@
-(* Learning games from examples. *)
-
-let debug_level = ref 0
-let set_debug_level i = (debug_level := i)
-
-let struc_of_string s = 
-  StructureParser.parse_structure Lexer.lex (Lexing.from_string s)
-
-
-
-let rec evens ?(acc=[0]) k =
-  let last = (List.hd (List.rev acc)) in
-  if (List.hd (List.rev acc))> k then
-    (List.rev (List.tl ( List.rev acc)))
-  else 
-    evens ~acc:(acc@[(last+2)]) k 
-let odds k =
-  evens ~acc:[1] k 
-
-
-let winFormula winningStates notWinningStates =
-  if !debug_level > 0 then
-    print_endline (
-      "Searching WIN:\n" ^ 
-	(String.concat "\n" (List.map Structure.str winningStates)) ^ "\nNOT\n"^
-	(String.concat "\n" (List.map Structure.str notWinningStates)));
-  FormulaOps.tnf_fv
-    (Aux.unsome (Distinguish.distinguish winningStates notWinningStates))
-
-let cleanStructure struc =
-  let funs = ref [] in
-  let append_fun f _ = funs := f :: !funs in
-  Structure.StringMap.iter append_fun (Structure.functions struc);
-  let struc = StructureParser.parse_structure Lexer.lex (Lexing.from_string  (Structure.str struc)) in
-  Structure.replace_names (List.fold_left
-    (fun x y ->
-      Structure.clear_fun x y)
-    struc !funs) Structure.StringMap.empty
-  Structure.IntMap.empty 
-
-
-let move struct1 struct2 =
-  let changed = (Aux.unique_sorted 
-    ( List.map fst  
-      (Structure.diff_elems struct1 struct2 )) )  in
-  let strucBefore = 
-    fst (Structure.del_elems struct1 
-      (Aux.list_diff 
-        (Aux.unique_sorted (Structure.elements struct1))
-        changed )) in
-  let strucAfter =
-    fst (Structure.del_elems struct2 
-      (Aux.list_diff 
-        (Aux.unique_sorted (Structure.elements struct2))
-        changed ))  in
-  ((cleanStructure strucBefore) , (cleanStructure strucAfter))
-  
-let movesi i partylist =
-  Aux.unique_sorted
-    ~cmp: (fun (s1,s2) (t1,t2) -> 
-      let c = ( Structure.compare s1 t1) in
-      if c != 0 then c
-      else (Structure.compare s2 t2))
-    (List.fold_left
-     (fun acc party -> 
-       List.append acc 
-         (List.fold_left
-           (fun prev i -> 
-             if (i < ((List.length party)-1)) then
-               let m = move (List.nth party i) (List.nth party (i+1)) in
-               (List.append prev [m])
-             else
-               (List.append prev []))
-           [] (evens ~acc:[i] (List.length party)) ) )
-     [] partylist)
-
-let learnFromParties partylistWin0 partylistWin1 =
-  let win0 = winFormula 
-    (List.map (fun x -> List.hd (List.rev x)) partylistWin0)
-    (List.flatten ((List.map (fun x->  List.tl (List.rev x))
-    partylistWin0)@partylistWin1)) in
-  let win1 = winFormula 
-    (List.map (fun x -> List.hd (List.rev x)) partylistWin1)
-    (List.flatten ((List.map (fun x->  List.tl (List.rev x))
-    partylistWin1)@partylistWin0)) in
-
-  let moves0 = movesi 0 (partylistWin0 @ partylistWin1) in
-  let moves1 = movesi 1 (partylistWin0 @ partylistWin1) in
-
-  "PLAYERS 1, 2\n"^
-  "REL Win1() = "^ (Formula.sprint win0) ^"\n"^
-  "REL Win2() = "^ (Formula.sprint win1) ^"\n"^
-  "RULE Mv1: " ^
-  (List.fold_left 
-    (fun old x-> 
-      old^"\n"^
-      (Structure.str (fst x))^" -> "^(Structure.str
-   (snd x)) ^ 
-     "\nemb "^(String.concat "," (List.map fst (Structure.rel_signature
-     (fst x)) )) ^ " " ^
-     "pre not Win2()" )
-    "" moves0) ^"\n"^
-  "RULE Mv2: " ^
-  (List.fold_left 
-    (fun old x-> 
-      old^"\n"^
-      (Structure.str (fst x))^" -> "^(Structure.str
-   (snd x)) ^ 
-     "\nemb "^(String.concat "," (List.map fst (Structure.rel_signature
-     (fst x)) )) ^ " " ^
-     "pre not Win1()" )
-    "" moves1) ^"\n"^
-  "LOC 0 { 
-  PLAYER 1 { PAYOFF : (Win1()) - :(Win2())
-               MOVES [Mv1 -> 1]}
-  PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) }
-}
-LOC 1{
-  PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) }
-  PLAYER 2 { PAYOFF :(Win2()) - :(Win1())
-             MOVES [Mv2 -> 0] }
-}" ^"\n" ^
-  "MODEL "^(Structure.str (List.hd (List.hd partylistWin0)))
-
-
-(* Get the play with given id from DB - as a sequence of structures. *)
-let playFromDB pid =
-  let dbtable select tbl = DB.get_table !DB.dbFILE ~select tbl in
-  let res = dbtable ("playid=" ^ (string_of_int pid) ) "old_states" in
-  let moveStrucs = List.map (fun x -> ((int_of_string x.(4)), x.(5))) res in
-  let prevs = List.sort (fun (a, b) (c, d) -> a - c) moveStrucs in
-  let cur = dbtable ("playid=" ^ (string_of_int pid)) "cur_states" in 
-  (List.map snd prevs) @ [(List.hd cur).(5)]
-
-(* Learn a two-player win-lose-or-tie game given 4 sets of plays of another
-   game [source]: [wins0] which are now supposed to be won by Player 0,
-   [wins1] - now won by Player 1, [tie] - now a tie, and [wrong] which
-   are not correct plays of the newly constructed game. *)
-let learnFromDB ~source ~wins0 ~wins1 ~tie ~wrong =
-  if !debug_level > 0 then (
-    let pl l = String.concat ", " (List.map string_of_int l) in
-    print_endline ("Learning from " ^ source ^ " w0: " ^ (pl wins0) ^ " w1: " ^
-		      (pl wins1) ^" tie: "^ (pl tie) ^" wrong: "^ (pl wrong));
-  );
-  let (wins0, wins1, tie, wrong) = 
-    (List.map playFromDB wins0, List.map playFromDB wins1,
-     List.map playFromDB tie, List.map playFromDB wrong) in
-  learnFromParties (List.map (List.map struc_of_string) wins0) 
-    (List.map (List.map struc_of_string) wins1)

Deleted: trunk/Toss/Server/LearnGame.mli
===================================================================
--- trunk/Toss/Server/LearnGame.mli	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Server/LearnGame.mli	2012-01-16 14:23:37 UTC (rev 1640)
@@ -1,25 +0,0 @@
-(** Module for learning games from examples. *)
-
-val move: Structure.structure -> Structure.structure ->
-  Structure.structure * Structure.structure
-
-val learnFromParties:
-  Structure.structure list list -> Structure.structure list list -> string
-
-
-(** Get the play with given id from DB - as a sequence of structure strings. *)
-val playFromDB: int -> string list
-
-(** Learn a two-player win-lose-or-tie game given 4 sets of plays of another
-    game [source]: [wins0] which are now supposed to be won by Player 0,
-    [wins1] - now won by Player 1, [tie] - now a tie, and [wrong] which
-    are not correct plays of the newly constructed game. The plays are given
-    as lists of ids to be retrieved from DB, result is a toss game string. *)
-val learnFromDB: source:string -> wins0: int list -> wins1: int list -> 
-  tie: int list -> wrong: int list -> string
-
-
-(** {2 Debugging} *)
-
-(* At higher debug levels we prints out diagnostic information. *)
-val set_debug_level: int -> unit

Deleted: trunk/Toss/Server/LearnGameTest.ml
===================================================================
--- trunk/Toss/Server/LearnGameTest.ml	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Server/LearnGameTest.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -1,338 +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 tests = "LearnGame" >::: [
-  "simple test game" >::
-    (fun () ->
-      let partylist0 = [
-        List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  
-.  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  
-.  P  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  
-Q  P  
-\"" ;]] in
-      let partylist1 = [
-        List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  
-.  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  
-P  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  
-P  Q  
-\"" ;]] in
-      let res_game =
-"PLAYERS 1, 2
-REL Win1() = ex x1 (Q(x1) and ex x0 R(x1, x0))
-REL Win2() = ex x1 (Q(x1) and ex x0 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()
-RULE Mv2: 
-[1 | P:1 {}; Q:1 {}; R:2 {} | ] -> [1 | P:1 {}; Q (1); R:2 {} | ]
-emb R,Q,P pre not Win1()
-LOC 0 { 
-  PLAYER 1 { PAYOFF : (Win1()) - :(Win2())
-               MOVES [Mv1 -> 1]}
-  PLAYER 2 { PAYOFF : (Win2()) - :(Win1()) }
-}
-LOC 1{
-  PLAYER 1 { PAYOFF :(Win1()) - :(Win2()) }
-  PLAYER 2 { PAYOFF :(Win2()) - :(Win1())
-             MOVES [Mv2 -> 0] }
-}
-MODEL [ | P:1 {}; Q:1 {} | ] R R \"
-	      
-	.  .  
-\"" in
-      assert_equal ~printer:(fun x -> x)  res_game
-	((LearnGame.learnFromParties partylist0 partylist1 ));
-    );
-]
-
-
-let bigtests = "LearnGame" >::: [
-  "tic-tac-toe" >::
-    (fun () ->
-      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 {} | ] \"
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-P  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  Q  .  
-.  .  .  
-P  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  Q  .  
-.  .  .  
-P  P  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  Q  Q  
-.  .  .  
-P  P  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\""; 
-      ];  List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  P  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  P  .  
-.  .  .  
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"";
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  P  .  
-.  .  .  
-Q  P  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"";
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  P  .  
-.  .  .  
-Q  P  .  
-.  .  .  
-Q  .  .  
-.  .  .  
-\"";]
-      ] in
-let partylist1 = [
-        List.map struc_of_string [ 
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-P  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  .  
-.  .  .  
-.  .  .  
-P  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  .  
-.  .  .  
-.  .  .  
-P  P  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  Q  
-.  .  .  
-.  .  .  
-P  P  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  P  
-.  .  .  
-.  Q  Q  
-.  .  .  
-.  .  .  
-P  P  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  Q  P  
-.  .  .  
-.  Q  Q  
-.  .  .  
-.  .  .  
-P  P  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  Q  P  
-.  .  .  
-.  Q  Q  
-.  .  .  
-.  .  .  
-P  P  P  
-\"";
-      ];  List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-\"" ;
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-P  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  .  
-.  .  .  
-.  .  .  
-P  .  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  .  
-.  .  .  
-.  .  .  
-P  P  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  Q  
-.  .  .  
-.  .  .  
-P  P  .  
-\""; 
-"[ | P:1 {}; Q:1 {} | ] \"
-Q  .  .  
-.  .  .  
-.  Q  Q  
-.  .  .  
-.  .  .  
-P  P  P  
-\""; 
-      ]
-      ; List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-.  .  .  
-P  P  P  
-\"";]
-      ; List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  .  
-.  P  .  
-.  .  .  
-.  P  .  
-.  .  .  
-.  P  .  
-\"";]
-      ; List.map struc_of_string [
-"[ | P:1 {}; Q:1 {} | ] \"
-.  .  .  
-.  .  P  
-.  .  .  
-.  P  .  
-.  .  .  
-P  .  .  
-\"";]
-        ] in
-assert_equal ~printer:(fun x -> x)  ""
-  ((LearnGame.learnFromParties partylist0 partylist1 ));
-    );
-
-]

Modified: trunk/Toss/Server/ReqHandler.ml
===================================================================
--- trunk/Toss/Server/ReqHandler.ml	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Server/ReqHandler.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -690,9 +690,36 @@
     let (w1, other) = List.partition (fun (_, b) -> b = "1") other in
     let (tie, other) = List.partition (fun (_, b) -> b = "2") other in
     let (wrong, _) = List.partition (fun (_, b) -> b = "3") other in
-    LearnGame.learnFromDB ~source:game 
-      ~wins0:(List.map fst w0) ~wins1:(List.map fst w1) 
-      ~tie:(List.map fst tie) ~wrong:(List.map fst wrong) in
+    (* Get the play with given id from DB - as a sequence of structures. *)
+    let playFromDB pid =
+      let dbtable select tbl = DB.get_table !DB.dbFILE ~select tbl in
+      let res = dbtable ("playid=" ^ (string_of_int pid) ) "old_states" in
+      let moveStrucs = List.map (fun x -> ((int_of_string x.(4)), x.(5))) res in
+      let prevs = List.sort (fun (a, b) (c, d) -> a - c) moveStrucs in
+      let cur = dbtable ("playid=" ^ (string_of_int pid)) "cur_states" in 
+      (List.map snd prevs) @ [(List.hd cur).(5)] in
+    (* Learn a two-player win-lose-or-tie game given 4 sets of plays of another
+       game [source]: [wins0] which are now supposed to be won by Player 0,
+       [wins1] - now won by Player 1, [tie] - now a tie, and [wrong] which
+       are not correct plays of the newly constructed game. *)
+    let learnFromDB source wins0 wins1 tie wrong =
+      if !debug_level > 0 then (
+	let pl l = String.concat ", " (List.map string_of_int l) in
+	print_endline ("Learning from "^ source ^" w0: "^ (pl wins0) ^" w1: "^ 
+			  (pl wins1)^" tie: "^(pl tie) ^" wrong: "^ (pl wrong));
+      );
+      let (wins0, wins1, tie, wrong) = 
+	(List.map playFromDB wins0, List.map playFromDB wins1,
+	 List.map playFromDB tie, List.map playFromDB wrong) in
+      let struc_of_string s = 
+	StructureParser.parse_structure Lexer.lex (Lexing.from_string s) in
+      LearnGame.learnFromParties
+	~win0:(List.map (List.map struc_of_string) wins0) 
+	~win1:(List.map (List.map struc_of_string) wins1) 
+	~tie:(List.map (List.map struc_of_string) tie) 
+	~wrong:(List.map (List.map struc_of_string) wrong) in
+    learnFromDB game (List.map fst w0) (List.map fst w1) 
+      (List.map fst tie) (List.map fst wrong) in
   let (tcmd, data) = split_two "#" msg in
   let resp, new_cookies = match tcmd with
     | "USERNAME" ->

Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Server/Tests.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -17,7 +17,6 @@
   "AssignmentsTest", [AssignmentsTest.tests];
   "SolverTest",      [SolverTest.tests; SolverTest.bigtests];
   "ClassTest",       [ClassTest.tests; ClassTest.bigtests];
-  "DistinguishTest", [DistinguishTest.tests; DistinguishTest.bigtests];
 ]
 
 let arena_tests = "Arena", [
@@ -41,10 +40,14 @@
   "TranslateFormulaTest",  [TranslateFormulaTest.tests];
 ]
 
+let learn_tests = "Learn", [
+  "DistinguishTest", [DistinguishTest.tests; DistinguishTest.bigtests];
+  "LearnGameTest",   [LearnGameTest.tests; LearnGameTest.bigtests];
+]
+
 let server_tests = "Server", [
   "PictureTest",     [PictureTest.tests];
   "ReqHandlerTest",  [ReqHandlerTest.tests];
-  "LearnGameTest",   [LearnGameTest.tests; LearnGameTest.bigtests];
 ]
 
 let tests_l = [
@@ -53,6 +56,7 @@
   arena_tests;
   play_tests;
   ggp_tests;
+  learn_tests;
   server_tests;
 ]
 

Deleted: trunk/Toss/Solver/Distinguish.ml
===================================================================
--- trunk/Toss/Solver/Distinguish.ml	2012-01-16 01:49:42 UTC (rev 1639)
+++ trunk/Toss/Solver/Distinguish.ml	2012-01-16 14:23:37 UTC (rev 1640)
@@ -1,269 +0,0 @@
-open Formula
-
-let debug_level = ref 0
-let set_debug_level i = (debug_level := i)
-
-type logic = FO | GuardedFO
-
-
-(* Helper functions to construct variables for indices. *)
-let varname i = "x" ^ string_of_int i
-let varnames k = List.map varname (Aux.range k)
-let var i = var_of_string (varname i)
-let fo_var i = fo_var_of_string (varname i)
-
-(* Helper function: check if a formula holds for a tuple on a structure. *)
-let check structure tuple 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 vars =Array.map fo_var (Array.of_list (Aux.range (Array.length tuple))) in
-  let assignment = if tuple = [||] then AssignmentSet.Any else
-      Assignments.assignments_of_list elems vars [tuple] in
-  eval structure formula assignment <> AssignmentSet.Empty
-
-(* - Atoms and FO Types - *)
-
-(* The list of literals which hold for a tuple on a structure. *)
-let atoms struc tuple =
-  let k = Array.length tuple in
-  let rec equalities = function
-    | [] -> []
-    | v :: vs -> (List.map (fun x -> Eq (`FO v,`FO x)) vs) @ (equalities vs) in
-  let atoms = FormulaOps.atoms (Structure.rel_signature struc) (varnames k) in
-  List.map (
-    fun atom -> if check struc tuple atom then atom else (Not atom)
-  ) (ato...
 
[truncated message content]