[Toss-devel-svn] SF.net SVN: toss:[1686] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1686] trunk/Toss
|
From: <luk...@us...> - 2012-03-09 12:06:07
|
Revision: 1686
http://toss.svn.sourceforge.net/toss/?rev=1686&view=rev
Author: lukaszkaiser
Date: 2012-03-09 12:05:53 +0000 (Fri, 09 Mar 2012)
Log Message:
-----------
Optimize JS interface, allow suggest from TossServer. Merge GameSelection into JsHandler and ReqHander into Server, clean up accordingly.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/Arena.mli
trunk/Toss/Arena/ArenaParser.mly
trunk/Toss/Client/JsHandler.ml
trunk/Toss/Client/Main.js
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormula.mli
trunk/Toss/Formula/BoolFormulaTest.ml
trunk/Toss/Formula/FormulaOpsTest.ml
trunk/Toss/Play/Heuristic.ml
trunk/Toss/Play/Heuristic.mli
trunk/Toss/Server/Server.ml
trunk/Toss/Server/Tests.ml
trunk/Toss/examples/Breakthrough.toss
trunk/Toss/examples/Checkers.toss
trunk/Toss/examples/Chess.toss
trunk/Toss/examples/Concurrent-Tic-Tac-Toe.toss
trunk/Toss/examples/Connect4.toss
trunk/Toss/examples/Gomoku.toss
trunk/Toss/examples/Gomoku19x19.toss
trunk/Toss/examples/Pawn-Whopping.toss
trunk/Toss/examples/Tic-Tac-Toe.toss
Removed Paths:
-------------
trunk/Toss/Client/Connect.js
trunk/Toss/Client/GameSelection.ml
trunk/Toss/Server/ReqHandler.ml
trunk/Toss/Server/ReqHandler.mli
trunk/Toss/Server/ReqHandlerTest.ml
trunk/Toss/examples/Breakthrough.tossstyle
trunk/Toss/examples/Checkers.tossstyle
trunk/Toss/examples/Chess.tossstyle
trunk/Toss/examples/Connect4.tossstyle
trunk/Toss/examples/Gomoku.tossstyle
trunk/Toss/examples/Pawn-Whopping.tossstyle
trunk/Toss/examples/Tic-Tac-Toe.tossstyle
trunk/Toss/examples/bishop_black.svg
trunk/Toss/examples/bishop_white.svg
trunk/Toss/examples/bluecircle.svg
trunk/Toss/examples/cross.svg
trunk/Toss/examples/greencircle.svg
trunk/Toss/examples/king_black.svg
trunk/Toss/examples/king_white.svg
trunk/Toss/examples/knight_black.svg
trunk/Toss/examples/knight_white.svg
trunk/Toss/examples/pawn_black.svg
trunk/Toss/examples/pawn_white.svg
trunk/Toss/examples/queen_black.svg
trunk/Toss/examples/queen_white.svg
trunk/Toss/examples/rook_black.svg
trunk/Toss/examples/rook_white.svg
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Arena/Arena.ml 2012-03-09 12:05:53 UTC (rev 1686)
@@ -549,100 +549,6 @@
with Diff_result expl -> false, expl
-(* ------------------ REQUESTS TO THE ARENA USED IN OPERATION --------------- *)
-
-(* Location of a structure: either arena or left or right-hand side of a rule *)
-type struct_loc = Struct | Left of string | Right of string
-
-(* Requests which we handle. *)
-type request =
- | SuggestLocMoves of int * int * int * string * int option *
- (string * Formula.real_expr) list array option * float option
-
-
-(* --------------------------- REQUEST HANDLER ------------------------------ *)
-
-(* Apply function [f] to named structure at location [loc] in [state].
- Include what [f] returns - changed named structure and string - and return.*)
-let apply_to_loc f loc (state_game, state) err_msg =
- match loc with
- Struct ->
- let (new_struc, msg) = f state.struc in
- ((state_game, { state with struc = new_struc }), msg)
- | Left rn -> (
- try
- let r = (List.assoc rn state_game.rules) in
- let signat = Structure.rel_signature state.struc in
- let defs = state_game.defined_rels in
- let new_r =
- ContinuousRule.apply_to_side true f signat defs r in
- let new_rules = Aux.replace_assoc rn new_r state_game.rules in
- (({state_game with rules=new_rules}, state), "")
- with Not_found ->
- ((state_game, state),
- "ERR [Not found] on left location of " ^ rn ^", " ^ err_msg)
- )
- | Right rn ->
- try
- let r = (List.assoc rn state_game.rules) in
- let signat = Structure.rel_signature state.struc in
- let defs = state_game.defined_rels in
- let new_r =
- ContinuousRule.apply_to_side false f signat defs r in
- let new_rules = Aux.replace_assoc rn new_r state_game.rules in
- (({state_game with rules=new_rules}, state), "")
- with Not_found ->
- ((state_game, state),
- "ERR [Not found] on right location of "^rn^", " ^ err_msg)
-
-(* Retrieve value of [f] from structure at location [loc] in [state]. *)
-let get_from_loc f loc (state_game, state) err_msg =
- match loc with
- Struct -> f state.struc
- | Left r_name -> (
- try
- let r = (List.assoc r_name state_game.rules) in
- (match r.ContinuousRule.discrete.DiscreteRule.struc_rule
- with
- | None -> raise Not_found
- | Some r -> f r.DiscreteRule.lhs_struc)
- with Not_found ->
- "ERR [Not found] getting from left location of " ^
- r_name ^ ", " ^ err_msg
- )
- | Right r_name ->
- try
- let r = (List.assoc r_name state_game.rules) in
- (match r.ContinuousRule.discrete.DiscreteRule.struc_rule
- with
- | None -> raise Not_found
- | Some r -> f r.DiscreteRule.rhs_struc)
- with Not_found ->
- "ERR [Not found] getting from right location of " ^
- r_name ^ ", " ^ err_msg
-
-(* Apply function [f] to named rule [r_name] in [state], insert and return. *)
-let apply_to_rule f r_name (state_game, state) err_msg =
- try
- let r = List.assoc r_name state_game.rules in
- let (nr, msg) = f r in
- let new_rules = Aux.replace_assoc r_name nr state_game.rules in
- (({state_game with rules=new_rules}, state), msg)
- with Not_found ->
- ((state_game, state),
- "ERR [Not found] applying to rule " ^ r_name ^ ": " ^ err_msg)
-
-(* Retrieve value of [f] from rule [r] in [state]. *)
-let get_from_rule f r state_game err =
- try f (List.assoc r state_game.rules)
- with Not_found ->
- "ERR [Not found] getting from rule " ^ r ^ ": " ^ err
-
-(* Print relational signature. *)
-let sig_str state =
- Structure.sig_str state.struc
-
-
let apply_rule_int (state_game, state) (r_name, mtch, t, p) =
(let try r = List.assoc r_name state_game.rules in (
match ContinuousRule.rewrite_single state.struc state.time mtch r t p with
Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Arena/Arena.mli 2012-03-09 12:05:53 UTC (rev 1686)
@@ -161,24 +161,6 @@
game * game_state -> game * game_state -> bool * string
-(** {2 Requests to the Arena used in Operation} *)
-
-(** Location of a structure: either arena or left or right-hand side of a rule *)
-type struct_loc = Struct | Left of string | Right of string
-
-(** Requests which we handle. *)
-type request =
- | SuggestLocMoves of int * int * int * string * int option *
- (string * Formula.real_expr) list array option * float option
- (** Suggested moves at loc, with timeout in so many seconds, for so
- much computational effort if possible before timeout, using given
- search method ("maximax", "alpha_beta", "alpha_beta_ord",
- "uct_random_playouts",
- "uct_greedy_playouts", "uct_maximax_playouts",
- "uct_no_playouts"), with optional horizon for playouts, with
- location-dependent heuristics, with advancement ratio for
- generating heuristics if they're not given *)
-
val apply_rule_int : game * game_state ->
string * (string * int) list * float * (string * float) list ->
(game * game_state) * string
Modified: trunk/Toss/Arena/ArenaParser.mly
===================================================================
--- trunk/Toss/Arena/ArenaParser.mly 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Arena/ArenaParser.mly 2012-03-09 12:05:53 UTC (rev 1686)
@@ -9,8 +9,7 @@
%}
-%start parse_game_defs parse_game_state parse_request
-%type <Arena.request> parse_request request
+%start parse_game_defs parse_game_state
%type <Arena.struct_loc> struct_location
%type <(string * int) list -> int * Arena.player_loc array> location
%type <Arena.definition> parse_game_defs
@@ -161,33 +160,9 @@
| RULE_SPEC id_int LEFT_SPEC { Arena.Left ($2) }
| RULE_SPEC id_int RIGHT_SPEC { Arena.Right ($2) }
-request:
- | EVAL_CMD LOC_MOD MOVES
- heur_adv_ratio=FLOAT loc=INT
- TIMEOUT_MOD timer=INT effort=INT algo=ID horizon=INT?
- {let heuristic = None in
- SuggestLocMoves (loc, timer, effort, algo, horizon, heuristic,
- Some heur_adv_ratio) }
- | EVAL_CMD LOC_MOD MOVES
- heuristic = delimited (
- OPENSQ,
- separated_nonempty_list(SEMICOLON,
- delimited(OPENCUR, separated_list (
- SEMICOLON, separated_pair (id_int, COLON, real_expr_err)
- ), CLOSECUR)), CLOSESQ)
- loc=INT
- TIMEOUT_MOD timer=INT effort=INT algo=ID horizon=INT?
- {let heur_adv_ratio = None in
- SuggestLocMoves (loc, timer, effort, algo, horizon,
- Some (Array.of_list heuristic), heur_adv_ratio) }
- | error
- { raise (Lexer.Parsing_error "Syntax error in Server request.") }
-
parse_game_defs:
game_defs EOF { $1 };
parse_game_state:
game_state EOF { $1 };
-parse_request:
- request EOF { $1 };
Deleted: trunk/Toss/Client/Connect.js
===================================================================
--- trunk/Toss/Client/Connect.js 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Client/Connect.js 2012-03-09 12:05:53 UTC (rev 1686)
@@ -1,166 +0,0 @@
-// JavaScript Toss Module -- Connect (basic Toss Server connection routines)
-
-var ASYNC_ALL_REQ_PENDING = 0;
-var ASYNC_CMD_REQ_PENDING = {};
-
-
-// Strip [c1] and [c2] from beginning and end of [str].
-function strip (c1, c2, str) {
- if (str.length == 0) return (str);
- var i = 0; var j = 0;
- for (i = 0; i < str.length; i++) {
- if (str.charAt(i) != c1 && str.charAt(i) != c2) break;
- }
- for (j = str.length - 1; j > -1; j--) {
- if (str.charAt(j) != c1 && str.charAt(j) != c2) break;
- }
- if (i > j) { return ("") };
- return (str.substring(i, j+1));
-}
-
-// Convert a string [str] representing python list to array and return it.
-// WARNING: we use [sep] as separator, it must not occur in list elements!
-function parse_list (sep, str_in) {
- var res_arr = [];
- var str = strip(' ', '\n', str_in);
- res_arr = strip('[', ']', str).split(sep);
- if (res_arr.length == 1 && res_arr[0] == "") { return ([]); }
- for (i = 0; i < res_arr.length; i++) {
- res_arr[i] = strip (' ', '\'', res_arr[i])
- }
- return (res_arr);
-}
-
-function Connect () {
- // Send [msg] to server and return response text.
- var sync_server_msg = function (msg) {
- var xml_request = new XMLHttpRequest ();
- xml_request.open ('POST', 'Handler', false);
- xml_request.setRequestHeader
- ('Content-Type', 'application/x-www-form-urlencoded; charset=UTF-8');
- xml_request.send (msg);
- resp = xml_request.responseText;
- if (resp.indexOf ("MOD_PYTHON ERROR") > -1) {
- alert (resp.substring(resp.indexOf("Traceback")));
- return ("");
- }
- return (resp)
- }
-
- this.s = sync_server_msg;//Just a copy of above for public usage
-
- // Send [msg] to server asynchronously, ignore response text.
- var async_server_msg = function (msg, count, f) {
- var xml_request = new XMLHttpRequest ();
- xml_request.open ('POST', 'Handler', true);
- xml_request.setRequestHeader (
- 'Content-Type', 'application/x-www-form-urlencoded; charset=UTF-8');
- if (count) {
- xml_request.onreadystatechange = function () {
- if (xml_request.readyState == 4) {
- ASYNC_ALL_REQ_PENDING -= 1;
- resp = xml_request.responseText;
- if (resp.indexOf ("MOD_PYTHON ERROR") > -1) {
- alert (resp.substring(resp.indexOf("Traceback")));
- } else { f(resp) };
- }
- }
- } else {
- xml_request.onreadystatechange = function () {
- if (xml_request.readyState == 4) {
- resp = xml_request.responseText;
- if (resp.indexOf ("MOD_PYTHON ERROR") > -1) {
- alert (resp.substring(resp.indexOf("Traceback")));
- } else { f(resp) };
- }
- }
- };
- if (count) { ASYNC_ALL_REQ_PENDING += 1; }
- xml_request.send (msg);
- }
-
- // Send [msg] to server attaching prefix '[cmd]#' and return response text.
- var srv = function (cmd, msg) {
- return (sync_server_msg (cmd + '#' + msg));
- }
-
- // Send [msg] to server attaching prefix '[cmd]#' async., ignore response.
- var async_srv_ignore = function (cmd, msg) {
- async_server_msg (cmd + '#' + msg, false, function(x) { });
- }
-
- // Send [msg] to server attaching prefix '[cmd]#' async., run f on return.
- var async_srv = function (cmd, msg, f) {
- if (ASYNC_CMD_REQ_PENDING[cmd]) {
- ASYNC_CMD_REQ_PENDING[cmd] += 1;
- } else { ASYNC_CMD_REQ_PENDING[cmd] = 1; };
- var fm = function (m) {
- ASYNC_CMD_REQ_PENDING[cmd] -= 1;
- f ();
- };
- async_server_msg (cmd + '#' + msg, true, f);
- }
-
- this.get_name = function (uname) { return (srv ("GET_NAME", uname)); }
-
- this.list_plays = function (game, uname) {
- if (uname == "guest") { return ("[]"); }
- return (srv ("LIST_PLAYS", game + ", " + uname));
- }
-
- this.open_db = function (pid) { return (srv ("OPEN_DB", pid)); }
- this.prev_move = function (pid, mv) {
- return (srv ("PREV_MOVE", pid + ", " + mv));
- }
- this.new_play = function (g, un, opp) {
- return (srv ("NEW_PLAY", g + ", " + un + ", " + opp));
- }
- this.make_move = function (move_s, pid, cont) {
- async_srv("MOVE_PLAY", move_s + ', ' + pid, cont);
- }
- this.suggest = function (player, time, pid, cont) {
- async_srv("SUGGEST", player + ', ' + time + ', ' + pid, cont);
- }
-
- this.friends = function () { return (srv ("LIST_FRIENDS", "user")); }
- this.search_users = function (txt) { return (srv ("SEARCHUSR", txt)); }
- this.plays = function () { return (srv("USERPLAYS", "user")); }
- this.username = function () { return (srv("USERNAME", "user")); }
- this.addopp = function (opp) { return (srv("ADDOPP", opp)); }
-
- this.name = function (un) { return (srv("GET_NAME", un)); }
- this.surname = function (un) { return (srv("GET_SURNAME", un)); }
- this.email = function (un) { return (srv("GET_MAIL", un)); }
-
- this.login = function (un, chk, cpwd) {
- return (srv ("LOGIN", un +"$"+ chk +"$"+ cpwd));
- }
- this.logout = function () { return (srv("LOGOUT", "user")); }
- this.register = function (data, cpwd) {
- return (srv ("REGISTER", data + "$" + cpwd));
- }
- this.invite = function (mail) { return (srv("INVITE", mail)); }
- this.forgotpwd = function (mail) { return (srv("FORGOTPWD", mail)); }
- this.change_pwd = function (un, pwd) {
- var resp = srv("CHANGEPWD", pwd);
- if (resp == "OK") {
- this.logout ();
- this.login (un, true, pwd);
- return ("Password changed successfully");
- } else { return (resp); }
- }
- this.change_data = function (name, surname, email) {
- return (srv ("CHANGEUSR", name +"$"+ surname +"$"+ email));
- }
- this.learn_game = function (game, plays) {
- return (srv ("LEARNGAME", game + ", " + plays));
- }
- this.get_game = function (game) { return (srv("GETGAME", game)); }
- this.set_game = function (game, toss) {
- return (srv("SETGAME", game + " $_$ " + toss));
- }
-
- return (this);
-}
-
-var CONN = new Connect ();
Deleted: trunk/Toss/Client/GameSelection.ml
===================================================================
--- trunk/Toss/Client/GameSelection.ml 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Client/GameSelection.ml 2012-03-09 12:05:53 UTC (rev 1686)
@@ -1,1065 +0,0 @@
-(* In-source definitions of several games, loading games from strings. *)
-
-type game_state_data = {
- heuristic : Formula.real_expr array array; (** heuristic *)
- game_state : (Arena.game * Arena.game_state); (** game and state *)
- playclock : int; (** playclock *)
- game_str : string; (** game representation *)
-}
-
-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
- res
- with Not_found ->
- Heuristic.default_heuristic ~struc:state.Arena.struc ?advr game
-
-let compile_game_data game_name game_str =
- let (game, game_state as game_with_state) =
- ArenaParser.parse_game_state Lexer.lex (Lexing.from_string game_str) in
- let adv_ratio =
- try Some (float_of_string (List.assoc "adv_ratio" game.Arena.data))
- with Not_found -> None in
- let heuristic = compute_heuristic adv_ratio game_with_state in
- game_name,
- {heuristic = heuristic;
- game_state = game_with_state;
- playclock = 30; (* game clock from where? *)
- game_str = game_str;
- }
-
-
-let chess_str = ("
-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)
-SET Sum (x | wBeats(x) : 1 + :(b(x)) + 3 * :(bK(x)))
-SET Sum (x | bBeats(x) : 1 + :(w(x)) + 3 * :(wK(x)))
-REL w(x) = wP(x) or wR(x) or wN(x) or wB(x) or wQ(x) or wK(x)
-REL b(x) = bP(x) or bR(x) or bN(x) or bB(x) or bQ(x) or bK(x)
-REL DoubleC(x, y) = ex z ((C(x, z) and C(z, y)) or (C(y, z) and C(z, x)))
-REL DoubleR(x, y) = ex z ((R(x, z) and R(z, y)) or (R(y, z) and R(z, x)))
-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 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 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)
-REL 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)
-REL wPBeats (x) = ex y (wP(y) and ex z ((R(y, z) or R(z, y)) and C(z, x)))
-REL bPBeats (x) = ex y (bP(y) and ex z ((R(y, z) or R(z, y)) and C(x, z)))
-REL wDiagBeats (x) = ex y ((wQ(y) or wB(y)) and Diag(y, x))
-REL bDiagBeats (x) = ex y ((bQ(y) or bB(y)) and Diag(y, x))
-REL wLineBeats (x) = ex y ((wQ(y) or wR(y)) and Line(y, x))
-REL bLineBeats (x) = ex y ((bQ(y) or bR(y)) and Line(y, x))
-REL wFigBeats(x) = wDiagBeats(x) or wLineBeats(x) or ex y(wN(y) and Knight(y,x))
-REL bFigBeats(x) = bDiagBeats(x) or bLineBeats(x) or ex y(bN(y) and Knight(y,x))
-REL wBeats(x) = wFigBeats(x) or wPBeats(x) or ex y (wK(y) and Near(y, x))
-REL bBeats(x) = bFigBeats(x) or bPBeats(x) or ex y (bK(y) and Near(y, x))
-REL CheckW() = ex x (wK(x) and bBeats(x))
-REL CheckB() = ex x (bK(x) and wBeats(x))
-RULE WhitePawnMove:
- [ | | ] \"
- ...
- ...
-
- wP
-\" -> [ | | ] \"
- ...
- wP
-
- .
-\" emb w, b pre not IsEight(a2) post not CheckW()
-RULE BlackPawnMove:
- [ | | ] \"
- ...
- bP.
-
- .
-\" -> [ | | ] \"
- ...
- ...
-
- bP
-\" emb w, b pre not IsFirst(a1) post not CheckB()
-RULE WhitePawnMoveDbl:
- [ | | ] \"
-
- .
- ...
- ...
-
- wP
-\" -> [ | | ] \"
- ...
- wP
-
- .
- ...
- ...
-\" emb w, b pre IsSecond(a1) post not CheckW()
-RULE BlackPawnMoveDbl:
- [ | | ] \"
- ...
- bP.
-
- .
- ...
- ...
-\" -> [ | | ] \"
-
-
- ...
- ...
-
- bP
-\" emb w, b pre IsSeventh(a3) post not CheckB()
-RULE WhitePawnBeat:
- [ a, b | wP { a }; b { b } | - ]
- ->
- [ a, b | wP { b } | - ]
- emb w, b
- pre not IsEight(b) and ex z (C(a, z) and (R(z, b) or R(b, z)))
- post not CheckW()
-RULE WhitePawnBeatPromote:
- [ a, b | wP { a }; b { b } | - ]
- ->
- [ a, b | wQ { b } | - ]
- emb w, b
- pre IsEight(b) and ex z (C(a, z) and (R(z, b) or R(b, z)))
- post not CheckW()
-RULE WhitePawnBeatRDbl:
- [ | | ] \"
- ...
- ?..-bP
- ...
- ? ...
- ...
- wP.bP
-\" -> [ | | ] \"
- ...
- ?...
- ...
- ? wP.
- ...
- ....
-\" emb w, b post not CheckW()
-RULE WhitePawnBeatLDbl:
- [ | | ] \"
- ...
- -bP?
- ...
- . ?..
- ...
- bP.wP
-\" -> [ | | ] \"
- ...
- ...?
- ...
- wP ?..
- ...
- ....
-\" emb w, b post not CheckW()
-RULE BlackPawnBeat:
- [ a, b | bP { a }; w { b } | - ]
- ->
- [ a, b | bP { b } | - ]
- emb w, b
- pre not IsFirst(b) and ex z (C(z, a) and (R(z, b) or R(b, z)))
- post not CheckB()
-RULE BlackPawnBeatPromote:
- [ a, b | bP { a }; w { b } | - ]
- ->
- [ a, b | bQ { b } | - ]
- emb w, b
- pre IsFirst(b) and ex z (C(z, a) and (R(z, b) or R(b, z)))
- post not CheckB()
-RULE BlackPawnBeatRDbl:
- [ | | ] \"
- ...
- bP.wP
- ...
- ? ...
- ...
- ?..-wP
-\" -> [ | | ] \"
- ...
- ....
- ...
- ? bP.
- ...
- ?...
-\" emb w, b post not CheckB()
-RULE BlackPawnBeatLDbl:
- [ | | ] \"
- ...
- wP.bP
- ...
- . ?..
- ...
- -wP?
-\" -> [ | | ] \"
- ...
- ....
- ...
- bP ?..
- ...
- ...?
-\" emb w, b post not CheckB()
-RULE WhitePawnPromote:
- [ | | ] \"
- ...
- ...
-
- wP
-\" -> [ | | ] \"
- ...
- wQ.
-
- .
-\" emb w, b pre IsEight(a2) post not CheckW()
-RULE BlackPawnPromote:
- [ | | ] \"
- ...
- bP.
-
- .
-\" -> [ | | ] \"
- ...
- ...
-
- bQ
-\" emb w, b pre IsFirst(a1) post not CheckB()
-RULE WhiteKnight:
- [ a, b | wN { a }; _opt_b { b } | - ]
- ->
- [ a, b | wN { b } | - ]
- emb w, b pre Knight(a, b) post not CheckW()
-RULE BlackKnight:
- [ a, b | bN { a }; _opt_w { b } | - ]
- ->
- [ a, b | bN { b } | - ]
- emb w, b pre Knight(a, b) post not CheckB()
-RULE WhiteBishop:
- [ a, b | wB { a }; _opt_b { b } | - ]
- ->
- [ a, b | wB { b } | - ]
- emb w, b pre Diag(a, b) post not CheckW()
-RULE BlackBishop:
- [ a, b | bB { a }; _opt_w { b } | - ]
- ->
- [ a, b | bB { b } | - ]
- emb w, b pre Diag(a, b) post not CheckB()
-RULE WhiteRook:
- [ a, b | wR { a }; _opt_b { b } | - ]
- ->
- [ a, b | wR { b } | - ]
- emb w, b pre not IsA1(a) and not IsH1(a) and Line(a, b) post not CheckW()
-RULE WhiteRookA1:
- [ a, b | wR { a }; _opt_b { b } | - ]
- ->
- [ a, b | wR { b } | - ]
- emb w, b pre IsA1(a) and Line(a, b) post not CheckW()
-RULE WhiteRookH1:
- [ a, b | wR { a }; _opt_b { b } | - ]
- ->
- [ a, b | wR { b } | - ]
- emb w, b pre IsH1(a) and Line(a, b) post not CheckW()
-RULE BlackRook:
- [ a, b | bR { a }; _opt_w { b } | - ]
- ->
- [ a, b | bR { b } | - ]
- emb w, b pre not IsA8(a) and not IsH8(a) and Line(a, b) post not CheckB()
-RULE BlackRookA8:
- [ a, b | bR { a }; _opt_w { b } | - ]
- ->
- [ a, b | bR { b } | - ]
- emb w, b pre IsA8(a) and Line(a, b) post not CheckB()
-RULE BlackRookH8:
- [ a, b | bR { a }; _opt_w { b } | - ]
- ->
- [ a, b | bR { b } | - ]
- emb w, b pre IsH8(a) and Line(a, b) post not CheckB()
-RULE WhiteQueen:
- [ a, b | wQ { a }; _opt_b { b } | - ]
- ->
- [ a, b | wQ { b } | - ]
- emb w, b pre (Line(a, b) or Diag(a, b)) post not CheckW()
-RULE BlackQueen:
- [ a, b | bQ { a }; _opt_w { b } | - ]
- ->
- [ a, b | bQ { b } | - ]
- emb w, b pre (Line(a, b) or Diag(a, b)) post not CheckB()
-RULE WhiteKing:
- [ a, b | wK { a }; _opt_b { b } | - ]
- ->
- [ a, b | wK { b } | - ]
- emb w, b pre Near(a, b) post not CheckW()
-RULE BlackKing:
- [ a, b | bK { a }; _opt_w { b } | - ]
- ->
- [ a, b | bK { b } | - ]
- emb w, b pre Near(a, b) post not CheckB()
-RULE WhiteLeftCastle:
- [ | | ] \"
- ... ... ...
- wR. ... wK.
-\" -> [ | | ] \"
- ... ... ...
- ... wK.wR ...
-\" emb w,b pre not(bBeats(c1) or bBeats(d1) or bBeats(e1)) and before
- not WhiteRookA1, not WhiteKing, not WhiteLeftCastle, not WhiteRightCastle
-RULE WhiteRightCastle:
- [ | | ] \"
- ... ...
- wK. ...wR
-\" -> [ | | ] \"
- ... ...
- ...wR wK.
-\" emb w,b pre not (bBeats(a1) or bBeats(b1) or bBeats(c1)) and before
- not WhiteRookH1, not WhiteKing, not WhiteLeftCastle, not WhiteRightCastle
-RULE BlackLeftCastle:
- [ | | ] \"
- ... ... ...
- bR. ... bK.
-\" -> [ | | ] \"
- ... ... ...
- ... bK.bR ...
-\" emb w,b pre not(wBeats(c1) or wBeats(d1) or wBeats(e1)) and before
- not BlackRookA8, not BlackKing, not BlackLeftCastle, not BlackRightCastle
-RULE BlackRightCastle:
- [ | | ] \"
- ... ...
- bK. ...bR
-\" -> [ | | ] \"
- ... ...
- ...bR bK.
-\" emb w,b pre not (wBeats(a1) or wBeats(b1) or wBeats(c1)) and before
- not BlackRookH8, not BlackKing, not BlackLeftCastle, not BlackRightCastle
-LOC 0 {
- PLAYER 1 {
- COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9; 0.05; -0.05
- PAYOFF :(CheckB()) - :(CheckW())
- MOVES
- [WhitePawnMove -> 1];
- [WhitePawnMoveDbl -> 1];
- [WhitePawnBeat -> 1];
- [WhitePawnBeatPromote -> 1];
- [WhitePawnBeatLDbl -> 1];
- [WhitePawnBeatRDbl -> 1];
- [WhitePawnPromote -> 1];
- [WhiteKnight -> 1];
- [WhiteBishop -> 1];
- [WhiteRook -> 1];
- [WhiteRookA1 -> 1];
- [WhiteRookH1 -> 1];
- [WhiteQueen -> 1];
- [WhiteLeftCastle -> 1];
- [WhiteRightCastle -> 1];
- [WhiteKing -> 1]
- }
- PLAYER 2 {
- COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9; -0.05; 0.05
- PAYOFF :(CheckW()) - :(CheckB())
- }
-}
-LOC 1 {
- PLAYER 2 {
- COND -1; -5; -3; -3; -9; 1; 5; 3; 3; 9; -0.05; 0.05
- PAYOFF :(CheckW()) - :(CheckB())
- MOVES
- [BlackPawnMove -> 0];
- [BlackPawnMoveDbl -> 0];
- [BlackPawnBeat -> 0];
- [BlackPawnBeatPromote -> 0];
- [BlackPawnBeatLDbl -> 0];
- [BlackPawnBeatRDbl -> 0];
- [BlackPawnPromote -> 0];
- [BlackKnight -> 0];
- [BlackBishop -> 0];
- [BlackRook -> 0];
- [BlackRookA8 -> 0];
- [BlackRookH8 -> 0];
- [BlackQueen -> 0];
- [BlackLeftCastle -> 0];
- [BlackRightCastle -> 0];
- [BlackKing -> 0]
- }
- PLAYER 1 {
- COND 1; 5; 3; 3; 9; -1; -5; -3; -3; -9; 0.05; -0.05
- PAYOFF :(CheckB()) - :(CheckW())
- }
-}
-MODEL [ | | ] \"
- ... ... ... ...
- 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
-\" with
-D1(x, y) = ex z ( (R(x, z) and C(z, y)) or (R(y, z) and C(z, x)) ) ;
-D2(x, y) = ex z ( (R(x, z) and C(y, z)) or (R(y, z) and C(x, z)) ) ;
-IsFirst(x) = not ex z C(z, x) ;
-IsSecond(x) = ex y (C(y, x) and IsFirst(y)) ;
-IsEight(x) = not ex z C(x, z) ;
-IsSeventh(x) = ex y (C(x, y) and IsEight(y)) ;
-IsA1(x) = not ex z R(z, x) and IsFirst(x) ;
-IsH1(x) = not ex z R(x, z) and IsFirst(x) ;
-IsA8(x) = not ex z R(z, x) and IsEight(x) ;
-IsH8(x) = not ex z R(x, z) and IsEight(x)
-")
-
-let connect4_str = ("PLAYERS 1, 2
-DATA r1: circle, r2: line, adv_ratio: 4, depth: 6
-REL Row4 (x, y, z, v) = R(x, y) and R(y, z) and R(z, v)
-REL Col4 (x, y, z, v) = C(x, y) and C(y, z) and C(z, v)
-REL DiagA4 (x, y, z, v) = DiagA(x, y) and DiagA(y, z) and DiagA(z, v)
-REL DiagB4 (x, y, z, v) = DiagB(x, y) and DiagB(y, z) and DiagB(z, v)
-REL Conn4 (x, y, z, v) =
- Row4(x,y,z,v) or Col4(x,y,z,v) or DiagA4(x,y,z,v) or DiagB4(x,y,z,v)
-REL WinQ() =
- ex x,y,z,v (Q(x) and Q(y) and Q(z) and Q(v) and Conn4(x, y, z, v))
-REL WinP() =
- ex x,y,z,v (P(x) and P(y) and P(z) and P(v) and Conn4(x, y, z, v))
-REL EmptyUnder (x) = ex y (C(y, x) and not P(y) and not Q(y))
-RULE Cross:
- [a | P:1 {} | - ] -> [a | P (a) | - ] emb Q, P
- pre not EmptyUnder (a) and not WinQ()
-RULE Circle:
- [a | Q:1 {} | - ] -> [a | Q (a) | - ] emb Q, P
- pre not EmptyUnder (a) and not WinP()
-LOC 0 {
- PLAYER 1 {
- PAYOFF :(WinP()) - :(WinQ())
- MOVES [Cross -> 1]
- }
- PLAYER 2 {
- PAYOFF :(WinQ()) - :(WinP())
- }
-}
-LOC 1 {
- PLAYER 1 {
- PAYOFF :(WinP()) - :(WinQ())
- }
- PLAYER 2 {
- PAYOFF :(WinQ()) - :(WinP())
- MOVES [Circle -> 0]
- }
-}
-MODEL [ | P:1 {}; Q:1 {} | ] \"
- ... ... ...
- ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ...
- ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ...
- ... ... ...
- ... ... ... ...
- ... ... ... ...
-\" with DiagA (x, y) = ex u (R(x, u) and C(u, y)) ;
- DiagB (x, y) = ex u (R(x, u) and C(y, u))
-")
-
-let pawn_whopping_str = ("
-PLAYERS 1, 2
-DATA depth: 4, adv_ratio: 2
-REL DiagW (x, y) = ex z (C(x, z) and (R(y, z) or R(z, y)))
-REL DiagB (x, y) = ex z (C(z, x) and (R(y, z) or R(z, y)))
-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)
-REL IsSeventh(x) = ex y (C(x, y) and IsEight(y))
-REL WhiteEnds() = (ex x (wP(x) and not ex y C(x, y))) or (not ex z bP(z))
-REL BlackEnds() = (ex x (bP(x) and not ex y C(y, x))) or (not ex z wP(z))
-RULE WhiteBeat:
- [ a, b | wP { a }; bP { b } | - ] -> [ a, b | wP { b } | - ] emb wP, bP
- pre DiagW(a, b) and not BlackEnds()
-RULE WhiteMove:
- [ | bP:1 {}; R:2 {} | ] \"
-
- .
-
- wP
-\" -> [ | bP:1 {}; R:2 {} | ] \"
-
- wP
-
- .
-\" emb wP, bP pre not BlackEnds()
-RULE WhiteMoveTwo:
- [ | bP:1 {}; R:2 {} | ] \"
-
- .
-
- .
-
- wP
-\" -> [ | bP:1 {}; R:2 {} | ] \"
-
- wP
-
- .
-
- .
-\" emb wP, bP pre IsSecond(a1) and not BlackEnds()
-RULE WhiteRightPassant:
- [ | | ] \"
- ...
- ?..-bP
- ...
- ? ...
- ...
- wP.bP
-\" -> [ | | ] \"
- ...
- ?...
- ...
- ? wP.
- ...
- ....
-\" emb wP, bP pre not BlackEnds()
-RULE WhiteLeftPassant:
- [ | | ] \"
- ...
- -bP?
- ...
- . ?..
- ...
- bP.wP
-\" -> [ | | ] \"
- ...
- ...?
- ...
- wP ?..
- ...
- ....
-\" emb wP, bP pre not BlackEnds()
-RULE BlackBeat:
- [ a, b | bP { a }; wP { b } | - ] -> [ a, b | bP { b } | - ] emb wP, bP
- pre DiagB(a, b) and not WhiteEnds()
-RULE BlackMove:
- [ | R:2 {}; wP:1 {} | ] \"
-
- bP
-
- .
-\" -> [ | R:2 {}; wP:1 {} | ] \"
-
- .
-
- bP
-\" emb wP, bP pre not WhiteEnds()
-RULE BlackMoveTwo:
- [ | R:2 {}; wP:1 {} | ] \"
-
- bP
-
- .
-
- .
-\" -> [ | R:2 {}; wP:1 {} | ] \"
-
- .
-
- .
-
- bP
-\" emb wP, bP pre IsSeventh(a3) and not WhiteEnds()
-RULE BlackRightPassant:
- [ | | ] \"
- ...
- bP.wP
- ...
- ? ...
- ...
- ?..-wP
-\" -> [ | | ] \"
- ...
- ....
- ...
- ? bP.
- ...
- ?...
-\" emb wP, bP pre not WhiteEnds()
-RULE BlackLeftPassant:
- [ | | ] \"
- ...
- wP.bP
- ...
- . ?..
- ...
- -wP?
-\" -> [ | | ] \"
- ...
- ....
- ...
- bP ?..
- ...
- ...?
-\" emb wP, bP pre not WhiteEnds()
-LOC 0 {
- PLAYER 1 {
- PAYOFF :(WhiteEnds()) - :(BlackEnds())
- MOVES
- [WhiteBeat -> 1]; [WhiteMove -> 1]; [WhiteMoveTwo -> 1];
- [WhiteRightPassant -> 1]; [WhiteLeftPassant -> 1]
- }
- PLAYER 2 { PAYOFF :(BlackEnds()) - :(WhiteEnds()) }
-}
-LOC 1 {
- PLAYER 1 { PAYOFF :(WhiteEnds()) - :(BlackEnds()) }
- PLAYER 2 {
- PAYOFF :(BlackEnds()) - :(WhiteEnds())
- MOVES
- [BlackBeat -> 0]; [BlackMove -> 0]; [BlackMoveTwo -> 0];
- [BlackRightPassant -> 0]; [BlackLeftPassant -> 0]
- }
-}
-MODEL [ | | ] \"
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- bP.bP bP.bP bP.bP bP.bP
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- wP wP.wP wP.wP wP.wP wP.
- ... ... ... ...
- ... ... ... ...
-\"
-")
-
-let breakthrough_str = ("
-PLAYERS 1, 2
-DATA depth: 2, adv_ratio: 2
-REL DiagW (x, y) = ex z (C(x, z) and (R(y, z) or R(z, y)))
-REL DiagB (x, y) = ex z (C(z, x) and (R(y, z) or R(z, y)))
-RULE WhiteDiag:
- [ a, b | W { a }; _opt_B { b } | - ]
- ->
- [ a, b | W { b } | - ]
- emb W, B pre DiagW(a, b) and not ex x (B(x) and not ex y C(y, x))
-RULE WhiteStraight:
- [ | B:1 {}; R:2 {} | ] \"
-
- .
-
- W
-\" -> [ | B:1 {}; R:2 {} |
- ] \"
-
- W
-
- .
-\" emb W, B pre not ex x (B(x) and not ex y C(y, x))
-RULE BlackDiag:
- [ a, b | B { a }; _opt_W { b } | - ]
- ->
- [ a, b | B { b } | - ]
- emb W, B pre DiagB(a, b) and not ex x (W(x) and not ex y C(x, y))
-RULE BlackStraight:
- [ | R:2 {}; W:1 {} | ] \"
-
- B
-
- .
-\" -> [ | R:2 {}; W:1 {} |
- ] \"
-
- .
-
- B
-\" emb W, B pre not ex x (W(x) and not ex y C(x, y))
-LOC 0 {
- PLAYER 1 {
- PAYOFF
- :(ex x (W(x) and not ex y C(x, y))) - :(ex x (B(x) and not ex y C(y, x)))
- MOVES
- [WhiteDiag -> 1]; [WhiteStraight -> 1]
- }
- PLAYER 2 {
- PAYOFF
- :(ex x (B(x) and not ex y C(y, x))) - :(ex x (W(x) and not ex y C(x, y)))
- }
-}
-LOC 1 {
- PLAYER 1 {
- PAYOFF
- :(ex x (W(x) and not ex y C(x, y))) - :(ex x (B(x) and not ex y C(y, x)))
- }
- PLAYER 2 {
- PAYOFF
- :(ex x (B(x) and not ex y C(y, x))) - :(ex x (W(x) and not ex y C(x, y)))
- MOVES
- [BlackDiag -> 0]; [BlackStraight -> 0]
- }
-}
-MODEL [ | | ] \"
- ... ... ... ...
- B B..B B..B B..B B..
- ... ... ... ...
- B..B B..B B..B B..B
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- W W..W W..W W..W W..
- ... ... ... ...
- W..W W..W W..W W..W
-\"
-")
-
-
-let checkers_str = ("
-PLAYERS 1, 2
-DATA depth: 4, adv_ratio: 2
-REL w(x) = W(x) or Wq(x)
-REL b(x) = B(x) or Bq(x)
-REL AnyDiag (x, y) =
- DiagWa (x, y) or DiagWb (x, y) or DiagBa (x, y) or DiagBb (x, y)
-REL Diag2 (x, y, z) = DiagW2 (x, y, z) or DiagB2 (x, y, z)
-REL BeatsW (x, y) = ex z (b(z) and not b(y) and not w(y) and DiagW2 (x, z, y))
-REL BeatsWX (x, y) = ex z (b(z) and not b(y) and not w(y) and Diag2 (x, z, y))
-REL BeatsB (x, y) = ex z (w(z) and not b(y) and not w(y) and DiagB2 (x, z, y))
-REL BeatsBX (x, y) = ex z (w(z) and not b(y) and not w(y) and Diag2 (x, z, y))
-REL BJumps() = ex x, y ((B(x) and BeatsB (x, y)) or (Bq(x) and BeatsBX (x, y)))
-REL WJumps() = ex x, y ((W(x) and BeatsW (x, y)) or (Wq(x) and BeatsWX (x, y)))
-RULE RedMove:
- [ a, b | W { a } | - ] -> [ a, b | W { b } | - ] emb w, b
- pre (not IsEight(b)) and (DiagWa(a, b) or DiagWb(a, b)) and not WJumps()
-RULE WhiteMove:
- [ a, b | B { a } | - ] -> [ a, b | B { b } | - ] emb w, b
- pre (not IsFirst(b)) and (DiagBa(a, b) or DiagBb(a, b)) and not BJumps()
-RULE RedPromote:
- [ a, b | W { a } | - ] -> [ a, b | Wq { b } | - ] emb w, b
- pre (IsEight(b)) and (DiagWa(a, b) or DiagWb(a, b)) and not WJumps()
-RULE WhitePromote:
- [ a, b | B { a } | - ] -> [ a, b | Bq { b } | - ] emb w, b
- pre (IsFirst(b)) and (DiagBa(a, b) or DiagBb(a, b)) and not BJumps()
-RULE RedQMove:
- [ a, b | Wq { a } | - ] -> [ a, b | Wq { b } | - ] emb w, b
- pre AnyDiag (a, b) and not WJumps()
-RULE WhiteQMove:
- [ a, b | Bq { a } | - ] -> [ a, b | Bq { b } | - ] emb w, b
- pre AnyDiag (a, b) and not BJumps()
-RULE RedBeat:
- [ a, b, c | W { a }; b { b } | - ] -> [ a, b, c | W { c } | - ] emb w, b
- pre DiagW2 (a, b, c) and not IsEight(c)
- post not ex x, y (_new_W(x) and BeatsWX (x, y))
-RULE WhiteBeat:
- [ a, b, c | B { a }; w { b } | - ] -> [ a, b, c | B { c } | - ] emb w, b
- pre DiagB2 (a, b, c) and not IsFirst(c)
- post not ex x, y (_new_B(x) and BeatsBX (x, y))
-RULE RedBeatBoth:
- [ a, b, c | W { a }; b { b } | - ] -> [ a, b, c | W { c } | - ] emb w, b
- pre _new_W(a) and Diag2 (a, b, c) and not IsEight(c)
- post not ex x, y (_new_W(x) and BeatsWX (x, y))
-RULE WhiteBeatBoth:
- [ a, b, c | B { a }; w { b } | - ] -> [ a, b, c | B { c } | - ] emb w, b
- pre _new_B(a) and Diag2 (a, b, c) and not IsFirst(c)
- post not ex x, y (_new_B(x) and BeatsBX (x, y))
-RULE RedBeatPromote:
- [ a, b, c | W { a }; b { b } | - ] -> [ a, b, c | Wq { c } | - ] emb w, b
- pre DiagW2 (a, b, c) and IsEight(c)
-RULE WhiteBeatPromote:
- [ a, b, c | B { a }; w { b } | - ] -> [ a, b, c | Bq { c } | - ] emb w, b
- pre DiagB2 (a, b, c) and IsFirst(c)
-RULE RedBeatCont:
- [ a, b, c | W { a }; b { b } | - ] -> [ a, b, c | W { c } | - ] emb w, b
- pre DiagW2 (a, b, c) and not IsEight(c)
- post ex x, y (_new_W(x) and BeatsWX (x, y))
-RULE WhiteBeatCont:
- [ a, b, c | B { a }; w { b } | - ] -> [ a, b, c | B { c } | - ] emb w, b
- pre DiagB2 (a, b, c) and not IsFirst(c)
- post ex x, y (_new_B(x) and BeatsBX (x, y))
-RULE RedBeatBothCont:
- [ a, b, c | W { a }; b { b } | - ] -> [ a, b, c | W { c } | - ] emb w, b
- pre _new_W(a) and Diag2 (a, b, c) and not IsEight(c)
- post ex x, y (_new_W(x) and BeatsWX (x, y))
-RULE WhiteBeatBothCont:
- [ a, b, c | B { a }; w { b } | - ] -> [ a, b, c | B { c } | - ] emb w, b
- pre _new_B(a) and Diag2 (a, b, c) and not IsFirst(c)
- post ex x, y (_new_B(x) and BeatsBX (x, y))
-RULE RedQBeat:
- [ a, b, c | Wq { a }; b { b } | - ] -> [ a, b, c | Wq { c } | - ] emb w, b
- pre Diag2 (a, b, c)
-RULE WhiteQBeat:
- [ a, b, c | Bq { a }; w { b } | - ] -> [ a, b, c | Bq { c } | - ] emb w, b
- pre Diag2 (a, b, c)
-LOC 0 {
- PLAYER 1 {
- PAYOFF :(ex x w(x)) - :(ex x b(x))
- MOVES
- [RedMove -> 1]; [RedPromote -> 1]; [RedQMove -> 1];
- [RedBeat -> 1]; [RedBeatPromote -> 1]; [RedQBeat -> 1];
- [RedBeatCont -> 2]
- }
- PLAYER 2 {
- PAYOFF :(ex x b(x)) - :(ex x w(x))
- }
-}
-LOC 1 {
- PLAYER 1 {
- PAYOFF :(ex x w(x)) - :(ex x b(x))
- }
- PLAYER 2 {
- PAYOFF :(ex x b(x)) - :(ex x w(x))
- MOVES
- [WhiteMove -> 0]; [WhitePromote -> 0]; [WhiteQMove -> 0];
- [WhiteBeat -> 0]; [WhiteBeatPromote -> 0]; [WhiteQBeat -> 0];
- [WhiteBeatCont -> 3]
- }
-}
-LOC 2 {
- PLAYER 1 {
- PAYOFF :(ex x w(x)) - :(ex x b(x))
- MOVES [RedBeatBoth -> 1]; [RedBeatPromote -> 1]; [RedBeatBothCont -> 2]
- }
- PLAYER 2 {
- PAYOFF :(ex x b(x)) - :(ex x w(x))
- }
-}
-LOC 3 {
- PLAYER 1 {
- PAYOFF :(ex x w(x)) - :(ex x b(x))
- }
- PLAYER 2 {
- PAYOFF :(ex x b(x)) - :(ex x w(x))
- MOVES
- [WhiteBeatBoth -> 0]; [WhiteBeatPromote -> 0]; [WhiteBeatBothCont -> 3]
- }
-}
-MODEL [ | Wq:1 { }; Bq:1 { } |
- ] \"
- ... ... ... ...
- B.. B.. B.. B..
- ... ... ... ...
- B.. B.. B.. B..
- ... ... ... ...
- B.. B.. B.. B..
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- W.. W.. W.. W..
- ... ... ... ...
- W.. W.. W.. W..
- ... ... ... ...
- W.. W.. W.. W..
-\" with
-IsFirst(x) = not ex z C(z, x) ;
-IsEight(x) = not ex z C(x, z) ;
-DiagWa (x, y) = ex z (C(x, z) and R(y, z)) ;
-DiagBa (x, y) = ex z (C(z, x) and R(z, y)) ;
-DiagWb (x, y) = ex z (C(x, z) and R(z, y)) ;
-DiagBb (x, y) = ex z (C(z, x) and R(y, z)) ;
-DiagW2 (x, y, z) =
- (DiagWa (x, y) and DiagWa (y, z)) or (DiagWb (x, y) and DiagWb (y, z)) ;
-DiagB2 (x, y, z) =
- (DiagBa (x, y) and DiagBa (y, z)) or (DiagBb (x, y) and DiagBb (y, z))
-")
-
-let gomoku_str = ("
-PLAYERS 1, 2
-DATA rCircle: circle, rCross: line, adv_ratio: 5, depth: 2
-REL Row5 (x, y, z, v, w) = R(x, y) and R(y, z) and R(z, v) and R(v, w)
-REL Col5 (x, y, z, v, w) = C(x, y) and C(y, z) and C(z, v) and C(v, w)
-REL DiagA5 (x, y, z, v, w) =
- DiagA(x, y) and DiagA(y, z) and DiagA(z, v) and DiagA(v, w)
-REL DiagB5 (x, y, z, v, w) =
- DiagB(x, y) and DiagB(y, z) and DiagB(z, v) and DiagB(v, w)
-REL Conn5 (x, y, z, v, w) =
- Row5(x,y,z,v,w) or Col5(x,y,z,v,w) or DiagA5(x,y,z,v,w) or DiagB5(x,y,z,v,w)
-REL WinQ() =
- ex x,y,z,v,w (Q(x) and Q(y) and Q(z) and Q(v) and Q(w) and Conn5(x,y,z,v,w))
-REL WinP() =
- ex x,y,z,v,w (P(x) and P(y) and P(z) and P(v) and P(w) and Conn5(x,y,z,v,w))
-RULE Cross:
- [a1 | P:1 {}; Q:1 {} | - ]
- ->
- [a1 | P (a1); Q:1 {} | - ]
- emb Q, P pre not WinQ()
-RULE Circle:
- [a1 | P:1 {}; Q:1 {} | - ]
- ->
- [a1 | P:1 {}; Q (a1) | - ]
- emb Q, P pre not WinP()
-LOC 0 {
- PLAYER 1 {
- PAYOFF :(WinP()) - :(WinQ())
- MOVES [Cross -> 1]
- }
- PLAYER 2 { PAYOFF :(WinQ()) - :(WinP()) }
-}
-LOC 1 {
- PLAYER 1 { PAYOFF :(WinP()) - :(WinQ()) }
- PLAYER 2 {
- PAYOFF :(WinQ()) - :(WinP())
- MOVES [Circle -> 0]
- }
-}
-MODEL [ | P:1 {}; Q:1 {} | ] \"
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
- ... ... ... ...
-\" with DiagA (x, y) = ex u (R(x, u) and C(u, y));
- DiagB (x, y) = ex u (R(x, u) and C(y, u))
-")
-
-let entanglement_str = ("
-PLAYERS 1, 2
-RULE Follow:
- [ a1, a2 | C { (a2) }; R { (a1) } |
- vx { a1->0., a2->0. }; vy { a1->0., a2->0. };
- x { a1->-10., a2->-10. }; y { a1->-10., a2->10. } ]
- ->
- [ a1, a2 | C { (a1) }; R { (a1) } |
- vx { a1->0., a2->0. }; vy { a1->0., a2->0. };
- x { a1->-10., a2->-10. }; y { a1->-10., a2->10. } ]
-emb R, C
-RULE Wait:
- [ a1 | R { (a1) } |
- vx { a1->0. }; vy { a1->0. }; x { a1->-10. }; y { a1->-10. } ]
- ->
- [ a1 | R { (a1) } |
- vx { a1->0. }; vy { a1->0. }; x { a1->-10. }; y { a1->-10. } ]
-emb R, C
-RULE Run:
- [ a1, a2 | C:1 { }; E { (a1, a2) }; R { (a1) }; _opt_C { (a1) } |
- vx { a1->0., a2->0. }; vy { a1->0., a2->0. };
- x { a1->-10., a2->10. }; y { a1->-10., a2->-10. } ]
- ->
- [ a1, a2 | C:1 { }; E { (a1, a2) }; R { (a2) }; _opt_C { (a1) } |
- vx { a1->0., a2->0. }; vy { a1->0., a2->0. };
- x { a1->-10., a2->10. }; y { a1->-10., a2->-10. } ]
-emb R, C
-LOC 0 {
- PLAYER 1 {
- PAYOFF 0.
- MOVES [Follow -> 1]; [Wait -> 1]
- }
- PLAYER 2 { PAYOFF 0. }
-}
-LOC 1 {
- PLAYER 1 { PAYOFF 1. }
- PLAYER 2 {
- PAYOFF -1.
- MOVES [Run -> 0]
- }
- }
-MODEL [ d4, a2, a1, b1, b2, e4, c2, c1, f4, d2, d1, f1, f2, g1, g2, h1, h2, e1, e2, i1, i2 | C { (d4); (e4); (f4) }; E { (a2, a1); (a2, b2); (a1, a2); (a1, b1); (b1, a1); (b1, b2); (b1, c1); (b2, a2); (b2, b1); (b2, c2); (c2, b2); (c2, c1); (c2, d2); (c1, b1); (c1, c2); (c1, d1); (d2, c2); (d2, d1); (d2, e1); (d1, c1); (d1, d2); (d1, e2); (f1, f2); (f1, g1); (f1, e1); (f2, f1); (f2, g2); (f2, e2); (g1, f1); (g1, g2); (g1, h1); (g2, f2); (g2, g1); (g2, h2); (h1, g1); (h1, h2); (h1, i1); (h2, g2); (h2, h1); (h2, i2); (e1, d2); (e1, f1); (e1, e2); (e2, d1); (e2, f2); (e2, e1); (i1, h1); (i1, i2); (i2, h2); (i2, i1) }; R { (e1) }; _opt_C:1 { } | vx { d4->0., a2->0., a1->0., b1->0., b2->0., e4->0., c2->0., c1->0., f4->0., d2->0., d1->0., f1->0., f2->0., g1->0., g2->0., h1->0., h2->0., e1->0., e2->0., i1->0., i2->0. }; vy { d4->0., a2->0., a1->0., b1->0., b2->0., e4->0., c2->0., c1->0., f4->0., d2->0., d1->0., f1->0., f2->0., g1->0., g2->0., h1->0., h2->0., e1->0., e2->0., i1->0., i2->0. }; x { d4->100., a2->-50., a1->-50., b1->0., b2->0., e4->150., c2->50., c1->50., f4->200., d2->100., d1->100., f1->200., f2->200., g1->250., g2->250., h1->300., h2->300., e1->150., e2->150., i1->350., i2->350. }; y { d4->-150., a2->-100., a1->-50., b1->-50., b2->-100., e4->0., c2->-100., c1->-50., f4->-150., d2->-100., d1->-50., f1->-100., f2->-50., g1->-100., g2->-50., h1->-100., h2->-50., e1->-100., e2->-50., i1->-100., i2->-50. } ]
-")
-
-let tictactoe_str = ("
-PLAYERS 1, 2
-DATA r1: circle, r2: line, adv_ratio: 5, depth: 3
-REL DiagA (x, y) = ex u (R(x, u) and C(u, y))
-REL DiagB (x, y) = ex u (R(x, u) and C(y, u))
-REL Row3 (x, y, z) = R(x, y) and R(y, z)
-REL Col3 (x, y, z) = C(x, y) and C(y, z)
-REL DiagA3 (x, y, z) = DiagA(x, y) and DiagA(y, z)
-REL DiagB3 (x, y, z) = DiagB(x, y) and DiagB(y, z)
-REL Conn3 (x, y, z) =
- Row3(x, y, z) or Col3(x, y, z) or DiagA3(x, y, z) or DiagB3(x, y, z)
-REL WinQ() = ex x, y, z (Q(x) and Q(y) and Q(z) and Conn3(x, y, z))
-REL WinP() = ex x, y, z (P(x) and P(y) and P(z) and Conn3(x, y, z))
-RULE Cross:
- [a | P:1 {} | - ] -> [a | P (a) | - ] emb Q, P pre not WinQ()
-RULE Circle:
- [a | Q:1 {} | - ] -> [a | Q (a) | - ] emb Q, P pre not WinP()
-LOC 0 {
- PLAYER 1 { PAYOFF :(WinP()) - :(WinQ())
- MOVES [Cross -> 1] }
- PLAYER 2 { PAYOFF :(WinQ()) - :(WinP()) }
-}
-LOC 1 {
- PLAYER 1 { PAYOFF :(WinP()) - :(WinQ()) }
- PLAYER 2 { PAYOFF :(WinQ()) - :(WinP())
- MOVES [Circle -> 0] }
-}
-MODEL [ | P:1 {}; Q:1 {} | ] \"
-
- . . .
-
- . . .
-
- . . .
-\"
-")
-
-let predef_games =
- [
- "Breakthrough", breakthrough_str;
- "Checkers", checkers_str;
- "Chess", chess_str;
- "Connect4", connect4_str;
- "Entanglement", entanglement_str;
- "Gomoku", gomoku_str;
- "Pawn-Whopping", pawn_whopping_str;
- "Tic-Tac-Toe", tictactoe_str;
- ]
-
-let games = ref [compile_game_data "Tic-Tac-Toe" tictactoe_str]
Modified: trunk/Toss/Client/JsHandler.ml
===================================================================
--- trunk/Toss/Client/JsHandler.ml 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Client/JsHandler.ml 2012-03-09 12:05:53 UTC (rev 1686)
@@ -1,25 +1,93 @@
(* JavaScript Handler for a subset of ReqHandler.handle_http_post requests. *)
+(* In-source definitions of several games, loading games from strings. *)
+
+type game_state_data = {
+ heuristic : Formula.real_expr array array; (** heuristic *)
+ game_state : (Arena.game * Arena.game_state); (** game and state *)
+ playclock : int; (** playclock *)
+ game_str : string; (** game representation *)
+}
+
+
+(* This is a hack to speed-up JS loading of games with harder heuristics.
+ We should remove it and optimize expansion and Heuristic ml instead. *)
+let expansion_cache =
+ [("Pawn-Whopping", [("ex x (bP(x) and not ex y C(y, x)) or not ex z wP(z)",
+ ["bP"; "wP"],
+ ("ex x (bP(x) and " ^
+ "ex y5, y4, y3, y2, y1, y0, y " ^
+ "(C(y4, y5) and C(y3, y4) and C(y2, y3) and " ^
+ "C(y1, y2) and C(y0, y1) and C(y, y0) and C(x, y)))"^
+ " or all z not wP(z)"));
+ ("ex x (wP(x) and not ex y C(x, y)) or not ex z bP(z)",
+ ["bP"; "wP"],
+ ("ex x (wP(x) and " ^
+ "ex y5, y4, y3, y2, y1, y0, y " ^
+ "(C(y5, y4) and C(y4, y3) and C(y3, y2) and " ^
+ "C(y2, y1) and C(y1, y0) and C(y0, y) and C(y, x)))"^
+ "or all z not bP(z)"));
+ ]);
+ ("Breakthrough", [("ex x (B(x) and not ex y C(y, x))", ["B"; "W"],
+ ("ex x (B(x) and ex y5, y4, y3, y2, y1, y0, y " ^
+ "(C(y4, y5) and C(y3, y4) and C(y2, y3) and " ^
+ "C(y1, y2) and C(y0, y1) and C(y,y0) and C(x,y)))"));
+ ("ex x (W(x) and not ex y C(x, y))", ["B"; "W"],
+ ("ex x (W(x) and ex y5, y4, y3, y2, y1, y0, y " ^
+ "(C(y5, y4) and C(y4, y3) and C(y3,y2) and C(y2,y1)"^
+ " and C(y1, y0) and C(y0, y) and C(y, x)))"))])]
+
+let add_expansion_cache game_name game_state =
+ let f_of_s s = FormulaParser.parse_formula Lexer.lex (Lexing.from_string s) in
+ try let lst = List.assoc game_name expansion_cache in
+ List.iter (fun (f, frels, res) -> Heuristic.cache_expanded_form
+ (f_of_s f) game_state.Arena.struc frels (f_of_s res)) lst
+ with Not_found -> ()
+
+let compile_game_data game_name game_str =
+ LOG 1 "parsing";
+ let (game, game_state as game_with_state) =
+ ArenaParser.parse_game_state Lexer.lex (Lexing.from_string game_str) in
+ LOG 1 "heuristic";
+ add_expansion_cache game_name game_state;
+ let heuristic = Heuristic.compute_heuristic game_with_state in
+ LOG 1 "computed";
+ game_name,
+ {heuristic = heuristic;
+ game_state = game_with_state;
+ playclock = 30; (* game clock from where? *)
+ game_str = game_str;
+ }
+
+let gSel_predef_games = [
+ ("Breakthrough", AuxIO.input_file "examples/Breakthrough.toss");
+ ("Checkers", AuxIO.input_file "examples/Checkers.toss");
+ ("Chess", AuxIO.input_file "examples/Chess.toss");
+ ("Connect4", AuxIO.input_file "examples/Connect4.toss");
+ ("Entanglement", AuxIO.input_file "examples/Entanglement.toss");
+ ("Gomoku", AuxIO.input_file "examples/Gomoku.toss");
+ ("Pawn-Whopping", AuxIO.input_file "examples/Pawn-Whopping.toss");
+ ("Tic-Tac-Toe", AuxIO.input_file "examples/Tic-Tac-Toe.toss");
+]
+
+let gSel_games = ref [compile_game_data "Tic-Tac-Toe"
+ (AuxIO.input_file "examples/Tic-Tac-Toe.toss")]
+
+
(* ---------- Basic request type and internal handler ---------- *)
-open GameSelection
(* History of states in last-in-first-out order. *)
let play_states = ref []
+
(* Arbitrarily initialized -- [cur_game] only has effect with
non-empty [play_states]. The game state in any [game_data] is only
the initial state, not the current state of a game. *)
-let cur_game = ref (snd (List.hd !GameSelection.games))
+let cur_game = ref (snd (List.hd !gSel_games))
let cur_move = ref 0
let cur_all_moves = ref [| |]
-(* TODO; FIXME; remove the function below. *)
-let select_moving a = (* temporary func - accept just one player w/ moves *)
- let locs = Aux.array_find_all (fun l -> l.Arena.moves <> []) a in
- if List.length locs <> 1 then failwith "too many moves" else
- if locs = [] then a.(0) else List.hd locs
-
(* ------------ The Handler ------------ *)
let js = Js.string
@@ -151,16 +219,16 @@
let new_play game_name pl1 pl2 =
(* players are currently not used by [JsHandler] *)
let game_name = of_js game_name in
- let game_loaded = List.mem_assoc game_name !GameSelection.games in
+ let game_loaded = List.mem_assoc game_name !gSel_games in
if game_loaded
then LOG 1 "new_play: %s already loaded." game_name
else LOG 1 "new_play: loading %s..." game_name;
let game_data =
- try List.assoc game_name !GameSelection.games
+ try List.assoc game_name !gSel_games
with Not_found ->
let game_data = compile_game_data game_name
- (List.assoc game_name GameSelection.predef_games) in
- games := game_data :: !games;
+ (List.assoc game_name gSel_predef_games) in
+ gSel_games := game_data :: !gSel_games;
snd game_data in
if not game_loaded then
LOG 1 "new_play: %s loaded." game_name;
@@ -208,6 +276,16 @@
let _ = set_handle "precache" precache
+let game_info timeout =
+ let game, _ = !cur_game.game_state in
+ let state = List.hd !play_states in
+ let hs a = String.concat "#" (Array.to_list (Array.map Formula.real_str a)) in
+ let h= String.concat "#" (Array.to_list (Array.map hs !cur_game.heuristic)) in
+ js(Printf.sprintf "%f#%s#%s" (Js.to_float timeout)
+ (Arena.state_str (game, state)) h)
+
+let _ = set_handle "gameinfo" game_info
+
(* When called in a different thread, we can't call continuation. So
arrange to do it from "outside". *)
let suggest player_name time =
@@ -241,8 +319,28 @@
let _ = set_handle "suggest" suggest
+(* Given a move string, construct the suggested move. *)
+let suggested_move move_js =
+ try
+ let game, _ = !cur_game.game_state in
+ let move_s, state = of_js move_js, List.hd !play_states in
+ let move_id = Aux.array_argfind
+ (fun (_, m, _) -> Move.move_gs_str state m = move_s) !cur_all_moves in
+ let result =
+ js_of_move game state move_id (!cur_all_moves.(move_id)) in
+ Js.Unsafe.set result (js"comp_iters")
+ (Js.number_of_float (float_of_int 0));
+ Js.Unsafe.set result (js"comp_started")
+ (Js.number_of_float (AuxIO.gettimeofday ()));
+ Js.Unsafe.set result (js"comp_ended")
+ (Js.number_of_float (AuxIO.gettimeofday ()));
+ Js.some result
+ with Not_found -> Js.null
+
+let _ = set_handle "suggested_move" suggested_move
+
let get_game game_name =
- let game_data = List.assoc (of_js game_name) !GameSelection.games in
+ let game_data = List.assoc (of_js game_name) !gSel_games in
js game_data.game_str
let _ = set_handle "get_game" get_game
@@ -250,7 +348,7 @@
let set_game game_name game_str =
let game_name = of_js game_name and game_str = of_js game_str in
try
- games := compile_game_data game_name game_str :: !games;
+ gSel_games := compile_game_data game_name game_str :: !gSel_games;
js ("Game "^game_name^" set.")
with Lexer.Parsing_error s ->
js ("Game "^game_name^" ERROR: "^s)
Modified: trunk/Toss/Client/Main.js
===================================================================
--- trunk/Toss/Client/Main.js 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Client/Main.js 2012-03-09 12:05:53 UTC (rev 1686)
@@ -560,6 +560,34 @@
}
}
+
+// Send [msg] to server asynchronously, ignore response text.
+var ASYNC_ALL_REQ_PENDING = 0;
+function async_server_msg (msg, count, f) {
+ var xml_request = new XMLHttpRequest ();
+ xml_request.open ('POST', 'Handler', true);
+ xml_request.setRequestHeader (
+ 'Content-Type', 'application/x-www-form-urlencoded; charset=UTF-8');
+ if (count) {
+ xml_request.onreadystatechange = function () {
+ if (xml_request.readyState == 4) {
+ ASYNC_ALL_REQ_PENDING -= 1;
+ resp = xml_request.responseText;
+ f (resp);
+ }
+ }
+ } else {
+ xml_request.onreadystatechange = function () {
+ if (xml_request.readyState == 4) {
+ resp = xml_request.responseText;
+ f (resp);
+ }
+ }
+ };
+ if (count) { ASYNC_ALL_REQ_PENDING += 1; }
+ xml_request.send (msg);
+}
+
function suggest_move_async (time, f) {
show_moving_msg (time);
var fm = function (m) {
@@ -578,9 +606,14 @@
// I'm not sure about players being numbered from 1
// anyway, player name is ignored in ASYNCH suggest
if (typeof time == 'string') time = parseFloat (time);
- ASYNCH ("suggest",
- [PLAYS[CUR_PLAY_I].cur_state.players[0]+1, time],
- fm);
+ var server_move = function (msg) {
+ async_server_msg (msg, false, function (resp) {
+ ASYNCH ("suggested_move", [resp], fm) })
+ }
+ ASYNCH ("gameinfo", [time], server_move);
+ //ASYNCH ("suggest",
+ // [PLAYS[CUR_PLAY_I].cur_state.players[0]+1, time],
+ // fm);
}
}
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Formula/Aux.ml 2012-03-09 12:05:53 UTC (rev 1686)
@@ -465,13 +465,16 @@
| x :: xs -> aux xs in
aux xs
-let take_n n l =
+let take_n_with_rest n l =
let rec aux n acc = function
| hd::tl when n > 0 ->
- aux (n-1) (hd::acc) tl
- | _ -> acc in
- List.rev (aux n [] l)
+ aux (n-1) (hd::acc) tl
+ | r -> acc, r in
+ let (acc, rest) = aux n [] l in
+ List.rev acc, rest
+let take_n n l = fst (take_n_with_rest n l)
+
let rec range ?(from=0) k =
if from >= k then [] else from :: range ~from:(from+1) k
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Formula/Aux.mli 2012-03-09 12:05:53 UTC (rev 1686)
@@ -230,6 +230,10 @@
contain enough values. *)
val take_n : int -> 'a list -> 'a list
+(** Take [n] elements of the given list, or less it the list does not
+ contain enough values. Return the rest-list as the second argument. *)
+val take_n_with_rest : int -> 'a list -> 'a list * 'a list
+
(** Returns an int list from [from] (default 0) to k-1.*)
val range: ?from : int -> int -> int list
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2012-03-08 20:18:20 UTC (rev 1685)
+++ trunk/Toss/Formula/BoolFormula.ml 2012-03-09 12:05:53 UTC (rev 1686)
@@ -6,7 +6,7 @@
let auxcnf_generation = ref 2
let set_auxcnf i = (auxcnf_generation := i)
-let simplification = ref 7
+let simplification = ref 2
let set_simplification i = (simplification := i)
(* bit 0 : subsumption test after cnf conversion
bit 1 : full-fledged simplification
@@ -21,7 +21,7 @@
(* This type describes formulas of relational logic with equality.
We allow only simple boolean junctors, other are resolved during parsing. *)
type bool_formula =
- BVar of int
+ | BVar of int
| BNot of bool_formula
| BAnd of bool_formula list
| BOr of bool_formula list
@@ -41,7 +41,7 @@
(** Print a Boolean formula as a string. *)
let rec str = function
- BVar v -> var_str v
+ | BVar v -> var_str v
| BNot phi -> "(not " ^ (str phi) ^ ")"
| BAnd [] -> "true"
| BOr [] -> "false"
@@ -49,7 +49,7 @@
| BOr (bflist) -> bf_list_str " or " bflist
and bf_list_str sep = function
- [] -> "[]"
+ | [] -> "[]"
| [phi] -> str phi
| lst -> "(" ^ (String.concat sep (List.map str lst)) ^ ")"
@@ -63,27 +63,27 @@
(* Helper function: compare lists lexicographically by [cmp]. *)
let rec compare_lists_lex cmp = function
- ([], []) -> 0
+ | ([], []) -> 0
| ([], _) -> -1
| (_, []) -> 1
| (x :: xs, y :: ys) ->
- let c = cmp x y in
- if c <> 0 then c else compare_lists_lex cmp (xs, ys)
+ let c = cmp x y in
+ if c <> 0 then c else compare_lists_lex cmp (xs, ys)
let rec compare_var_lists l1 l2 =
if l1 = l2 then 0 else
compare_lists_lex compare_vars (l1, l2)
let rec size ?(acc=0) = function
- BVar _ -> acc + 1
+ | BVar _ -> acc + 1
| BNot phi -> size ~acc:(acc + 1) phi
| BAnd flist | BOr flist ->
- List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
+ List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
let rec rec_compare phi1 phi2 =
let cmp_lists = compare_lists_lex rec_compare in
match (phi1, phi2) with
- (BVar v1, BVar v2) -> compare_vars v1 v2
+ | (BVar v1, BVar v2) -> compare_vars v1 v2
| (BVar _, _) -> -1
| (_, BVar _) -> 1
| (BNot psi1, BNot psi2) -> rec_compare psi1 psi2
@@ -118,7 +118,7 @@
(* Convert a Boolean combination into reduced form (over 'not' and 'or') *)
let rec to_reduced_form ?(neg=false) = function
- BVar v -> if neg then BVar (-1 * v) else BVar v
+ | BVar v -> if neg then BVar (-1 * v) else BVar v
| BNot phi ->
if neg then to_reduced_form ~neg:false phi else
to_reduced_form ~neg:true phi
@@ -134,7 +134,7 @@
(* Convert a Boolean formula to NNF and additionally negate if [neg] is set. *)
let rec to_nnf ?(neg=false) = function
- BVar v -> if neg then BVar (-1 * v) else BVar v
+ | BVar v -> if neg then BVar (-1 * v) else BVar v
| BNot phi -> if neg then to_nnf ~neg:false phi else to_nnf ~neg:true phi
| BAnd (flist) when neg -> BOr (List.map (to_nnf ~neg:true) flist)
| BAnd (flist) -> BAnd (List.map (to_nnf ~neg:false) flist)
@@ -144,71 +144,71 @@
(* Helper function to flatten multiple or's and and's and sort by compare. *)
let rec flatten_sort = function
- BVar _ as phi -> phi
+ | BVar _ as phi -> phi
| BNot (BAnd []) -> BOr[]
| BNot (BOr []) -> BAnd[]
| BNot phi -> BNot (flatten_sort phi)
| BOr flist_orig ->
- let flist = List.map flatten_sort flist_orig in
- let is_or = function BOr _ -> true | _ -> false in
- let (ors_all, non_ors) = List.partition i...
[truncated message content] |
