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

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

Revision: 1699
          http://toss.svn.sourceforge.net/toss/?rev=1699&view=rev
Author:   lukaszkaiser
Date:     2012-04-17 18:07:32 +0000 (Tue, 17 Apr 2012)
Log Message:
-----------
Correcting a solver bug, learning Pawn-Whoppining works again.

Modified Paths:
--------------
    trunk/Toss/Learn/Distinguish.ml
    trunk/Toss/Learn/Distinguish.mli
    trunk/Toss/Learn/LearnGame.ml
    trunk/Toss/Learn/LearnGame.mli
    trunk/Toss/Learn/LearnGameTest.ml
    trunk/Toss/Learn/Makefile
    trunk/Toss/Solver/Solver.ml

Modified: trunk/Toss/Learn/Distinguish.ml
===================================================================
--- trunk/Toss/Learn/Distinguish.ml	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Learn/Distinguish.ml	2012-04-17 18:07:32 UTC (rev 1699)
@@ -1,5 +1,8 @@
 open Formula
 
+let debug_level = ref 0
+let set_debug_level i = (debug_level := i)
+
 type logic = FO | ExFO | GuardedFO | ExGuardedFO
 
 
@@ -14,7 +17,7 @@
   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 varname (Array.of_list (Aux.range (Array.length tuple))) in
+  let vars =Array.map varname (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
@@ -185,7 +188,7 @@
     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
-  LOG 1 "guarded_types:\t\t tuples generated";
+  if !debug_level>0 then print_endline "guarded_types:\t\t tuples generated";
   let mem = Hashtbl.create 63 in
   Aux.unique_sorted (List.rev_map 
 		       (guarded_type_memo existential struc mem qr) ktups)
@@ -209,7 +212,8 @@
   let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in
   let atoms = Array.of_list (FormulaOps.atoms ~repetitions:repeat_vars
 			       (Structure.rel_signature struc) (varnames 2)) in
-  LOG 1 "tc_atomic:\t\t %i atoms\n%!" (Array.length atoms);
+  if !debug_level > 0 then
+    Printf.printf "tc_atomic:\t\t %i atoms\n%!" (Array.length atoms);
   let choices = List.rev_map Array.of_list
     (if positive then Aux.product (rept (Array.length atoms) [0; 1]) else
 	Aux.product (rept (Array.length atoms) [0; 1; -1])) in
@@ -257,7 +261,8 @@
 (* 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 =
-  LOG 2 "greedy_remove:\t\t %s\n%!" (Formula.str phi);
+  if !debug_level > 1 then
+    Printf.printf "greedy_remove:\t\t %s\n%!" (Formula.str phi);
   let rec greedy_remove_list minimize constructor acc = function
     | [] -> acc 
     | x :: xs -> 
@@ -270,7 +275,7 @@
       else greedy_remove_list minimize constructor (x::acc) xs in
   let greedy_remove_lst cons lst = 
     let l = greedy_remove_list false cons [] lst in
-    LOG 2 "greedy_remove_lst:\t min %i: %s" 
+    if !debug_level > 1 then Printf.printf "greedy_remove_lst:\t min %i: %s\n%!"
       (List.length l) (Formula.str (cons l));
     greedy_remove_list true cons [] (List.rev l) in
   match phi with
@@ -299,8 +304,9 @@
     | ExGuardedFO -> guarded_types ~existential:true struc ~qr ~k 
     | FO -> ntypes struc ~qr ~k
     | ExFO -> ntypes ~existential:true struc ~qr ~k in
-  LOG 1 "min_type_omitting:\t types generated";
+  if !debug_level > 0 then print_endline "min_type_omitting:\t types generated";
   let ok_types = List.filter (fun f -> not (List.mem f neg_types)) pos_types in
+  if !debug_level > 0 then Printf.printf "%i ok_types\n%!" (List.length ok_types);
   let ok_types = List.sort !compare_types ok_types in
   if ok_types = [] then None else Some (Formula.flatten_sort (List.hd ok_types))
 
@@ -313,17 +319,19 @@
     | FO -> ntypes s ~qr ~k
     | ExFO -> ntypes ~existential:true s ~qr ~k in
   let neg_tps = Aux.unique_sorted (Aux.concat_map types neg_strucs) in
-  LOG 1 "distinguish_upto:\t neg types done (%i): " (List.length neg_tps);
+  if !debug_level > 0 then print_endline "distinguish_upto:\t neg types done";
   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
+	| Some f -> let g = greedy_remove ~pos:true fails_on_negs f in
+		    (* Formula.print g; *) g :: 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
-  LOG 1 "distinguish_upto:\t pos_formulas %i" (List.length pos_formulas);
+  if !debug_level > 0 then Printf.printf 
+    "distinguish_upto:\t pos_formulas %i\n%!" (List.length pos_formulas);
   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
@@ -334,24 +342,27 @@
 
 (* Find a formula holding on all [pos_strucs] and on no [neg_strucs].
    Leaves free variables (existential) if [skip_outer_exists] is set. *)
-let distinguish ?(skip_outer_exists=false) s1 s2 = 
-  LOG 1 "distinguishing:\n\n%s\n\n and\n\n %s\n" 
-    (String.concat "\n" (List.map Structure.str s1))
-    (String.concat "\n" (List.map Structure.str s2));
+let distinguish ?(use_tc=true) ?(skip_outer_exists=false) s1 s2 = 
+  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 s1))
+      (String.concat "\n" (List.map Structure.str s2));
   let rec diff qr k =
     if qr > k then diff 0 (k+1) else (
-      LOG 1 "distinguish:\t\t qr %i k %i\n%!" qr k;
+      if !debug_level > 0 then
+	Printf.printf "distinguish:\t\t qr %i k %i\n%!" qr k;
       if qr = 0 then 
 	match distinguish_upto ~logic:GuardedFO ~qr ~k s1 s2 with
-	  | Some f -> f | None -> 
-	    match tc_atomic_distinguish ~positive:true 
-	      ~repeat_vars:false s1 s2 (3*k) with
-		| Some f -> Formula.flatten_sort f | None -> diff (qr+1) k 
+	  | Some f -> f | None -> if not use_tc then diff (qr+1) k else
+	      match tc_atomic_distinguish ~positive:true 
+		~repeat_vars:false s1 s2 (3*k) with
+		  | Some f -> Formula.flatten_sort f | None -> diff (qr+1) k 
       else
 	match distinguish_upto ~logic:GuardedFO ~qr ~k s1 s2 with
 	  | Some f -> 
 	    if qr > 1 (* hurry up for large qr *) then f else (
-	      LOG 1 "distinguish:\t\t guarded found: %s\n%!" (Formula.str f);
+	      if !debug_level > 0 then Printf.printf
+		"distinguish:\t\t guarded found: %s\n%!" (Formula.str f);
 	      match distinguish_upto ~logic:ExGuardedFO ~qr ~k s1 s2 with
 		| Some g-> if 2*(Formula.size f) < Formula.size g then f else g 
 		| None -> f

Modified: trunk/Toss/Learn/Distinguish.mli
===================================================================
--- trunk/Toss/Learn/Distinguish.mli	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Learn/Distinguish.mli	2012-04-17 18:07:32 UTC (rev 1699)
@@ -90,5 +90,5 @@
 
 (** Find a formula holding on all [pos_strucs] and on no [neg_strucs].
     Leaves free variables (existential) if [skip_outer_exists] is set. *)
-val distinguish: ?skip_outer_exists: bool ->
+val distinguish: ?use_tc: bool -> ?skip_outer_exists: bool ->
   Structure.structure list -> Structure.structure list -> Formula.formula

Modified: trunk/Toss/Learn/LearnGame.ml
===================================================================
--- trunk/Toss/Learn/LearnGame.ml	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Learn/LearnGame.ml	2012-04-17 18:07:32 UTC (rev 1699)
@@ -1,5 +1,7 @@
 (* Learning games from examples. *)
 
+let tc = ref true
+
 let rec evens ?(acc=[0]) k =
   let last = (List.hd (List.rev acc)) in
   if (List.hd (List.rev acc))> k then
@@ -14,7 +16,7 @@
   LOG 1 "Searching WIN:\n%s \nNOT\n%s\n"
     (String.concat "\n" (List.map Structure.str winningStates))
     (String.concat "\n" (List.map Structure.str notWinningStates));
-  let res = Distinguish.distinguish winningStates notWinningStates in
+  let res= Distinguish.distinguish ~use_tc:!tc winningStates notWinningStates in
   let print_tc (i, f) =
     Printf.sprintf "(tc !%i x0, x1 (%s))" i (Formula.str f) in
   match !Distinguish.distinguish_result_tc with
@@ -83,7 +85,7 @@
     let (good, bad) = (List.map mark mright, List.map mark mwrong) in
     LOG 1 "%s" (String.concat "\n" (List.map Structure.str good));
     LOG 1 "%s" (String.concat "\n" (List.map Structure.str bad));
-    let pre = Distinguish.distinguish good bad in
+    let pre = Distinguish.distinguish ~use_tc:!tc good bad in
     LOG 1 "pre: %s" (Formula.str pre);
     let elems = Aux.range ~from:1 ((Structure.nbr_elems (fst m)) + 1) in
     let let_part i = Printf.sprintf "let ch%i (x) = x = e%i in" i i in

Modified: trunk/Toss/Learn/LearnGame.mli
===================================================================
--- trunk/Toss/Learn/LearnGame.mli	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Learn/LearnGame.mli	2012-04-17 18:07:32 UTC (rev 1699)
@@ -1,5 +1,7 @@
 (** Module for learning games from examples. *)
 
+(** A flag whether to use the TC operator or not. *)
+val tc : bool ref
 
 (** 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,

Modified: trunk/Toss/Learn/LearnGameTest.ml
===================================================================
--- trunk/Toss/Learn/LearnGameTest.ml	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Learn/LearnGameTest.ml	2012-04-17 18:07:32 UTC (rev 1699)
@@ -96,6 +96,7 @@
     ("-v", Arg.Unit (fun () -> dbg_level 1), "be verbose");
     ("-d", Arg.Int (fun i -> dbg_level i), "set debug level");
     ("-f", Arg.String (fun s -> testname := s), "process files");
+    ("-notc", Arg.Unit (fun () -> LearnGame.tc := false), "no TC operator");
     ("-dir", Arg.String (fun s -> dir := s), "set files directory");
   ] in
   Arg.parse opts (fun _ -> ()) "Try -help for help or one of the following.";

Modified: trunk/Toss/Learn/Makefile
===================================================================
--- trunk/Toss/Learn/Makefile	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Learn/Makefile	2012-04-17 18:07:32 UTC (rev 1699)
@@ -28,13 +28,19 @@
 	diff res.toss examples/$(basename $@).toss
 	rm res.toss
 
+%.learnnotc:
+	make -C .. Learn/LearnGameTest.native
+	time ../LearnGameTest.native -notc -f $(basename $@) > res.toss
+	diff res.toss examples/$(basename $@).toss
+	rm res.toss
+
 learntests:
 	make Tic-Tac-Toe001.learn
 	make Tic-Tac-Toe002.learn
 	make Breakthrough001.learn
 	make Gomoku001.learn
 	make Connect4001.learn
-	make Pawn-Whopping001.learn
+	make Pawn-Whopping001.learnnotc
 
 
 %.reco:

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2012-04-16 19:52:08 UTC (rev 1698)
+++ trunk/Toss/Solver/Solver.ml	2012-04-17 18:07:32 UTC (rev 1699)
@@ -216,10 +216,10 @@
       | Ex (vl, phi) as ephi ->
 	check_timeout "Solver.eval.Ex";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in
-	if (fp = [] && 
-	    ((List.exists (fun v->List.mem v aset_vars) vl) ||
-		(aset_vars <> [] && FormulaSubst.free_vars ephi = []))) then
-	  let phi_asgn = 
+	let in_aset =
+          if List.exists(fun v->List.mem v aset_vars) vl then Any else aset in
+	let phi_asgn = 
+	  if (fp = [] && FormulaSubst.free_vars ephi = []) then
 	    try
 	      let (res, _) = Hashtbl.find !cache_results phi in
 	      LOG 2 "In-Eval found in cache: %s" (Formula.str phi);
@@ -228,13 +228,10 @@
 	      LOG 1 "In-Eval_m %s" (str phi);
 	      let phi_asgn = eval fp model elems Any phi in
 	      Hashtbl.add !cache_results phi (phi_asgn, phi_rels phi);
-	      phi_asgn in
-          report (simp (join aset 
-			  (project_list elems phi_asgn (List.map var_str vl))))
-	else
-          let phi_asgn = eval fp model elems aset phi in
-          report (simp (join aset 
-			  (project_list elems phi_asgn (List.map var_str vl))))
+	      phi_asgn
+	  else eval fp model elems in_aset phi in
+        report (simp (join aset 
+			(project_list elems phi_asgn (List.map var_str vl))))
       | All (vl, phi) ->
 	check_timeout "Solver.eval.All";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in

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