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

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

Revision: 1433
          http://toss.svn.sourceforge.net/toss/?rev=1433&view=rev
Author:   lukaszkaiser
Date:     2011-05-07 22:30:43 +0000 (Sat, 07 May 2011)

Log Message:
-----------
Fixed-points corrections and optimisations, using lfp for tc, manual heuristic in Chess.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Arena.mli
    trunk/Toss/Arena/ArenaParser.mly
    trunk/Toss/Client/Makefile
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/Formula/FormulaParser.mly
    trunk/Toss/Formula/Lexer.mll
    trunk/Toss/Play/Heuristic.ml
    trunk/Toss/Play/Heuristic.mli
    trunk/Toss/Server/ReqHandler.ml
    trunk/Toss/Server/Server.ml
    trunk/Toss/Solver/AssignmentSet.ml
    trunk/Toss/Solver/Assignments.ml
    trunk/Toss/Solver/Assignments.mli
    trunk/Toss/Solver/Solver.ml
    trunk/Toss/Solver/SolverTest.ml
    trunk/Toss/TossFullTest.ml
    trunk/Toss/examples/Chess.toss

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Arena/Arena.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -113,6 +113,7 @@
   | DefPlayers of string list               (* add players (fresh numbers) *)
   | DefRel of string * string list * Formula.formula
   (* add a defined relation *)
+  | DefPattern of Formula.real_expr     (* Pattern definition *)
   | StateStruc of Structure.structure   (* initial/saved state *)
   | StateTime of float                  (* initial/saved time *)
   | StateLoc of int                     (* initial/saved location *)
@@ -138,12 +139,13 @@
 
 
 let make_player_loc defs =
-  let (payoff, moves) = List.fold_left
-    (fun (payoff, moves) -> function
-      | `Payoff poff -> (poff, moves)
-      | `Moves mvs -> (payoff, moves @ mvs)
-    ) (Formula.Const 0., []) defs in
-  { zero_loc with payoff = payoff ; moves = moves }
+  let (payoff, moves, heurs) = List.fold_left
+    (fun (payoff, moves, heurs) -> function
+      | `Payoff poff -> (poff, moves, heurs)
+      | `Moves mvs -> (payoff, moves @ mvs, heurs)
+      | `Heurs hs -> (payoff, moves, heurs @ hs)
+    ) (Formula.Const 0., [], []) defs in
+  { zero_loc with payoff = payoff ; moves = moves; heur = heurs }
 
 let make_location id loc_defs =
   fun player_names ->
@@ -158,18 +160,16 @@
    list of definitions (usually corresponding to a ".toss" file.) *)
 let process_definition ?extend_state defs =
   let (old_rules, old_locs, players, old_defined_rels,
-       state, time, cur_loc, data) =
+       state, time, cur_loc, patterns, data) =
     match extend_state with
       | None ->
-        [], [], [], [], Structure.empty_structure (), 0.0, 0, []
-      | Some state ->
-        (fst state).rules, Array.to_list (fst state).graph,
-        List.map fst (List.sort (fun (_,x) (_,y) -> x-y)
-                        (fst state).player_names),
-        List.map (fun (rel, (args, body)) -> rel, args, body)
-	  (fst state).defined_rels,
-        (snd state).struc, (snd state).time,
-        (snd state).cur_loc, (fst state).data in
+        [], [], [], [], Structure.empty_structure (), 0.0, 0, [], []
+      | Some (game, gstate) ->
+        game.rules, Array.to_list game.graph,
+        List.map fst (List.sort (fun (_,x) (_,y) -> x-y) game.player_names),
+        List.map (fun (rel, (args, body)) -> rel, args, body) game.defined_rels,
+        gstate.struc, gstate.time, gstate.cur_loc,
+	game.patterns, game.data in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     printf "process_definition: %d old rules, %d old locs\n%!"
@@ -177,37 +177,40 @@
   );
   (* }}} *)
   let rules, locations, players, defined_rels,
-    state, time, cur_loc, data =
+    state, time, cur_loc, patterns, data =
     List.fold_left (fun (rules, locations, players, defined_rels,
-                         state, time, cur_loc, data) def ->
+                         state, time, cur_loc, patterns, data) def ->
       match def with
         | DefRule (rname, r) ->
           ((rname, r)::rules, locations, players, defined_rels,
-           state, time, cur_loc, data)
+           state, time, cur_loc, patterns, data)
         | DefLoc loc ->
           (rules, loc::locations, players, defined_rels,
-           state, time, cur_loc, data)
+           state, time, cur_loc, patterns, data)
         | DefPlayers more_players ->
           (rules, locations, players @ more_players, defined_rels,
-           state, time, cur_loc, data)
+           state, time, cur_loc, patterns, data)
         | DefRel (rel, args, body) ->
           (rules, locations, players,
            (rel, args, body)::defined_rels,
-           state, time, cur_loc, data)
+           state, time, cur_loc, patterns, data)
+	| DefPattern pat ->
+          (rules, locations, players, defined_rels,
+           state, time, cur_loc, pat :: patterns, data)
         | StateStruc struc ->
           (rules, locations, players, defined_rels,
-           struc, time, cur_loc, data)
+           struc, time, cur_loc, patterns, data)
         | StateTime ntime ->
           (rules, locations, players, defined_rels,
-           state, ntime, cur_loc, data)
+           state, ntime, cur_loc, patterns, data)
         | StateLoc ncur_loc ->
           (rules, locations, players, defined_rels,
-           state, time, ncur_loc, data)
+           state, time, ncur_loc, patterns, data)
         | StateData more_data ->
           (rules, locations, players, defined_rels,
-           state, time, cur_loc, data @ more_data)
+           state, time, cur_loc, patterns, data @ more_data)
     ) ([], [], players, [],
-       state, time, cur_loc, data) defs in
+       state, time, cur_loc, patterns, data) defs in
   (* {{{ log entry *)
   if !debug_level > 2 then (
     printf "process_definition: %d new rules, %d new defined rels\n%!"
@@ -261,15 +264,15 @@
   (* }}} *)
   let graph = Array.of_list (List.rev locations) in 
   (* TODO; FIXME; JUST THIS List.rev ABOVE WILL NOT ALWAYS BE GOOD, OR?!! *)
-  let game = {
+  {
     rules = rules;
-    patterns = [];
+    patterns = List.rev patterns;
     graph = graph;
     num_players = num_players;
     player_names = player_names;
     data = data;
     defined_rels = List.map (fun (a, b, c) -> (a, (b, c))) defined_rels;
-  } in game, {
+  }, {
     struc = state;
     time = time;
     cur_loc = cur_loc;

Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Arena/Arena.mli	2011-05-07 22:30:43 UTC (rev 1433)
@@ -93,6 +93,7 @@
   | DefPlayers of string list               (** add players (fresh numbers) *)
   | DefRel of string * string list * Formula.formula
   (** add a defined relation *)
+  | DefPattern of Formula.real_expr     (** Pattern definition *)
   | StateStruc of Structure.structure   (** initial/saved state *)
   | StateTime of float                  (** initial/saved time *)
   | StateLoc of int                     (** initial/saved location *)
@@ -110,7 +111,8 @@
 val make_location :
   int ->
   (string * [< `Moves of (label * int) list 
-	    | `Payoff of Formula.real_expr ] list) list ->
+	    | `Payoff of Formula.real_expr
+	    | `Heurs of float list ] list) list ->
   (string * int) list -> player_loc array
 
 (** Create a game state, possibly by extending an old state, from a

Modified: trunk/Toss/Arena/ArenaParser.mly
===================================================================
--- trunk/Toss/Arena/ArenaParser.mly	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Arena/ArenaParser.mly	2011-05-07 22:30:43 UTC (rev 1433)
@@ -37,23 +37,28 @@
         "Syntax error in move definition."
     }
 
-real_expr_wrapper:
+real_expr_err:
   | rexp = real_expr { rexp }
   | error
     { Lexer.report_parsing_error $startpos $endpos
         "Syntax error in real expression."
     }
 
-formula_expr_wrapper:
+formula_expr_err:
   | phi = formula_expr { phi }
   | error
     { Lexer.report_parsing_error $startpos $endpos
         "Syntax error in formula expression."
     }
 
+float_or_int:
+  | FLOAT { $1 }
+  | INT   { float_of_int $1 }
+
 player_loc_defs:
-  | PAYOFF poff = real_expr_wrapper                 { `Payoff poff }
-  | MOVES moves = separated_list (SEMICOLON, move)  { `Moves moves }
+  | PAYOFF poff = real_expr_err                         { `Payoff poff }
+  | MOVES moves = separated_list (SEMICOLON, move)      { `Moves moves }
+  | COND hs = separated_list (SEMICOLON, float_or_int)  { `Heurs hs }
   | error
     { Lexer.report_parsing_error $startpos $endpos
         "Syntax error in location field."
@@ -78,7 +83,7 @@
 
 rel_def_simple:
   | rel = ID args = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
-    EQ body = formula_expr { (rel, args, body) }
+    EQ body = formula_expr_err { (rel, args, body) }
 
 game_defs:
   | RULE_SPEC rname = id_int COLON r = rule_expr
@@ -87,14 +92,16 @@
     { DefLoc l }
   | PLAYERS_MOD pnames = separated_list (COMMA, id_int)
     { DefPlayers pnames }
+  | SET_CMD r = real_expr_err 
+    { DefPattern r }
   | REL_MOD rel = ID
     arg = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
-    body = delimited (OPENCUR, formula_expr, CLOSECUR)
+    body = delimited (OPENCUR, formula_expr_err, CLOSECUR)
     { DefRel (rel, arg, body) }
   | REL_MOD rel = ID
     arg = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
     EQ
-    body = formula_expr
+    body = formula_expr_err
     { DefRel (rel, arg, body) }
   | MODEL_SPEC model = struct_expr
     { StateStruc model }
@@ -164,7 +171,7 @@
       { GetFun (wh, fn, elem) }
   | SET_CMD PLAYER_MOD oldn=id_int PLAYER_MOD newn=id_int
       { RenamePlayer (oldn, newn) }
-  | SET_CMD LOC_MOD PAYOFF loc=INT player=id_int poff=real_expr_wrapper
+  | SET_CMD LOC_MOD PAYOFF loc=INT player=id_int poff=real_expr_err
       { SetLocPayoff (loc, player, poff) }
   | GET_CMD LOC_MOD PAYOFF loc=INT player=id_int
     { GetLocPayoff (loc, player) }
@@ -184,7 +191,7 @@
         OPENSQ,
         separated_nonempty_list(SEMICOLON,
           delimited(OPENCUR, separated_list (
-            SEMICOLON, separated_pair (id_int, COLON, real_expr_wrapper)
+            SEMICOLON, separated_pair (id_int, COLON, real_expr_err)
           ), CLOSECUR)), CLOSESQ)
     loc=INT
     TIMEOUT_MOD timer=INT effort=INT algo=ID horizon=INT?
@@ -196,8 +203,8 @@
   | GET_CMD LOC_MOD PLAYER_MOD loc=INT   { GetLocPlayer loc }
   | SET_CMD LOC_MOD loc=INT              { SetLoc loc }
   | GET_CMD LOC_MOD                      { GetLoc }
-  | EVAL_CMD OPEN phi=formula_expr CLOSE { EvalFormula phi }
-  | EVAL_CMD OPENSQ re=real_expr_wrapper CLOSESQ { EvalRealExpr re }
+  | EVAL_CMD OPEN phi=formula_expr_err CLOSE { EvalFormula phi }
+  | EVAL_CMD OPENSQ re=real_expr_err CLOSESQ { EvalRealExpr re }
   | SET_CMD DATA_MOD i=ID v=id_int       { SetData (i, v) }
   | GET_CMD DATA_MOD i=ID                { GetData i }
   | SET_CMD RULE_SPEC r=id_int rdef=rule_expr { SetRule (r, rdef) }
@@ -234,7 +241,7 @@
   | GET_CMD RULE_SPEC EMB r=id_int                 { GetRuleEmb r }
   | GET_CMD RULE_SPEC COND r=id_int                { GetRuleCond r }
   | SET_CMD RULE_SPEC COND r=id_int
-      pre=formula_expr inv=formula_expr post=formula_expr
+      pre=formula_expr_err inv=formula_expr_err post=formula_expr_err
       { SetRuleCond (r, pre, inv, post) }
   | error
     { raise (Lexer.Parsing_error "Syntax error in Server request.") }

Modified: trunk/Toss/Client/Makefile
===================================================================
--- trunk/Toss/Client/Makefile	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Client/Makefile	2011-05-07 22:30:43 UTC (rev 1433)
@@ -1,7 +1,8 @@
 all: Shapes.so
 
 Shapes.so: Shapes.c
-	gcc -fPIC Shapes.c -I/usr/include/python2.5/ -I/usr/include/python2.6/ -lm -lpthread -shared -o Shapes.so
+	gcc -fPIC Shapes.c -I/usr/include/python2.5/ -I/usr/include/python2.6/\
+	  -I/usr/include/python2.7/ -lm -lpthread -shared -o Shapes.so
 
 clean:
 	rm -rf *.pyc Shapes.so

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -524,7 +524,18 @@
 
 (* --------------------------- TRANSITIVE CLOSURE --------------------------- *)
 
-(* We construct transitive closure of phi(x, y, z) over x, y as
+(* We construct the lfp transitive closure of phi(x, y, z) over x, y as
+  "lfp T(y) = (y = x or ex n (n in T and phi (n, y, z)))" *)
+let make_lfp_tc x y phi =
+  let (fv, xv, yv) = (free_vars phi, fo_var_of_string x, fo_var_of_string y) in
+  let (_, nn) = subst_name_avoiding fv (fo_var_of_string "n") in
+  let nnv = fo_var_of_string nn in
+  let frT = mso_var_of_string(snd(subst_name_avoiding fv(var_of_string "T"))) in
+  let nphi = subst_vars [(x, nn)] phi in
+  let fpphi = Or [Eq (xv, yv); Ex([(nnv :> var)], And [In (nnv, frT); nphi])] in
+  Lfp ((frT :> [ mso_var | so_var ]), [|yv|], fpphi)
+
+(* We construct the mso transitive closure of phi(x, y, z) over x, y as
   "all X (x in X and (all x',y' 
       (x' in X and phi(x',y',z)-> y' in X)) -> y in X)" *)
 let make_mso_tc x y phi =

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-05-07 22:30:43 UTC (rev 1433)
@@ -137,6 +137,10 @@
 
 (** {2 Transitive Closure} *)
 
+
+(** Transitive closure of phi(x, y, z) over x and y, an LFP formula. *)
+val make_lfp_tc : string -> string -> formula -> formula
+
 (** Transitive closure of phi(x, y, z) over x and y, an MSO formula. *)
 val make_mso_tc : string -> string -> formula -> formula
 

Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Formula/FormulaParser.mly	2011-05-07 22:30:43 UTC (rev 1433)
@@ -89,7 +89,8 @@
   | NOT formula_expr        { Not ($2) }
   | EX var_list formula_expr         { Ex ($2, $3) }
   | ALL var_list formula_expr        { All ($2, $3) }
-  | TC ID COMMA ID formula_expr      { FormulaOps.make_mso_tc $2 $4 $5 }
+  | TC ID COMMA ID formula_expr      { FormulaOps.make_lfp_tc $2 $4 $5 }
+  | TC IN ID COMMA ID formula_expr   { FormulaOps.make_mso_tc $3 $5 $6 }
   | TC INT ID COMMA ID formula_expr  { FormulaOps.make_fo_tc_conj $2 $3 $5 $6 }
   | LFP ID OPEN fo_var_list CLOSE EQ formula_expr
       { let vs = Array.of_list $4 in if Array.length vs <> 1 then 

Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Formula/Lexer.mll	2011-05-07 22:30:43 UTC (rev 1433)
@@ -193,6 +193,7 @@
   | "false"         { FALSE }
   | "assoc"         { ASSOC }
   | "cond"          { COND }
+  | "COND"          { COND }
   | "PAYOFF"        { PAYOFF }
   | "MOVES"         { MOVES }
   | "ADD"           { ADD_CMD }

Modified: trunk/Toss/Play/Heuristic.ml
===================================================================
--- trunk/Toss/Play/Heuristic.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Play/Heuristic.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -267,7 +267,16 @@
   Times (Formula.pow n (int_of_float adv_ratio),
          Const (1. /. float_of_int m ** adv_ratio))
 
+let print_heur msg heur =
+  print_endline ("\nAll-Heuristics " ^ msg);
+  let print_heur_arr = Array.iteri (fun i heur ->
+    print_endline ("\n    for player " ^ (string_of_int i));
+    print_endline ("    " ^ Formula.sprint_real heur);) in
+  Array.iteri (fun i harr ->
+    print_endline ("\nHeuristic for location " ^ (string_of_int i));
+    print_heur_arr harr;) heur
 
+
 (* ********** Structure-Expanded Form ********** *)
 
 let rec has_rels frels = function

Modified: trunk/Toss/Play/Heuristic.mli
===================================================================
--- trunk/Toss/Play/Heuristic.mli	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Play/Heuristic.mli	2011-05-07 22:30:43 UTC (rev 1433)
@@ -59,6 +59,9 @@
 
 val debug_level : int ref
 
+(** Simple heuristic print helper. *)
+val print_heur : string -> Formula.real_expr array array -> unit
+
 (** Irrespective of the shape of payoffs, take the difference of
     heuristics as the final heuristic for each player (in
     {!Heuristic.default_heuristic_old}). *)

Modified: trunk/Toss/Server/ReqHandler.ml
===================================================================
--- trunk/Toss/Server/ReqHandler.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Server/ReqHandler.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -11,19 +11,33 @@
 
 let possibly_modifies_game = Arena.can_modify_game 
 
+let compute_heuristic advr (game, state) =
+  let pat_arr = Array.of_list game.Arena.patterns in
+  let pl_heur l = 
+    let len = List.length l.Arena.heur in
+    if len = 0 || len > Array.length pat_arr then raise Not_found else
+      let add_pat (i, h) pw = 
+	let pat = Formula.Times (Formula.Const pw, pat_arr.(i)) in
+	(i+1, Formula.Plus (pat, h)) in
+      snd (List.fold_left add_pat (0, Formula.Const 0.) l.Arena.heur) in
+  try
+    let res = Array.map (fun a-> Array.map pl_heur a) game.Arena.graph in
+    if !debug_level > 1 then Heuristic.print_heur "manual heur" res;
+    res
+  with Not_found ->
+    Heuristic.default_heuristic ~struc:state.Arena.struc ?advr game
+
 exception Found of int
 
 let req_handle g_heur game_modified state gdl_transl playclock = function 
 
   | Aux.Left (Arena.SuggestLocMoves
-                (loc, timer, effort, how, horizon, heuristic, advr)) -> (
+                (loc, timer, effort, _, _, heuristic, advr)) -> (
     Random.self_init ();
     Play.set_timeout (float(timer));
     let heur = match game_modified, g_heur with
       | false, Some h -> Some h
-      | true, _ | _, None -> 
-	Some (Heuristic.default_heuristic ~struc:(snd state).Arena.struc 
-		?advr (fst state)); in
+      | true, _ | _, None -> Some (compute_heuristic advr state) in
     let (move, _) = 
       Aux.random_elem (Play.maximax_unfold_choose effort
 			 (fst state) (snd state) (Aux.unsome heur)) in

Modified: trunk/Toss/Server/Server.ml
===================================================================
--- trunk/Toss/Server/Server.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Server/Server.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -1,6 +1,7 @@
 (* Server for Toss Functions. *)
 
 let debug_level = ref 0
+
 let set_debug_level i =
   debug_level := i;
   if i > 5 then Solver.set_debug_level 1;
@@ -102,7 +103,8 @@
     let (line, marshaled) = read_in_line in_ch in
     if line = "COMP" && marshaled <> None then (
       let (f, x) = Aux.unsome marshaled in
-      let res = Marshal.to_channel out_ch (f x) [Marshal.Closures] in
+      let res = f x in
+      Marshal.to_channel out_ch res [Marshal.Closures];
       flush out_ch;
     ) else
     let req = req_of_str line in
@@ -144,13 +146,18 @@
   let f = open_in fn in
   let s = ArenaParser.parse_game_state Lexer.lex (Lexing.from_channel f) in
   game_modified := true;
-  state := s
-;;
+  state := s;
+  let pats = (fst !state).Arena.patterns in
+  print_endline ("P: " ^ String.concat ", " (List.map Formula.real_str pats));
+  let ploc l = if l.Arena.heur <> [] then
+      print_endline ("H: " ^ String.concat ", " 
+			(List.map string_of_float l.Arena.heur)) in
+  Array.iter (fun l -> Array.iter ploc l) (fst !state).Arena.graph
 
-let heur_val_white1 = ref "";;
-let heur_val_black1 = ref "";;
-let heur_val_white2 = ref "";;
-let heur_val_black2 = ref "";;
+let heur_val_white1 = ref ""
+let heur_val_black1 = ref ""
+let heur_val_white2 = ref ""
+let heur_val_black2 = ref ""
 
 let heur_of_vals white_val black_val =
   let real_expr_of_str s = 
@@ -161,17 +168,8 @@
     real_expr_of_str ("("^black_val^") - ("^white_val^")") in
   let heuristic = [|white_heur; black_heur|] in
   Array.make (Array.length (fst !state).Arena.graph) heuristic
-;;
 
-let print_heur pl heur =
-  print_endline ("\nAll-Heuristics for player " ^ pl);
-  let print_heur_arr = Array.iteri (fun i heur ->
-    print_endline ("\n    for player " ^ (string_of_int i));
-    print_endline ("    " ^ Formula.sprint_real heur);) in
-  Array.iteri (fun i harr ->
-    print_endline ("\nHeuristic for location " ^ (string_of_int i));
-    print_heur_arr harr;) heur
-;;
+let print_heur pl heur = Heuristic.print_heur ("for player " ^ pl) heur
 
 let do_play game state depth1 depth2 advr heur1 heur2 =
   let cur_state = ref state in
@@ -194,7 +192,6 @@
   let payoffs = Array.map (fun l -> l.Arena.payoff)
     game.Arena.graph.(!cur_state.Arena.cur_loc) in
   Array.map (fun p -> Solver.M.get_real_val p (!cur_state).Arena.struc) payoffs
-;;
 
 let run_test n depth1 depth2 =
   let advr = 2.0 in
@@ -232,8 +229,7 @@
     aggr_payoff_w := !aggr_payoff_w +. payoff.(0);
     aggr_payoff_b := !aggr_payoff_b +. payoff.(1);
     Printf.printf "Aggregate payoffs %f, %f\n" !aggr_payoff_w !aggr_payoff_b;
-  ) done;
-;;
+  ) done
 
 
 (* ----------------------- START SERVER WHEN CALLED ------------------------- *)
@@ -312,7 +308,6 @@
     start_server req_handle !port !server
   with Aux.Host_not_found ->
     print_endline "The host you specified was not found."
-;;
 
 let _ =
   (* Test against being called from a test... *)
@@ -327,4 +322,4 @@
   (* so that the server is not started by the test suite. *)
   if not test_fname then (
     main ()
-  ) ;;
+  )

Modified: trunk/Toss/Solver/AssignmentSet.ml
===================================================================
--- trunk/Toss/Solver/AssignmentSet.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Solver/AssignmentSet.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -117,9 +117,10 @@
    in order in which [vars] are given. [elems] are all elements. *)
 let rec tuples elems vars = function
   | Empty -> []
-  | Any -> List.rev_map Array.of_list 
-    (Aux.product
-       (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
+  | Any ->
+    List.rev_map Array.of_list 
+      (Aux.product
+	 (List.rev_map (fun _ -> Structure.Elems.elements elems) vars))
   | FO (`FO v, (e,other_aset)::asg_list) when e < 0 ->
     let asg_list = List.map (fun e ->
       e, try List.assoc e asg_list with Not_found -> other_aset)

Modified: trunk/Toss/Solver/Assignments.ml
===================================================================
--- trunk/Toss/Solver/Assignments.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Solver/Assignments.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -68,7 +68,7 @@
    before join and join must take elems as argument. *)
 let small_simp l =
   let rec del_dupl acc = function
-      [] -> acc
+    | [] -> acc
     | [x] -> x :: acc 
     | x :: y :: xs when x = y -> del_dupl acc (y :: xs)
     | x :: y :: xs -> del_dupl (x :: acc) (y :: xs) in
@@ -86,7 +86,7 @@
     let r = small_simp (map_snd f m) in 
     if r=[] then Empty else MSO(v,r) in
   match (aset1, aset2) with
-      (Empty, _) | (_, Empty) -> Empty
+    | (Empty, _) | (_, Empty) -> Empty
     | (Any, a) -> a
     | (a, Any) -> a
     | (FO (v1, map1), FO (v2, map2)) -> (
@@ -119,7 +119,7 @@
           if poly_dnf = [] then Empty else Real (poly_dnf)
 
 and join_maps_rev acc = function
-    ([], _) -> acc
+  | ([], _) -> acc
   | (_, []) -> acc
   | ((e1, a1) :: r1, (e2, a2) :: r2) ->
       match compare_elems e1 e2 with
@@ -131,7 +131,7 @@
 	| x -> join_maps_rev acc (((e1, a1) :: r1), r2)
 
 and join_disj acc disj1 = function
-    [] -> acc
+  | [] -> acc
   | ((pos2, neg2), a2) :: rest ->
       let adjoin_one acc ((pos1, neg1), a1) =
         let (pos, neg) = (Elems.union pos2 pos1, Elems.union neg2 neg1) in
@@ -146,7 +146,7 @@
 
 (* Enforce [aset] and additionally that the FO variable [v] is set to [e]. *)
 let rec set_equal v e = function
-    Empty -> Empty
+  | Empty -> Empty
   | FO (u, map) as aset -> (
       match compare_vars (u :> Formula.var) (v :> Formula.var) with
           0 -> 
@@ -161,7 +161,7 @@
 
 (* Enforce that in [aset] the variable [u] is equal to [w]; assumes u < w. *)
 let rec eq_vars els u w = function
-    Empty -> Empty
+  | Empty -> Empty
   | FO (v, map) as aset -> (
       match compare_vars (v :> Formula.var) (u :> Formula.var) with
           0 -> 
@@ -179,7 +179,7 @@
 (* Enforce that in [aset] the variable [u] is equal to [w]. *)
 let equal_vars elems u w aset =
   match compare_vars (u :> Formula.var) (w :> Formula.var) with
-      0 -> aset (* TODO: with one var is assigned, we could be more efficient *)
+    | 0 -> aset (* TODO: with one var is assigned, we could be more efficient *)
     | x when x < 0 -> eq_vars elems u w aset
     | _ -> eq_vars elems w u aset
 
@@ -202,12 +202,12 @@
    We assume that [elems] are sorted. Corresponds to disjunction of formulas. *)
 let rec sum elems aset1 aset2 = 
   match (aset1, aset2) with
-      (Any, _) | (_, Any) -> Any
+    | (Any, _) | (_, Any) -> Any
     | (Empty, a) -> a
     | (a, Empty) -> a
     | (FO (v1, map1), FO (v2, map2)) -> (
 	match compare_vars (v1 :> Formula.var) (v2 :> Formula.var) with
-	    0 -> 
+	  | 0 -> 
 	      let res_map = List.rev (sum_maps_rev elems [] (map1, map2)) in
 		if is_full elems res_map then Any else FO (v1, res_map)
 	  | x when x < 0 -> 
@@ -253,7 +253,7 @@
         Real (List.rev_append poly_disj1 poly_disj2)
 
 and sum_maps_rev elems acc = function
-    ([], m) -> List.rev_append m acc
+  | ([], m) -> List.rev_append m acc
   | (m, []) -> List.rev_append m acc
   | ((e1, a1) :: r1, (e2, a2) :: r2) ->
       match compare_elems e1 e2 with
@@ -276,7 +276,7 @@
 (* Project assignments on a given variable. We assume that [elems] are all
    elements and are sorted. Corresponds to the existential quantifier. *)
 let rec project elems v = function
-    Empty -> Empty
+  | Empty -> Empty
   | Any -> Any
   | FO (u, m) when (u :> Formula.var) = v -> (* Sum the assignments below *)
       List.fold_left (fun s (_, a) -> sum elems s a) Empty m
@@ -317,7 +317,7 @@
 (* Project assignments on a given universal variable. We assume that [elems]
    are all elements and are sorted. Corresponds to the for-all v quantifier. *)
 let rec universal elems v = function
-    Empty -> Empty
+  | Empty -> Empty
   | Any -> Any
   | FO (u, m) when (u :> Formula.var) = v -> (* Join the assignments below *)
       if List.length m < sllen elems then Empty else
@@ -347,7 +347,7 @@
       let neg_disj = negate_real_disj poly_disj in
         if neg_disj = [] then Any else
           match project elems v (Real (neg_disj)) with
-              Any -> Empty
+            | Any -> Empty
             | Real disj -> 
                 let nd = negate_real_disj disj in
                   if nd = [] then Empty else Real nd
@@ -363,29 +363,29 @@
 (* Complement an assignment set assuming [elems] are all assignable elements. 
    We assume [elems] are sorted. This corresponds to negation of formulas. *)
 let rec complement elems = function
-    Empty -> Any
+  | Empty -> Any
   | Any -> Empty
   | FO (v, map) -> 
-      let compl_map = 
-        List.rev (complement_map_rev elems [] (slist elems, map)) in
-      if compl_map = [] then Empty else FO (v, compl_map)
+    let compl_map = 
+      List.rev (complement_map_rev elems [] (slist elems, map)) in
+    if compl_map = [] then Empty else FO (v, compl_map)
   | MSO (v, disj) -> 
-      let compl_disj = complement_disj elems disj in
-        if compl_disj = [] then Empty else MSO (v, compl_disj)
+    let compl_disj = complement_disj elems disj in
+    if compl_disj = [] then Empty else MSO (v, compl_disj)
   | Real poly_disj -> Real (negate_real_disj poly_disj)
 
 and complement_map_rev elems acc = function
-    ([], []) -> acc
+  | ([], []) -> acc
   | ([], _) -> failwith "more assigned elements as elements at all"
   | (e::es, []) -> complement_map_rev elems ((e, Any)::acc) (es, [])
   | (e1 :: es, (e2, a) :: ms) ->
       match compare_elems e1 e2 with
-          0 -> 
-            let compl = complement elems a in
-              if compl = Empty then complement_map_rev elems acc (es, ms) else
-                complement_map_rev elems ((e1, compl)::acc) (es, ms)
+        | 0 -> 
+          let compl = complement elems a in
+          if compl = Empty then complement_map_rev elems acc (es, ms) else
+            complement_map_rev elems ((e1, compl)::acc) (es, ms)
         | x when x < 0 ->
-            complement_map_rev elems ((e1, Any)::acc) (es, (e2, a) :: ms)
+          complement_map_rev elems ((e1, Any)::acc) (es, (e2, a) :: ms)
         | _ -> failwith "assigned element not in the set of all elements"
 
 and complement_disj elems disj =
@@ -419,7 +419,7 @@
 (* Complement [a] and join with [aset]; assumes [a] is joined with [aset] *)
 let rec complement_join elems aset a =
   match (aset, a) with
-      (Empty, _) | (_, Any) -> Empty
+    | (Empty, _) | (_, Any) -> Empty
     | (Any, a) -> complement elems a
     | (a, Empty) -> a
     | (FO (v1, map1), FO (v2, map2)) when v1 = v2 ->
@@ -429,7 +429,7 @@
     | _ -> join aset (complement elems a)
 
 and complement_join_map_rev elems acc = function
-    ([], []) -> acc
+  | ([], []) -> acc
   | ([], _) -> failwith "complement-join-map: set to complement too big (1)"
   | (map, []) -> List.rev_append map acc
   | ((e1, aset) :: es, (e2, a) :: ms) ->
@@ -450,7 +450,7 @@
 (* Helper function to remove duplicate assignments to variables and append.*)
 let remove_dup_append assgn_list asgn =
   let rec remove_dup acc = function
-      [] -> acc :: assgn_list
+    | [] -> acc :: assgn_list
     | [x] -> (x :: acc) :: assgn_list
     | (v1, e1) :: (v2, e2) :: xs when v1 = v2 ->
 	if e1 = e2 then remove_dup acc ((v2, e2) :: xs) else assgn_list
@@ -469,7 +469,7 @@
   let make_append l t = remove_dup_append l (make_assign t) in
   let asgn_list = List.fold_left make_append [] tl in
   let rec set_of_single = function
-      [] -> Empty
+    | [] -> Empty
     | [(v, e)] -> FO (v, [(e, Any)])
     | (v, e) :: rest -> FO (v, [(e, set_of_single rest)])
   in
@@ -480,7 +480,7 @@
 
 let rec join_rel aset vars tuples_set incidence_map all_elems =
   match aset with (* TODO: better use of incidence map? *)
-      Empty -> Empty
+    | Empty -> Empty
     | FO (v, map) when Aux.array_mem v vars -> 
         let tps e = 
           try IntMap.find e incidence_map with Not_found -> Tuples.empty in
@@ -495,3 +495,16 @@
   let tuples = Tuples.elements tuples_set in
   let rel_aset = assignments_of_list all_elems vars tuples in
     join aset rel_aset
+
+(* ------------ SIMPLE VARIABLE COMPRESSION ---------- *)
+
+let rec same_asg = function
+  | [] | [_] -> true
+  | (_, a1) :: (((_, a2) :: _) as r) when a1 = a2 -> same_asg r
+  | _ -> false
+
+let rec compress no_elems = function
+  | FO (v, map) when List.length map = no_elems && same_asg map ->
+    compress no_elems (snd (List.hd map))
+  | FO (v, map) -> FO (v, map_snd (compress no_elems) map)
+  | x -> x

Modified: trunk/Toss/Solver/Assignments.mli
===================================================================
--- trunk/Toss/Solver/Assignments.mli	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Solver/Assignments.mli	2011-05-07 22:30:43 UTC (rev 1433)
@@ -104,6 +104,12 @@
   Structure.Tuples.t -> set_list ref -> assignment_set
 
 
+(** {2 Basic univeral variable compression} *)
+
+(** Compress the given assignment set, use number of elements. *)
+val compress : int -> assignment_set -> assignment_set
+
+
 (** {2 Debugging} *)
 
 

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Solver/Solver.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -98,9 +98,10 @@
     if !debug_level > 1 then print_endline ("Got: " ^ (AssignmentSet.str res));
     res in
   if !debug_level > 1 then print_endline ("Evaluating: " ^ (str phi)) else ();
-  let fp_split vl nasg =
-    let vlen, vs = Array.length vl, (Array.to_list vl :> var list) in
-    let avars = List.map to_fo (AssignmentSet.assigned_vars [] nasg) in
+  let fp_split vs nasg =
+    let vlen = List.length vs in
+    let avars = 
+      Aux.unique_sorted (List.map to_fo(AssignmentSet.assigned_vars [] nasg)) in
     let ovars = List.filter (fun v -> not (List.mem (v :> var) vs)) avars in
     let vars = vs @ (ovars :> var list) in
     let tps = AssignmentSet.tuples (Assignments.sset elems)
@@ -108,20 +109,23 @@
     let split tp = 
       if Array.length tp = vlen then (tp, [||]) else
 	Array.sub tp 0 vlen, Array.sub tp vlen ((Array.length tp) - vlen) in
-    let asplit tp =
-      let (vasg, rst) = split tp in
-      ((if rst = [||] then Any else
-          Assignments.assignments_of_list elems (Array.of_list ovars) [rst]),
+    let asplit (vasg, rst) =
+      ((if List.hd rst = [||] then Any else
+          Assignments.assignments_of_list elems (Array.of_list ovars) rst),
        vasg) in
-    Aux.collect (List.map asplit tps) in
-  let fp_next v vl psi nasg =
+    let res= Aux.collect (List.map asplit (Aux.collect (List.map split tps))) in
+    if !debug_level > 1 then Printf.printf "rlen %i\n%!" (List.length res);
+    res in
+  let fp_next v vs psi nasg =
     let nx (a, vsl) =
       eval ((v, Structure.tuples_of_list vsl)::fp) model elems a psi in
     List.fold_left (fun acc a -> Assignments.sum elems (nx a) acc)
-      Empty (fp_split vl nasg) in
-  let rec fixpnt v vl psi a =
-    let nxt = fp_next v vl psi a in
-    if nxt = a then nxt else fixpnt v vl psi nxt in
+      Empty (fp_split vs nasg) in
+  let rec fixpnt v vs psi a =
+    if !debug_level > 1 then print_endline "Fixed-point step.";
+    let nxt = report(fp_next v vs psi a) in
+    if nxt = a then nxt else fixpnt v vs psi nxt in
+  let simp a = Assignments.compress (Assignments.sllen elems) a in
   if aset = Empty then Empty else
     match phi with
       | Rel (relname, vl) ->
@@ -178,23 +182,29 @@
 	let in_aset =
 	  if List.exists (fun v->List.mem v aset_vars) vl then Any else aset in
         let phi_asgn = eval fp model elems in_aset phi in
-        report (join aset (project_list elems phi_asgn vl))
+        report (simp (join aset (project_list elems phi_asgn vl)))
       | All (vl, phi) ->
 	check_timeout "Solver.eval.All";
 	let aset_vars = AssignmentSet.assigned_vars [] aset in
 	let in_aset =
 	  if List.exists (fun v->List.mem v aset_vars) vl then Any else aset in
         let phi_asgn = eval fp model elems in_aset phi in
-        report (join aset (universal_list elems phi_asgn vl))
+        report (simp (join aset (universal_list elems phi_asgn vl)))
       | Lfp (v, vl, phi) ->
-	let a0 = eval ((v, Structure.Tuples.empty)::fp) model elems aset phi in
-	report (if a0 = Empty then Empty else fixpnt v vl phi a0)
-      | Gfp (v, vl, phi) -> 
+	let vll = (Array.to_list vl :> var list) in
+	let asg0 = simp (project_list elems aset vll) in
+	let a0 = eval ((v, Structure.Tuples.empty)::fp) model elems asg0 phi in
+	let fp_res = if a0 = Empty then Empty else fixpnt v vll phi a0 in
+	report (simp (join aset fp_res))
+      | Gfp (v, vl, phi) ->
+	let vll = (Array.to_list vl :> var list) in
+	let asg0 = simp (project_list elems aset vll) in
 	let alltps = Structure.tuples_of_list
 	  (AssignmentSet.tuples (Assignments.sset elems)
 	     (List.map var_str ((Array.to_list vl) :> var list)) Any) in
-	let a0 = eval ((v, alltps)::fp) model elems aset phi in
-	report (if a0 = Empty then Empty else fixpnt v vl phi a0)
+	let a0 = eval ((v, alltps)::fp) model elems asg0 phi in
+	let fp_res = if a0 = Any then Any else fixpnt v vll phi a0 in
+	report (simp (join aset fp_res))
 
 and assignment_of_real_expr fp ?(check=true) model elems (p, sgn) =
   let rec fo_vars_r_rec = function

Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/Solver/SolverTest.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -111,12 +111,12 @@
 
   "eval: mso with quantifiers" >::
     (fun () ->
-      eval_eq "[ | R { (a, b); (a, c) } | ]" "tc x, y R(x, y)"
+      eval_eq "[ | R { (a, b); (a, c) } | ]" "tc in x, y R(x, y)"
 	"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 }  }";
-      eval_eq "[ | R { (a, b); (b, c) } | ]" "tc x, y R(x, y)"
+      eval_eq "[ | R { (a, b); (b, c) } | ]" "tc in x, y R(x, y)"
 	"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
       eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]" 
-	"x != y and not R(x, y) and tc x, y R(x, y)"
+	"x != y and not R(x, y) and tc in x, y R(x, y)"
 	("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
 	    " y->6{ x->1, x->2, x->3, x->4 } , y->7{ x->1, x->2, x->3, x->4," ^
 	    " x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 }  }");
@@ -134,7 +134,7 @@
 
   "eval: fixed-points" >::
     (fun () ->
-      eval_eq "[ | P (a)  | ]" "lfp T(x) = P(x)" "{ x->1 }";
+      eval_eq "[a, b | P (a)  | ]" "lfp T(x) = P(x)" "{ x->1 }";
       eval_eq "[ | P:1 {} | ]" "lfp T(x) = P(x)" "{}";
       eval_eq "[ | R { (a, b); (b, c) } | ]"
 	"lfp T(x) = (x = y or ex z (z in T and R (x, z)))"
@@ -142,47 +142,16 @@
       eval_eq "[ | R { (a, b); (b, a); (b, c) } | ]"
 	"gfp T(x) = (x != y and x in T and all z (R (x, z) -> z in T))"
 	"{ y->1{ x->3 } , y->2{ x->3 }  }";
-    );
 
-  "eval: bigger tc tests" >::
-    (fun () ->
-      let diag_phi = 
-        "set d1(x, y) = ex z ((R(x, z) and C(z, y)) or (R(y, z) and C(z, x))) in
-         set d2(x, y) = ex z ((R(x, z) and C(y, z)) or (R(y, z) and C(x, z))) in
-         set w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x) in
-         set b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x) in
-         set fd1(x, y) = tc x,y (d1(x, y) and not w(y) and not b(y)) in
-         set fd2(x, y) = tc x,y (d2(x, y) and not w(y) and not b(y)) in
-         set Diag1 (x, y) = ex z (fd1 (x, z) and (z = y or d1 (z, y))) in
-         set Diag2 (x, y) = ex z (fd2 (x, z) and (z = y or d2 (z, y))) in
-         wB(x) and (Diag1 (x, y) or Diag2 (x, y))" in
-      eval_eq "[  |  |  ] \"
-	   ...   ...
-	   ...   ...
-	...   ...   
-	...   ...   
-	   ...   ...
-	   ...   ...
-	...   ...   
-	...   wB.   
-\"" diag_phi
-	"{ y->3{ x->3 } , y->6{ x->3 } , y->8{ x->3 } , y->9{ x->3 }  }";
-(*      eval_eq "[  |  |  ] \"
-	   ...   ...   ...
-	   ...   ...   ...
-	...   ...   ...   
-	...   ...   ...   
-	   ...   ...   ...
-	   ...   ...   ...
-	...   ...   ...   
-	...   ...   ...   
-	   ...   ...   ...
-	   ...   ...   ...
-	...   ...   ...   
-	...   wB.   ...   
-\"" diag_phi
-	("{ y->3{ x->3 } , y->8{ x->3 } , y->10{ x->3 } ," ^
-	    " y->13{ x->3 } , y->17{ x->3 } , y->24{ x->3 }  }"); *)
+      eval_eq "[ | R { (a, b); (a, c) } | ]" "tc x, y R(x, y)"
+	"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3{ x->1, x->3 }  }";
+      eval_eq "[ | R { (a, b); (b, c) } | ]" "tc x, y R(x, y)"
+	"{ y->1{ x->1 } , y->2{ x->1, x->2 } , y->3 }";
+      eval_eq "[ | R { (a,b); (b,c); (c,d); (d,e); (e,f); (f,g); (g,h) } | ]" 
+	"x != y and not R(x, y) and tc x, y R(x, y)"
+	("{ y->3{ x->1 } , y->4{ x->1, x->2 } , y->5{ x->1, x->2, x->3 } ," ^
+	    " y->6{ x->1, x->2, x->3, x->4 } , y->7{ x->1, x->2, x->3, x->4," ^
+	    " x->5 } , y->8{ x->1, x->2, x->3, x->4, x->5, x->6 }  }");
     );
 
   "eval: with real values" >::
@@ -271,48 +240,171 @@
 ]
 
 
-let exec = Aux.run_test_if_target "SolverTest" tests
+let bigtests = "SolverBig" >::: [
+  "eval: bigger tc tests" >::
+    (fun () ->
+      let diag_phi_mso = 
+        "set d1(x, y) = ex z ((R(x, z) and C(z, y)) or (R(y, z) and C(z, x))) in
+         set d2(x, y) = ex z ((R(x, z) and C(y, z)) or (R(y, z) and C(x, z))) in
+         set w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x) in
+         set b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x) in
+         set fd1(x, y) = tc in x,y (d1(x, y) and not w(y) and not b(y)) in
+         set fd2(x, y) = tc in x,y (d2(x, y) and not w(y) and not b(y)) in
+         set Diag1 (x, y) = ex z (fd1 (x, z) and (z = y or d1 (z, y))) in
+         set Diag2 (x, y) = ex z (fd2 (x, z) and (z = y or d2 (z, y))) in
+         wB(x) and (Diag1 (x, y) or Diag2 (x, y))" in
+      eval_eq "[  |  |  ] \"
+	   ...   ...
+	   ...   ...
+	...   ...   
+	...   ...   
+	   ...   ...
+	   ...   ...
+	...   ...   
+	...   wB.   
+\"" diag_phi_mso
+	"{ y->3{ x->3 } , y->6{ x->3 } , y->8{ x->3 } , y->9{ x->3 }  }";
 
+      let diag_phi = 
+        "set d1(x, y) = ex z ((R(x, z) and C(z, y)) or (R(y, z) and C(z, x))) in
+         set d2(x, y) = ex z ((R(x, z) and C(y, z)) or (R(y, z) and C(x, z))) in
+         set w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x) in
+         set b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x) in
+         set fd1(x, y) = tc x,y (d1(x, y) and not w(y) and not b(y)) in
+         set fd2(x, y) = tc x,y (d2(x, y) and not w(y) and not b(y)) in
+         set Diag1 (x, y) = ex z (fd1 (x, z) and (z = y or d1 (z, y))) in
+         set Diag2 (x, y) = ex z (fd2 (x, z) and (z = y or d2 (z, y))) in
+         wB(x) and (Diag1 (x, y) or Diag2 (x, y))" in
+      eval_eq "[  |  |  ] \"
+	   ...   ...   ...
+	   ...   ...   ...
+	...   ...   ...   
+	...   ...   ...   
+	   ...   ...   ...
+	   ...   ...   ...
+	...   ...   ...   
+	...   ...   ...   
+	   ...   ...   ...
+	   ...   ...   ...
+	...   ...   ...   
+	...   wB.   ...   
+\"" diag_phi 
+	("{ y->3{ x->3 } , y->8{ x->3 } , y->10{ x->3 } , " ^ 
+	    "y->13{ x->3 } , y->17{ x->3 } , y->24{ x->3 }  }");
 
+      let chess_phi = "
+set D1(x, y) = ex z ( (R(x, z) and C(z, y)) or (R(y, z) and C(z, x)) ) in
+set D2(x, y) = ex z ( (R(x, z) and C(y, z)) or (R(y, z) and C(x, z)) ) in
+set IsFirst(x) = not ex z C(z, x) in
+set IsSecond(x) = ex y (C(y, x) and IsFirst(y)) in
+set IsEight(x) = not ex z C(x, z) in
+set IsSeventh(x) = ex y (C(x, y) and IsEight(y)) in
+set IsA1(x) = not ex z R(z, x) and IsFirst(x) in
+set IsH1(x) = not ex z R(x, z) and IsFirst(x) in
+set IsA8(x) = not ex z R(z, x) and IsEight(x) in
+set IsH8(x) = not ex z R(x, z) and IsEight(x) in
+set w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x) in
+set b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x) in
+set DoubleC(x, y) = ex z ((C(x, z) and C(z, y)) or (C(y, z) and C(z, x))) in
+set DoubleR(x, y) = ex z ((R(x, z) and R(z, y)) or (R(y, z) and R(z, x))) in
+set KnightRCC(x, y) = ex z ((R(x, z) or R(z, x)) and DoubleC(z, y)) in
+set KnightCRR(x, y) = ex z ((C(x, z) or C(z, x)) and DoubleR(z, y)) in
+set Knight(x, y) = KnightRCC(x, y) or KnightCRR(x, y) in
+set FreeD1 (x, y) = tc x, y (D1 (x, y) and not w(y) and not b(y)) in
+set FreeD2 (x, y) = tc x, y (D2 (x, y) and not w(y) and not b(y)) in
+set Diag1 (x, y) = ex z (FreeD1 (x, z) and (z = y or D1 (z, y))) in
+set Diag2 (x, y) = ex z (FreeD2 (x, z) and (z = y or D2 (z, y))) in
+set Diag (x, y) = Diag1 (x, y) or Diag2 (x, y) in
+set FreeC (x, y) = tc x, y ((C(x, y) or C(y, x)) and not w(y) and not b(y)) in
+set FreeR (x, y) = tc x, y ((R(x, y) or R(y, x)) and not w(y) and not b(y)) in
+set Col (x, y) = ex z (FreeC (x, z) and (z = y or (C(z, y) or C(y, z)))) in
+set Row (x, y) = ex z (FreeR (x, z) and (z = y or (R(z, y) or R(y, z)))) in
+set Line (x, y) = Col (x, y) or Row (x, y) in
+set Near(x, y) = C(x,y) or C(y,x) or R(x,y) or R(y,x) or D1(x, y) or D2(x, y) in
+set wPBeats (x) = ex y (wP(y) and ex z ((R(y, z) or R(z, y)) and C(z, x))) in
+set bPBeats (x) = ex y (bP(y) and ex z ((R(y, z) or R(z, y)) and C(x, z))) in
+set wDiagBeats (x) = ex y ((wQ(y) or wB(y)) and Diag(y, x)) in
+set bDiagBeats (x) = ex y ((bQ(y) or bB(y)) and Diag(y, x)) in
+set wLineBeats (x) = ex y ((wQ(y) or wR(y)) and Line(y, x)) in
+set bLineBeats (x) = ex y ((bQ(y) or bR(y)) and Line(y, x)) in
+set wFBeats(x)= wDiagBeats(x) or wLineBeats(x) or ex y(wN(y) and Knight(y,x)) in
+set bFBeats(x)= bDiagBeats(x) or bLineBeats(x) or ex y(bN(y) and Knight(y,x)) in
+set wBeats(x) = wFBeats(x) or wPBeats(x) or ex y (wK(y) and Near(y, x)) in
+set bBeats(x) = bFBeats(x) or bPBeats(x) or ex y (bK(y) and Near(y, x)) in
+set CheckW() = ex x (wK(x) and bBeats(x)) in
+set CheckB() = ex x (bK(x) and wBeats(x)) in " in
+      eval_eq "[  |  |  ] \"
+	   ...   ...   ...   ...
+	bR bN.bB bQ.bK bB.bN bR.
+	...   ...   ...   ...   
+	bP.bP bP.bP bP.bP bP.bP 
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	   ...   ...   ...   ...
+	...   ...   ...   ...   
+	...   ...   ...   ...   
+	   ...   ...   ...   ...
+	wP wP.wP wP.wP wP.wP wP.
+	...   ...   ...   ...   
+	wR.wN wB.wQ wK.wB wN.wR 
+\"" (chess_phi ^ "IsA8(x) and not CheckW()") "{ x->57 }";
+    );
 
-
-(* ----------------------- FOUR POINTS PROBLEM --------------------------- *)
-
-(*
-test_eval "[ | P {x}; Q {y}; Z {z}; S {v} | ]"
- "ex :px, :py, :qx, :qy, :zx, :zy, :sx, :sz all X ex :rt, :rb, :rl, :rr all x(
+  (*"eval: four points problem" >::
+    (fun () ->
+      Solver.set_debug_level 3;
+      FormulaOps.set_debug_level 3;
+      BoolFormula.set_debug_level 3;
+      Sat.set_debug_level 3;
+      eval_eq "[ | P {x}; Q {y}; Z {z}; S {v} | ]"
+	("ex :px, :py, :qx, :qy, :zx, :zy, :sx, :sz all X ex :rt,:rb,:rl,:rr" ^
+	    " all x(
     (P(x) -> (x in X <-> (:px>:rl and :px<:rr and :py>:rb and :py<:rt))) and
     (Q(x) -> (x in X <-> (:qx>:rl and :qx<:rr and :qy>:rb and :qy<:rt))) and
     (Z(x) -> (x in X <-> (:zx>:rl and :zx<:rr and :zy>:rb and :zy<:rt))) and
-    (S(x) -> (x in X <-> (:sx>:rl and :sx<:rr and :sy>:rb and :sy<:rt))))"
-*)
+    (S(x) -> (x in X <-> (:sx>:rl and :sx<:rr and :sy>:rb and :sy<:rt))))")
+	"";
+    );
 
+  "eval: four coloring problem" >::
+    (fun () ->
+      let four_color_f = "all a, b, c, d
+        (C(a,b) and C(c, d) and R(a,c) and R(b,d) -> (
+        not (a in C1 and b in C1 and c in C1 and d in C1) and
+        not (a in C2 and b in C2 and c in C2 and d in C2) and
+        not (a in C3 and b in C3 and c in C3 and d in C3) and
+        not (a in C4 and b in C4 and c in C4 and d in C4) ))" in
+      let rec linear_order name do_pref i =
+	let elem j = 
+	  if do_pref then 
+	    name ^ (string_of_int j) 
+	  else (string_of_int j) ^ name in
+	let rec all_from j = 
+	  let str = "(" ^ (elem j) ^ ", " ^ (elem i) ^ ")" in
+	  if j = i - 1 then str else str ^ ", " ^ (all_from (j+1)) in
+	if i = 2 then "(" ^ (elem 1) ^ ", " ^ (elem 2) ^ ")" else
+	  (linear_order name do_pref (i-1)) ^ ", " ^ (all_from 1) in
 
-(* ---------------------- FOUR COLORING PROBLEM --------------------------- *)
+      let grid n =
+	let rec upto i = if i = 1 then [1] else (upto (i-1)) @ [i] in
+	let col i = linear_order (string_of_int i) true n in
+	let row i = linear_order (string_of_int i) false n in
+	let cols = String.concat "; " (List.map col (upto n)) in
+	let rows = String.concat "; " (List.map row (upto n)) in
+	"[ | C { " ^ cols ^ " }; R { " ^ rows ^ " } | ]" in
 
-let four_color_f = "all a, b, c, d
-  (C(a,b) and C(c, d) and R(a,c) and R(b,d) -> (
-    not (a in C1 and b in C1 and c in C1 and d in C1) and
-    not (a in C2 and b in C2 and c in C2 and d in C2) and
-    not (a in C3 and b in C3 and c in C3 and d in C3) and
-    not (a in C4 and b in C4 and c in C4 and d in C4) ))"
+      Solver.set_debug_level 3;
+      FormulaOps.set_debug_level 3;
+      BoolFormula.set_debug_level 3;
+      Sat.set_debug_level 3;
+      eval_eq (grid 2) four_color_f "";
+    );*)
+]
 
-let rec linear_order name do_pref i =
-  let elem j = 
-    if do_pref then name ^ (string_of_int j) else (string_of_int j) ^ name in
-  let rec all_from j = 
-    let str = "(" ^ (elem j) ^ ", " ^ (elem i) ^ ")" in
-      if j = i - 1 then str else str ^ ", " ^ (all_from (j+1))
-  in
-    if i = 2 then "(" ^ (elem 1) ^ ", " ^ (elem 2) ^ ")" else
-      (linear_order name do_pref (i-1)) ^ ", " ^ (all_from 1)
 
-let grid n =
-  let rec upto i = if i = 1 then [1] else (upto (i-1)) @ [i] in
-  let col i = linear_order (string_of_int i) true n in
-  let row i = linear_order (string_of_int i) false n in
-  let cols = String.concat ", " (List.map col (upto n)) in
-  let rows = String.concat ", " (List.map row (upto n)) in
-    "[ | C { " ^ cols ^ " }; R { " ^ rows ^ " } | ]"
+let exec = Aux.run_test_if_target "SolverTest" tests
 
-(* test_eval (grid 2) four_color_f ;; *)
+let execbig = Aux.run_test_if_target "SolverTest" bigtests

Modified: trunk/Toss/TossFullTest.ml
===================================================================
--- trunk/Toss/TossFullTest.ml	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/TossFullTest.ml	2011-05-07 22:30:43 UTC (rev 1433)
@@ -15,6 +15,7 @@
   StructureTest.tests;
   AssignmentsTest.tests;
   SolverTest.tests;
+  SolverTest.bigtests;
   ClassTest.tests;
   ClassTest.bigtests;
 ]

Modified: trunk/Toss/examples/Chess.toss
===================================================================
--- trunk/Toss/examples/Chess.toss	2011-05-07 00:43:34 UTC (rev 1432)
+++ trunk/Toss/examples/Chess.toss	2011-05-07 22:30:43 UTC (rev 1433)
@@ -1,5 +1,15 @@
 PLAYERS 1, 2
 DATA depth: 0, adv_ratio: 1
+SET Sum (x | wP(x) : 1)
+SET Sum (x | wR(x) : 1)
+SET Sum (x | wN(x) : 1)
+SET Sum (x | wB(x) : 1)
+SET Sum (x | wQ(x) : 1)
+SET Sum (x | bP(x) : 1)
+SET Sum (x | bR(x) : 1)
+SET Sum (x | bN(x) : 1)
+SET Sum (x | bB(x) : 1)
+SET Sum (x | bQ(x) : 1)
 REL IsFirst(x) = not ex z C(z, x)
 REL IsSecond(x) = ex y (C(y, x) and IsFirst(y))
 REL IsEight(x) = not ex z C(x, z)
@@ -15,13 +25,13 @@
 REL KnightRCC(x, y) = ex z ((R(x, z) or R(z, x)) and DoubleC(z, y))
 REL KnightCRR(x, y) = ex z ((C(x, z) or C(z, x)) and DoubleR(z, y))
 REL Knight(x, y) = KnightRCC(x, y) or KnightCRR(x, y)
-REL FreeD1 (x, y) = tc 6 x, y (D1 (x, y) and not w(y) and not b(y))
-REL FreeD2 (x, y) = tc 6 x, y (D2 (x, y) and not w(y) and not b(y))
+REL FreeD1 (x, y) = tc x, y (D1 (x, y) and not w(y) and not b(y))
+REL FreeD2 (x, y) = tc x, y (D2 (x, y) and not w(y) and not b(y))
 REL Diag1 (x, y) = ex z (FreeD1 (x, z) and (z = y or D1 (z, y)))
 REL Diag2 (x, y) = ex z (FreeD2 (x, z) and (z = y or D2 (z, y)))
 REL Diag (x, y) = Diag1 (x, y) or Diag2 (x, y)
-REL FreeC (x, y) = tc 6 x, y ((C(x, y) or C(y, x)) and not w(y) and not b(y))
-REL FreeR (x, y) = tc 6 x, y ((R(x, y) or R(y, x)) and not w(y) and not b(y))
+REL FreeC (x, y) = tc x, y ((C(x, y) or C(y, x)) and not w(y) and not b(y))
+REL FreeR (x, y) = tc x, y ((R(x, y) or R(y, x)) and not w(y) and not b(y))
 REL Col (x, y) = ex z (FreeC (x, z) and (z = y or (C(z, y) or C(y, z))))
 REL Row (x, y) = ex z (FreeR (x, z) and (z = y or (R(z, y) or R(y, z))))
 REL Line (x, y) = Col (x, y) or Row (x, y)
@@ -314,6 +324,7 @@
 " emb w,b pre not (wBeats(a1) or wBeats(b1) or wBeats(c1)) post true
 LOC 0 { // both can castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 1];
@@ -333,10 +344,14 @@
    [WhiteRightCastle -> 7];
    [WhiteKing -> 7]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 1 { // both can castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 0];
@@ -356,10 +371,14 @@
     [BlackRightCastle -> 24];
     [BlackKing -> 24]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 2 { // w left, b can castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 3];
@@ -378,10 +397,14 @@
    [WhiteLeftCastle -> 7];
    [WhiteKing -> 7]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 3 { // w left, b can castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 2];
@@ -401,10 +424,14 @@
     [BlackRightCastle -> 26];
     [BlackKing -> 26]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 4 { // w right, b can castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 5];
@@ -423,10 +450,14 @@
    [WhiteRightCastle -> 7];
    [WhiteKing -> 7]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 5 { // w right, b can castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 4];
@@ -446,10 +477,14 @@
     [BlackRightCastle -> 28];
     [BlackKing -> 28]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 6 { // w no, b can castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 7];
@@ -467,10 +502,14 @@
    [WhiteQueen -> 7];
    [WhiteKing -> 7]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 7 { // w no, b can castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 6];
@@ -490,10 +529,14 @@
     [BlackRightCastle -> 30];
     [BlackKing -> 30]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 8 { // w can, b left castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 9];
@@ -513,10 +556,14 @@
    [WhiteRightCastle -> 15];
    [WhiteKing -> 15]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 9 { // w can, b left castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 8];
@@ -535,10 +582,14 @@
     [BlackLeftCastle -> 24];
     [BlackKing -> 24]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 10 { // w left, b left castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 11];
@@ -557,10 +608,14 @@
    [WhiteLeftCastle -> 15];
    [WhiteKing -> 15]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 11 { // w left, b left castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 10];
@@ -579,10 +634,14 @@
     [BlackLeftCastle -> 26];
     [BlackKing -> 26]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 12 { // w right, b left castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 13];
@@ -601,10 +660,14 @@
    [WhiteRightCastle -> 15];
    [WhiteKing -> 15]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 13 { // w right, b left castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 12];
@@ -623,10 +686,14 @@
     [BlackLeftCastle -> 28];
     [BlackKing -> 28]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 14 { // w no, b left castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 15];
@@ -644,10 +711,14 @@
    [WhiteQueen -> 15];
    [WhiteKing -> 15]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 15 { // w no, b left castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 14];
@@ -666,10 +737,14 @@
     [BlackLeftCastle -> 30];
     [BlackKing -> 30]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 16 { // w can, b right castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 17];
@@ -689,10 +764,14 @@
    [WhiteRightCastle -> 23];
    [WhiteKing -> 23]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 17 { // w can, b right castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 16];
@@ -711,10 +790,14 @@
     [BlackRightCastle -> 24];
     [BlackKing -> 24]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 18 { // w left, b right castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 19];
@@ -733,10 +816,14 @@
    [WhiteLeftCastle -> 23];
    [WhiteKing -> 23]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 19 { // w left, b right castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 18];
@@ -755,10 +842,14 @@
     [BlackRightCastle -> 26];
     [BlackKing -> 26]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 20 { // w right, b right castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 21];
@@ -777,10 +868,14 @@
    [WhiteRightCastle -> 23];
    [WhiteKing -> 23]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 21 { // w right, b right castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 20];
@@ -799,10 +894,14 @@
     [BlackRightCastle -> 28];
     [BlackKing -> 28]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 22 { // w no, b right castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 23];
@@ -820,10 +919,14 @@
    [WhiteQueen -> 23];
    [WhiteKing -> 23]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
+  PAYOFF :(CheckW()) - :(CheckB())
+ }
 }
 LOC 23 { // w no, b right castle
  PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9
   PAYOFF :(CheckW()) - :(CheckB())
   MOVES 
     [BlackPawnMove -> 22];
@@ -842,10 +945,14 @@
     [BlackRightCastle -> 30];
     [BlackKing -> 30]
  }
- PLAYER 1 { PAYOFF :(CheckB()) - :(CheckW()) }
+ PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
+  PAYOFF :(CheckB()) - :(CheckW())
+ }
 }
 LOC 24 { // w can, b no castle
  PLAYER 1 {
+  COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9
   PAYOFF :(CheckB()) - :(CheckW())
   MOVES 
    [WhitePawnMove -> 25];
@@ -865,10 +972,14 @@
    [WhiteRightCastle -> 31];
    [WhiteKing -> 31]
  }
- PLAYER 2 { PAYOFF :(CheckW()) - :(CheckB()) }
+ PLAYER 2 {
+  COND -1; -5; -3; -3; -9; 1;...
 
[truncated message content]