[Toss-devel-svn] SF.net SVN: toss:[1316] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
|
From: <luk...@us...> - 2011-02-10 12:16:14
|
Revision: 1316
http://toss.svn.sourceforge.net/toss/?rev=1316&view=rev
Author: lukstafi
Date: 2011-02-10 12:16:07 +0000 (Thu, 10 Feb 2011)
Log Message:
-----------
GDL translation work in progress: game rules fully translated into Toss semantics (but not generated yet, only as precondition + update).
Modified Paths:
--------------
trunk/Toss/GGP/GDL.ml
trunk/Toss/GGP/GDL.mli
trunk/Toss/GGP/GDLTest.ml
trunk/Toss/Play/GameTest.ml
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-02-09 03:37:28 UTC (rev 1315)
+++ trunk/Toss/GGP/GDL.ml 2011-02-10 12:16:07 UTC (rev 1316)
@@ -154,6 +154,8 @@
duplication turns out prohibitive, this will be a huge TODO for
this translation framework.)
+ First, we expand all uses of the built-in "role" predicate.
+
(6a) The definition:
[(r, params1) <= body1 ... (r, params_n) <= body_n]
@@ -190,14 +192,14 @@
eliminating the [params] (rather than the [args]) when
possible. Still, we freshen each [vars_i] to avoid capture. We
remember the (uneliminated) [vars_i] in the set of variables
- quantified under the negation. If unification fails, we drop the
- corresponding negated subformula. If unification succeeds but the
- corresponding [body_i] is empty (and, in general, no other
- disjuncts in the negated subformula are left), we drop the branch.
+ quantified existentially under the negation (since the free
+ variables occurring only under the negation are quantified
+ universally there -- it is a positive position). If unification
+ fails, we drop the corresponding negated subformula. If
+ unification succeeds but the corresponding [body_i] is empty (and,
+ in general, no other disjuncts in the negated subformula are
+ left), we drop the branch.
- (6b1) The general case is not implemented yet since it slightly
- complicates the code, and expressivity gain is very small.
-
(7) Generation of rewrite rules when the dynamic relations are not
recursive and are expanded in the GDL definition.
@@ -212,6 +214,9 @@
associated with a single "lead legal" branch of the location's
player.
+ (7a1) Filter "lead legal" rules by satisfiability in the current
+ location plys of the aggregate playout.
+
(7b) We collect all the branches of the "next" relation definition
for which the selected branches of "lead legal" and "noop legal"
(the "joint legal" actions) unify with all (usually one, but we
@@ -274,7 +279,10 @@
disjunct, place the original "next" atom but with meta-variable
positions replaced by _BLANK_ as the head of the "erasure" branch,
apply (and remove) unification atoms resulting from negating the
- "distinct" relation.
+ "distinct" relation. The local variables of newly created negated
+ subformulas become existentially-quantified-under-negation
+ (i.e. universally quantified) (while the local variables of old
+ negated subformulas are "let free").
(7f4) Drop the erasure branches that contradict the "legal"
condition of their rule.
@@ -293,30 +301,43 @@
GDL-originals of branches (so to use GDL atoms for "subsumption
checking" in (7l)).
+ (7i-7k) Variables corresponding to negated "true" atoms
+ that contain locally existentially quantified variables are
+ quantified universally (with a scope containing all their
+ occurrences).
+
+ Implementation: we only introduce universal quantification after
+ filtering (7m), is it OK?
+
(7i-4a) For all subterms of "next" and "true" atoms, identify the
sets of <mask-path, element variable> they "inhabit". Replace a
static fact relation by relations built over a cartesian product
of <mask-path, element variable> sets derived for each static
fact's argument by applying corresponding (4a) relations. For a
- negative literal generate result equivalent to a conjunction of
- negations of generated atoms (FIXME: why disjunction is wrong?).
+ negative literal generate result equivalent to a *conjunction* of
+ negations of generated atoms, but deferred to (7k) to fall under a
+ common disjunction (unless there's only one disjunct).
(7i-4c) Include the (4c) relations for "next" and "true" positive
- atoms. Negative atoms are added with (5) relations since they are
- under a common negation.
+ atoms. Negative atoms are added with (5) relations since they (the
+ (5) predicates and the mask-path anchors of (4c)) are under a
+ common negation.
(7i-4b) Add an appropriate equality relation of (4b) for each case
- of variable shared by terms corresponding to different element
+ of subterm shared by terms corresponding to different element
variables (regardless if the element terms are in positive or
- negative literals). FIXME: any shared subterm, not limited to
- variables, right?
+ negative literals).
Implementation: instead of all subterms we currently only consider
subterms that instantiate (ordinary) variables in the mask
corresponding to the "next"/"true" atom.
+ Reason for unsoundness: inclusion of negative "true" literals in
+ (4b) relations is a necessary "heuristic". Whether to extend it to
+ constant subterms (see above) is not clear.
+
(7i1) Remove branches that are unsatisfiable by their static
- relations (4a), (4b) and (4c) alone.
+ relations (4a), (4b) and (positive) (4c) alone.
(7j) Identify variables in "next" & "true" terms that are
at-or-below meta-variables in the corresponding mask. (Most of
@@ -326,11 +347,14 @@
position). (Note that since branches do not have unfixed variables
anymore, we do not rename variables during duplication.)
+ Implementation: TODO.
+
(7k) Replace the "next" and "true" atoms by the conjunction of
(4c) and (5) predicates over their corresponding variable. (For
negative "true" literals this will be equivalent to a disjunction
of negations of the predicates.) Note that positive static
- relations are already added in (7i-4c).
+ relations are already added in (7i-4c). Handle negative literal
+ translations of (4a, 4c, 5) together.
(7l) Build a pre-lattice of branch bodies w.r.t. subsumption,
in a manner similar to (7b). The subsumption test has to say "no"
@@ -351,8 +375,17 @@
associate the set of branches that do not allow such literal. For
every vector we calculate the complement of the sum of branch sets
associated with every bit. The unique resulting sets are exactly
- the Toss rules precursors.
+ the Toss rules precursors. Heuristic (FIXME: needed?): We only use
+ atoms that are deterministically present or absent in at least
+ some branch for indexing.
+ (7l2) Filter rule candidates so that each has a "does"-specific
+ branch.
+
+ (7l3) Filter out rule candidates that contradict all states
+ from the current location plys of aggregate playout (by their
+ "true" atoms -- "not true" are not valid in the aggregate playout).
+
(7m) Filter the final rule candidates by satisfiability of the
static part (same as (7i1) conjoined).
@@ -362,6 +395,9 @@
branches with unifiers more general than the equiv class, and from
the disjointness conditions and the terminal condition.)
+ (7n1) Prior to translation, expand all variables under
+ meta-variables in "terminal" branches, as in (7j). Implementation TODO.
+
The rewrite rule is generated by joining the derived conjunctions
from "next" atoms as RHS, and from bodies as the
precondition. Exactly the RHS variables are listed in the LHS
@@ -481,9 +517,10 @@
type gdl_atom = string * term list
type gdl_rule = gdl_atom * gdl_atom list * gdl_atom list
(* Definition with expanded definitions: expansion of a negated
- relation brings negated conjunctions. *)
+ relation brings negated (possibly locally existentially quantified)
+ conjunctions. *)
type exp_def_branch =
- term list * gdl_atom list * gdl_atom list list
+ term list * gdl_atom list * (Aux.Strings.t * gdl_atom list) list
type exp_def =
string * exp_def_branch list
@@ -493,8 +530,11 @@
struct type t = string * term list let compare = Pervasives.compare end)
(*
-let branch_vars (args, body, neg_body) =
+ let branch_vars (args, body, neg_body) =
*)
+let rels_vars body =
+ List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map (fun (_,args)->terms_vars args) body)
let rules_of_entry = function
| Datalog (rel, args, body) ->
@@ -542,10 +582,19 @@
head, pos_body, neg_body) bodies
| Atomic (rel, args) -> [(rel, args), [], []]
-let defs_of_rules rules : (string * exp_def_branch list) list =
+let add_neg_body_vars global_vars neg_body =
+ List.map (fun (_, args as a)->
+ let local_vs = Aux.Strings.diff (terms_vars args) global_vars in
+ local_vs, [a]) neg_body
+
+let defs_of_rules rules
+ : (string * exp_def_branch list) list =
Aux.map_reduce
(fun ((drel, params), body, neg_body) ->
- drel,(params, body, List.map (fun a->[a]) neg_body))
+ let global_vs =
+ Aux.Strings.union (terms_vars params) (rels_vars body) in
+ drel,(params, body,
+ add_neg_body_vars global_vs neg_body))
(fun x y->y::x) [] rules
(* Only use [rules_of_defs] when sure that no multi-premise negative
@@ -554,7 +603,7 @@
Aux.concat_map (fun (rel, branches) ->
List.map (fun (args, body, neg_body) ->
let neg_body =
- List.map (function [a]->a | _ -> assert false) neg_body in
+ List.map (function _,[a]->a | _ -> assert false) neg_body in
(rel, args), body, neg_body) branches) defs
(* Stratify either w.r.t. the dependency graph ([~def:true]) or its
@@ -563,11 +612,12 @@
match
List.partition (fun (_, branches) ->
List.for_all (fun (_, body, neg_body) ->
+ let neg_bodies = List.concat (List.map snd neg_body) in
List.for_all (fun (rel1,_) ->
rel1 = "distinct" || rel1 = "true" || rel1 = "does" ||
not (List.mem_assoc rel1 defs))
- (if def then body @ List.concat neg_body
- else List.concat neg_body)) branches) defs
+ (if def then body @ neg_bodies
+ else neg_bodies)) branches) defs
with
| [], [] ->
(* {{{ log entry *)
@@ -615,6 +665,7 @@
| Func (f, args) ->
Func (f, List.map (subst_one sb) args)
+(* Eliminate [terms1] variables when possible. *)
let rec unify sb terms1 terms2 =
match terms1, terms2 with
| [], [] -> sb
@@ -715,6 +766,10 @@
if rel1 = rel2 then unify [] args1 args2
else raise Not_found
+let unifies term1 term2 =
+ try ignore (unify [] [term1] [term2]); true
+ with Not_found -> false
+
let subst_rel sb (rel, args) = rel, List.map (subst sb) args
let subst_rels sb body = List.map (subst_rel sb) body
let extend_sb sb1 sb = Aux.map_prepend sb1 (fun (x,t)->x, subst sb1 t) sb
@@ -727,8 +782,8 @@
let subst_br sb (head, body, neg_body) =
List.map (subst sb) head,
- List.map (subst_rel sb) body,
- List.map (List.map (subst_rel sb)) neg_body
+ subst_rels sb body,
+ List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body
let fact_str (rel, args) =
"("^rel^" "^String.concat " " (List.map term_str args) ^")"
@@ -738,26 +793,42 @@
"("^String.concat " " (List.map term_str tup) ^")" in
String.concat " " (List.map tup_str tups)
+let terms_str facts =
+ String.concat ", " (List.map term_str facts)
+
let facts_str facts =
String.concat " " (List.map fact_str facts)
let neg_facts_str negs =
String.concat " "
- (List.map (fun d -> "(not (and "^facts_str d^"))") negs)
+ (List.map (fun (vs,d) ->
+ let vs = Aux.Strings.elements vs in
+ let q = if vs = [] then ""
+ else "forall "^String.concat ", " vs in
+ q ^ "(not (and "^facts_str d^"))") negs)
+let branch_str rel (args, body, neg_body) =
+ "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
+ " " ^ neg_facts_str neg_body ^ ")"
+
let def_str (rel, branches) =
String.concat "\n" (List.map (fun (args, body, neg_body) ->
"("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
" " ^ neg_facts_str neg_body ^ ")"
) branches)
-
-let rule_pretransl_str (heads, bodies, neg_bodies) =
- "("^ facts_str bodies ^
- " " ^ neg_facts_str neg_bodies ^ "==>" ^
- String.concat "; " (List.map term_str heads) ^ ")"
-
+(*
+let rule_str (head, body, neg_body) =
+ String.concat "\n" (List.map (fun (args, body, neg_body) ->
+ "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^
+ " " ^ String.concat " "
+ (List.map (fun f->"not "^fact_str f) neg_body) ^ ")"
+ ) branches)
+*)
let sb_str sb =
String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb)
+let proto_rel_str (rel, args) =
+ rel ^"(" ^ String.concat ", " (Array.to_list args) ^")"
+
(* 1b *)
(* TODO: optimize by using rel-indexing (also in [aggregate_playout]).
@@ -884,9 +955,14 @@
Func (f, List.map map_vnames args) in
let map_rel (rel, args) =
rel, List.map map_vnames args in
+ let map_neg (vs, atoms) =
+ Aux.strings_of_list
+ (List.map (fun x-> x^string_of_int !freshen_count)
+ (Aux.Strings.elements vs)),
+ List.map map_rel atoms in
List.map map_vnames args,
List.map map_rel body,
- List.map (List.map map_rel) neg_body
+ List.map map_neg neg_body
let freshen_def_branches =
List.map freshen_branch
@@ -917,7 +993,8 @@
let sb1 = unify [] dparams args in
Some (
subst_rels sb1 (dbody @ pos_sol),
- List.map (subst_rels sb1) (dneg_body @ neg_sol),
+ List.map (fun (vs,bs)->vs, subst_rels sb1 bs)
+ (dneg_body @ neg_sol),
extend_sb sb1 sb)
with Not_found -> None
) def
@@ -928,32 +1005,46 @@
([[],[],[]]) body in
(* 6b *)
let sols =
- List.fold_left (fun sols -> function [rel, args as atom] ->
- (let try def =
- freshen_def_branches (List.assoc rel defs) in
- List.map (fun (pos_sol, neg_sol, sb) ->
- let args = List.map (subst sb) args in
- let more_neg =
- Aux.map_some (fun (dparams, dbody, dneg_body) ->
- if dneg_body <> [] then
- failwith
- ("GDL.subst_def_branch: negation in negatively used" ^
- " defined rels not supported yet, relation "^rel);
- try
- let sb1 = unify [] dparams args in
- Some (subst_rels sb1 dbody)
- with Not_found -> None
- ) def in
- pos_sol, more_neg @ neg_sol, sb
- ) sols
- with Not_found ->
- List.map (fun (pos_sol, neg_sol, sb) ->
- pos_sol, [subst_rel sb atom]::neg_sol, sb) sols)
- | _ -> failwith
- "GDL.subst_def_branch: unimplemented, see (6b1) of spec")
- sols neg_body in
+ (* no branch duplication, but each negation has its own substitution *)
+ List.map (fun (pos_sol, neg_sol, sb) ->
+ let more_neg_sol =
+ Aux.concat_map (fun (uni_vs, neg_conjs) ->
+ (* negated subformulas are duplicated instead *)
+ List.fold_left (fun neg_sol (rel, args as atom) ->
+ (let try def =
+ freshen_def_branches (List.assoc rel defs) in
+ Aux.concat_map (fun (uni_vs, neg_acc, sb) ->
+ let args = List.map (subst sb) args in
+ Aux.map_try (fun (dparams, dbody, dneg_body) ->
+ if dneg_body <> [] then
+ failwith
+ ("GDL.subst_def_branch: negation in negatively used" ^
+ " defined rels not supported yet, relation "^rel);
+ (let sb1 = unify [] dparams args in
+ let param_vars = terms_vars dparams in
+ let body_vars = rels_vars dbody in
+ let dbody = subst_rels sb1 dbody in
+ let local_vs =
+ Aux.Strings.inter (Aux.Strings.diff body_vars param_vars)
+ (rels_vars dbody) in
+ let neg_acc = subst_rels sb1 neg_acc in
+ Aux.Strings.union uni_vs local_vs,
+ dbody @ neg_acc,
+ extend_sb sb1 sb)
+ ) def) neg_sol
+ with Not_found -> (* rel not in defs *)
+ List.map (fun (uni_vs, neg_acc, sb) ->
+ uni_vs, subst_rel sb atom::neg_acc, sb) neg_sol)
+ ) [uni_vs, [], sb] neg_conjs
+ ) neg_body in
+ let more_neg_sol =
+ List.map (fun (uni_vs, neg_conjs,_) -> uni_vs, neg_conjs)
+ more_neg_sol in
+ List.rev pos_sol, List.rev_append neg_sol more_neg_sol, sb
+ ) sols in
Aux.map_some (fun (pos_sol, neg_sol, sb) ->
- if List.mem [] neg_sol then None
+ if List.exists (function _,[] -> true | _ -> false) neg_sol
+ then None
else Some (List.map (subst sb) head, pos_sol, neg_sol)) sols
(* Stratify and expand all relations in the given set. *)
@@ -991,25 +1082,29 @@
(legal_args, legal_body, legal_neg_body : exp_def_branch)
(head, body, neg_body : exp_def_branch)
: (exp_def_branch * exp_def_branch) option =
- if List.exists (List.exists (fun (rel,_)->rel="does")) neg_body
+ if List.exists (fun (_,neg_conjs) ->
+ List.exists (fun (rel,_)->rel="does") neg_conjs) neg_body
then failwith
"GDL.translate_game: negated \"does\" conditions not implemented yet";
try
let body, more_neg_body, sb =
List.fold_left (fun (body,more_neg_body,sb) (rel, args as atom) ->
if rel = "does" then
- List.rev_append legal_body body,
+ ("_DOES_PLACEHOLDER_", args) :: List.rev_append legal_body body,
List.rev_append legal_neg_body more_neg_body,
unify sb legal_args args
else atom::body, more_neg_body, sb) ([],[],[]) body in
-
Some (
(List.map (subst sb) legal_args,
- List.map (subst_rel sb) legal_body,
- List.map (List.map (subst_rel sb)) legal_neg_body),
+ subst_rels sb legal_body,
+ List.map (fun (uni_vs,neg_conjs) ->
+ (* local variables so cannot be touched *)
+ uni_vs, subst_rels sb neg_conjs)
+ legal_neg_body),
(List.map (subst sb) head,
- List.map (subst_rel sb) (List.rev body),
- List.map (List.map (subst_rel sb))
+ subst_rels sb (List.rev body),
+ List.map (fun (uni_vs, neg_conjs) ->
+ uni_vs, subst_rels sb neg_conjs)
(List.rev_append more_neg_body neg_body)))
with Not_found -> None
@@ -1072,21 +1167,17 @@
else dynamic_rules in
let rec loop actions_accu state_accu step state =
(* {{{ log entry *)
-
if !debug_level > 0 then (
Printf.printf "aggregate_playout: step %d...\n%!" step
);
-
(* }}} *)
(let try actions, next =
aggregate_ply players static_base state state_rules in
(* {{{ log entry *)
-
if !debug_level > 0 then (
Printf.printf "aggregate_playout: state %s\n%!"
(String.concat " " (List.map term_str next))
);
-
(* }}} *)
if step < horizon then
loop (actions::actions_accu) (state::state_accu) (step+1) next
@@ -1183,9 +1274,9 @@
let mask, _, _, blank = term_to_blank masks term in
mask, Formula.fo_var_of_string (term_to_name blank)
-let translate_branches struc masks static_rnames dyn_rels brs =
+let translate_branches struc masks static_rnames dyn_rels
+ (brs : exp_def_branch list) =
(* 7i *)
- (* Do not flatten the already built super-partition. *)
let state_terms =
List.fold_left (fun acc -> function
| [next_arg], body, neg_body ->
@@ -1195,16 +1286,29 @@
| "true", _ -> assert false
| _ -> acc) acc body in
let res =
- List.fold_left (List.fold_left (fun acc -> function
- | "true", [true_arg] -> Terms.add true_arg acc
- | "true", _ -> assert false
- | _ -> acc)) res neg_body in
- if next_arg = Const "_TERMINAL_"
+ List.fold_left (fun acc (_, neg_conjs) ->
+ List.fold_left (fun acc -> function
+ | "true", [true_arg] -> Terms.add true_arg acc
+ | "true", _ -> assert false
+ | _ -> acc) acc neg_conjs) res neg_body in
+ if next_arg = Const "_IGNORE_RHS_"
then res
else Terms.add next_arg res
| _ -> assert false
) Terms.empty brs in
let state_terms = Terms.elements state_terms in
+ let uni_gdl_vars =
+ List.fold_left (fun acc (_, _, neg_body) ->
+ Aux.Strings.union acc
+ (List.fold_left Aux.Strings.union Aux.Strings.empty
+ (List.map fst neg_body))
+ ) Aux.Strings.empty brs in
+ let uni_toss_vars =
+ Aux.map_some (fun term ->
+ if Aux.Strings.is_empty
+ (Aux.Strings.inter uni_gdl_vars (term_vars term))
+ then None
+ else Some (snd (toss_var masks term))) state_terms in
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "state_terms: %s\n%!" (
@@ -1220,7 +1324,7 @@
let ptups = List.map (fun arg ->
Aux.assoc_all arg state_subterms) args in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "conjs_4a: of %s = subterms %s\n%!"
(fact_str (rel,args)) (String.concat "; " (
List.map (fun l -> String.concat ", "
@@ -1238,7 +1342,7 @@
Formula.Rel (rname, Array.of_list tup)) ptups in
let res = Aux.unique_sorted res in
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "conjs_4a: of %s = %s\n%!"
(fact_str (rel,args)) (Formula.str (Formula.And res))
);
@@ -1267,7 +1371,7 @@
let brs = Aux.map_some (function
| [next_arg],body,neg_body ->
let phi, lvars =
- if next_arg = Const "_TERMINAL_" then [], ref []
+ if next_arg = Const "_IGNORE_RHS_" then [], ref []
else
let mask, sb, m_sb, blanked = term_to_blank masks next_arg in
let rname = term_to_name mask in
@@ -1297,35 +1401,20 @@
conjs_4a rel args
else []
) body in
+ (* only to prune early *)
let neg_conjs =
- Aux.concat_map (
- Aux.concat_map (fun (rel, args) ->
- if rel = "true" then
- (* lvars := svar :: !lvars; ??? *)
- (* negated (4c) is calculated together with (5) *)
- []
- (*
- let true_arg = List.hd args in
- let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
- let rname = term_to_name mask in
- let _, svar = toss_var masks true_arg in
- let phi = Formula.Rel (rname, [|svar|]) in
- let conjs =
- Aux.map_some (function
- | _, Var _ -> None
- | v, t as v_sb ->
- let rname = term_to_name (subst_one v_sb mask) in
- Some (Formula.Rel (rname, [|svar|]))) sb in
- (* FIXME: make sure it's the right semantics *)
- [phi; Formula.Not (Formula.And/Or conjs)]
- *)
+ Aux.concat_map (function
+ | _, [rel, args] ->
+ if rel = "true" then []
+ else if rel = "_DOES_PLACEHOLDER_"
+ then []
else if List.mem rel static_rnames then
- (* 7i-4a *)
- (* FIXME: And / Or semantics? *)
+ (* 7i-4a *)
List.map (fun c -> Formula.Not c) (conjs_4a rel args)
- (* [Formula.Not (Formula.And (conjs_4a rel args))] *)
- else []
- )) neg_body in
+ else
+ (* dynamic relations have been expanded *)
+ assert false
+ | _ -> []) neg_body in
let all_conjs = phi @ conjs @ neg_conjs in
let phi = Formula.And all_conjs in
let lvars = (!lvars :> Formula.var list) in
@@ -1335,6 +1424,7 @@
let rphi = Solver.M.register_formula
(Formula.And optim_conjs) in
(* {{{ log entry *)
+
if !debug_level > 4 then (
(* do not print, because it generates too many
answers -- too little constraints per number of
@@ -1350,11 +1440,12 @@
(Formula.str phi)
(* (List.length atups) *)
);
+
(* }}} *)
if Solver.M.check_formula struc rphi
then (
(* {{{ log entry *)
- if !debug_level > 3 then (
+ if !debug_level > 4 then (
Printf.printf "holds\n%!"
);
(* }}} *)
@@ -1367,7 +1458,7 @@
let brs =
List.map (fun (static_conjs, (next_arg,body,neg_body)) ->
let rhs_pos_preds, rhs_possneg_preds =
- if next_arg = Const "_TERMINAL_" then [], []
+ if next_arg = Const "_IGNORE_RHS_" then [], []
else
let mask, sb, m_sb, blanked = term_to_blank masks next_arg in
let rhs_elem = term_to_name blanked in
@@ -1404,7 +1495,7 @@
let lhs_possneg_preds = List.flatten lhs_possneg_preds in
*)
lhs_pos_preds
- else if List.mem rel static_rnames
+ else if List.mem rel static_rnames || rel = "_DOES_PLACEHOLDER_"
then []
else (
Printf.printf "\nunexpected_dynamic: %s\n%!" rel;
@@ -1412,42 +1503,86 @@
assert false)
) body in
let neg_conjs =
- Aux.concat_map (
- Aux.concat_map (fun (rel, args) ->
- if rel = "true" then
- let true_arg = List.hd args in
- let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
- let rname = term_to_name mask in
- let _, svar = toss_var masks true_arg in
- let phi = Formula.Rel (rname, [|svar|]) in
- let conjs_4c =
- Aux.map_some (function
- | _, Var _ -> None
- | v, t as v_sb ->
- let rname = term_to_name (subst_one v_sb mask) in
- Some (Formula.Rel (rname, [|svar|]))) sb in
- let conjs_5 =
- List.map (fun (v,t as v_sb) ->
- if t = Const "_BLANK_" then
- assert false
- else
- (* t = Var _ have been expanded *)
- let rname = term_to_name (subst_one v_sb mask) in
- Formula.Rel (rname, [|svar|])) m_sb in
+ Aux.map_some (fun (_, neg_conjs) ->
+ let disjs =
+ Aux.map_some (fun (rel, args) ->
+ if rel = "true" then
+ let true_arg = List.hd args in
+ let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
+ let rname = term_to_name mask in
+ let _, svar = toss_var masks true_arg in
+ let phi = Formula.Rel (rname, [|svar|]) in
+ let conjs_4c =
+ Aux.map_some (function
+ | _, Var _ -> None
+ | v, t as v_sb ->
+ let rname = term_to_name (subst_one v_sb mask) in
+ Some (Formula.Rel (rname, [|svar|]))) sb in
+ let conjs_5 =
+ List.map (fun (v,t as v_sb) ->
+ if t = Const "_BLANK_" then
+ assert false
+ else
+ (* t = Var _ have been expanded *)
+ let rname = term_to_name (subst_one v_sb mask) in
+ Formula.Rel (rname, [|svar|])) m_sb in
- (* FIXME: make sure it's the right semantics *)
- [phi; Formula.Not (Formula.And (conjs_4c @ conjs_5))]
- else if List.mem rel static_rnames
- then []
- else
- (* dynamic relations have been expanded *)
- assert false
- )) neg_body in
+ (* FIXME: make sure it's the right semantics *)
+ Some (Formula.Not (Formula.And (phi :: conjs_4c @ conjs_5)))
+ else if rel = "_DOES_PLACEHOLDER_"
+ then None
+ else if List.mem rel static_rnames then
+ (* 7i-4a *)
+ Some (Formula.And (
+ List.map (fun c -> Formula.Not c) (conjs_4a rel args)))
+ else
+ (* dynamic relations have been expanded *)
+ assert false
+ ) neg_conjs in
+ match disjs with
+ | [] -> None
+ | [disj] -> Some disj
+ | _ -> Some (Formula.Or disjs)) neg_body in
let all_conjs = static_conjs @ dyn_conjs @ neg_conjs in
(rhs_pos_preds, rhs_possneg_preds, static_conjs, all_conjs),
(next_arg, body, neg_body)) brs in
- conjs_4b, brs
+ uni_toss_vars, conjs_4b, brs
+
+let lift_universal (uni_vars : Formula.fo_var list) conjs =
+ let rec flatten_ands = function
+ | Formula.And conjs -> Aux.concat_map flatten_ands conjs
+ | phi -> [phi] in
+ let conjs = Aux.unique_sorted (Aux.concat_map flatten_ands conjs) in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf "lift_universal: vars %s -- conjs:\n%s\n%!"
+ (String.concat ", "
+ (List.map Formula.var_str (uni_vars :> Formula.var list)))
+ (Formula.sprint (Formula.And conjs))
+ );
+ (* }}} *)
+ let uni_vars = (uni_vars :> Formula.var list) in
+ let local, global = List.partition
+ (fun phi ->
+ let phi_vs = FormulaOps.free_vars phi in
+ List.exists (fun v -> List.mem v phi_vs) uni_vars) conjs in
+ let used_uni_vars =
+ List.filter (fun v -> List.mem v uni_vars)
+ (FormulaOps.free_vars (Formula.And local)) in
+ let res =
+ if local = [] then Formula.And global
+ else
+ Formula.And (global @ [
+ Formula.All (used_uni_vars, Formula.And local)]) in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf "lift_universal: result\n%s\n%!"
+ (Formula.sprint res)
+ );
+ (* }}} *)
+ res
+
let translate_game game_descr =
freshen_count := 0;
let player_terms =
@@ -1539,6 +1674,34 @@
done;
loc_noops in
(* 6 *)
+ let expand_roles rules =
+ Aux.concat_map (fun (head, body, neg_body as br) ->
+ let roles, body =
+ List.partition (fun (rel,_)->rel="role") body in
+ let neg_roles, neg_body =
+ List.partition (fun (rel,_)->rel="role") neg_body in
+ let pterms = Array.to_list player_terms in
+ let vs, roles =
+ Aux.partition_map
+ (function _,[Var v] -> Aux.Left v | _,[p] -> Aux.Right p
+ | _ -> assert false) roles in
+ let neg_roles = List.map (function _,[p] -> p
+ | _ -> assert false) neg_roles in
+ if List.exists (fun p -> not (List.mem p pterms)) roles
+ || List.exists (fun p -> List.mem p pterms) neg_roles
+ then []
+ else if vs = [] then [br]
+ else
+ let sbs = Aux.product (List.map (fun _ -> pterms) vs) in
+ List.map (fun sb ->
+ let sb = List.combine vs sb in
+ subst_rel sb head,
+ subst_rels sb body,
+ subst_rels sb neg_body) sbs
+ ) rules in
+ let static_rules = (* Aux.unique_sorted *) (expand_roles static_rules)
+ and dynamic_rules = (* Aux.unique_sorted *) (expand_roles dynamic_rules) in
+
let static_rules, exp_static_rules =
List.partition (fun ((rel,args), _, _) ->
List.length args <= !expand_arity_above ||
@@ -1562,6 +1725,7 @@
(defs_of_rules static_rules)) in
let exp_defs =
expand_def_rules ~more_defs:static_exp_defs dynamic_rules in
+
(* {{{ log entry *)
if !debug_level > 0 then (
Printf.printf "translate_game: All expanded dynamic rules:\n%s\n%!"
@@ -1593,7 +1757,8 @@
("GDL.initialize_game: invalid arity of \"true\" atom"))
| _ -> None) in
let pos_cands = collect body in
- let neg_cands = Aux.concat_map collect neg_body in
+ let neg_cands =
+ Aux.concat_map (fun (_,neg) -> collect neg) neg_body in
let pos_gens = List.map (generalize next_arg) pos_cands in
let neg_gens = List.map (generalize next_arg) neg_cands in
(* using the fact that Pervasives.compare is lexicographic *)
@@ -1818,8 +1983,8 @@
(Array.map (fun player ->
let sb = [v, player] in
[player; subst sb lterm],
- List.map (subst_rel sb) body,
- List.map (List.map (subst_rel sb)) neg_body)
+ subst_rels sb body,
+ List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body)
player_terms)
| [Func _; lterm], _, _ ->
(* TODO: easy to fix *)
@@ -1851,9 +2016,9 @@
&& loc_noop_legal.(i).(p) <> Some legal
then (
Printf.printf "Multiple noops: %s, %s\n%!"
- (term_str (Func ("legal", Aux.fst3 legal)))
- (term_str (Func ("legal", Aux.fst3
- (Aux.unsome loc_noop_legal.(i).(p)))));
+ (branch_str "legal" legal)
+ (branch_str "legal"
+ (Aux.unsome loc_noop_legal.(i).(p)));
assert false)
else loc_noop_legal.(i).(p) <- Some legal
done
@@ -1861,6 +2026,43 @@
| _ -> assert false
) legal_rules;
loc_lead_legal, loc_noop_legal in
+ let agg_actions = Array.of_list agg_actions in
+ (* 7a1 *)
+ let loc_lead_legal = Array.mapi (fun i legals ->
+ let loc_actions = ref [] in
+ Array.iteri (fun ply actions ->
+ if ply mod loc_n = i then
+ loc_actions := actions @ !loc_actions) agg_actions;
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "Possible actions in location %d:\n%s\n%!"
+ i (String.concat "; "
+ (List.map (fun a -> term_str (Func ("legal", a))) !loc_actions))
+ );
+ (* }}} *)
+ let matches head =
+ List.exists (fun action ->
+ try ignore (match_meta [] [] action head); true
+ with Not_found -> false) !loc_actions in
+ let res = List.filter (fun (head, _, _) -> matches head) legals in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "Filtered actions in location %d:\n%s\n\n%!"
+ i (String.concat "; "
+ (List.map (fun (a,_,_) -> term_str (Func ("legal", a))) res))
+ );
+ (* }}} *)
+ res
+ ) loc_lead_legal in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf "Lead actions in locations:\n%!";
+ Array.iteri (fun i lead ->
+ Printf.printf "loc: %d -- %s\n%!" i (
+ String.concat "; "
+ (List.map (fun a -> branch_str "legal" a) lead))) loc_lead_legal
+ );
+ (* }}} *)
(* the joint actions available in a location *)
let loc_joint_legal =
Array.mapi (fun i lead ->
@@ -1876,6 +2078,7 @@
) loc_lead_legal in
(* 7b *)
let grtr ((lead1,_,_), _) ((lead2,_,_), _) = cmp_masks lead2 lead1 in
+ let agg_states = Array.of_list agg_states in
let loc_next_classes =
Array.mapi (fun loc joint_legal_branches ->
Aux.concat_map (fun joint_legal ->
@@ -1924,7 +2127,7 @@
done;
let layers = List.rev !layers in
(* 7d *)
- let rules_brs = List.fold_left
+ let rules_brs : ('a * exp_def_branch list) list = List.fold_left
(* folding reverses order so the maximal layer will
generate the returned classes *)
(fun rules_brs layer ->
@@ -1988,13 +2191,14 @@
let multi_body = List.map
(fun (head2, body2, neg_body2) ->
let sb, _ = match_meta [] [] head head2 in
- List.map (subst_rel sb) body2,
- List.map (List.map (subst_rel sb)) neg_body2
+ subst_rels sb body2,
+ List.map (fun (uni_vs,neg) ->
+ uni_vs, subst_rels sb neg) neg_body2
) f_brs in
head, (body, neg_body)::multi_body
) frames in
(* 7f3 *)
- let erasure_brs = Aux.concat_map
+ let erasure_brs : exp_def_branch list = Aux.concat_map
(function
| [next_arg] as next_args,multi_body ->
let mask, _, _, blank_arg = term_to_blank masks next_arg in
@@ -2024,8 +2228,8 @@
let neg_body =
List.map
(function
- | ["distinct", []] -> assert false
- | ["distinct", arg::more_args] ->
+ | _, ["distinct", []] -> assert false
+ | _, ["distinct", arg::more_args] ->
let _, sb =
List.fold_left (fun (base, sb) arg ->
let sb = unify sb [base] [arg] in
@@ -2038,9 +2242,9 @@
-> v2, Var v1
| vsb -> vsb) sb in
Aux.Right (Aux.Right sb)
- | conj when List.mem_assoc "distinct" conj ->
+ | _, conj when List.mem_assoc "distinct" conj ->
assert false
- | conj ->
+ | _, conj ->
Aux.Right (Aux.Left conj))
neg_body in
body @ neg_body) multi_body in
@@ -2057,8 +2261,13 @@
then None
else
let body = List.map (subst_rel sb) body in
+ let global_vs =
+ Aux.Strings.union (
+ Aux.Strings.union (term_vars next_arg)
+ (rels_vars body)) fixed_vars in
let neg_body =
- List.map (fun a -> [subst_rel sb a]) neg_body in
+ add_neg_body_vars global_vs
+ (subst_rels sb neg_body) in
let head = subst sb blank_arg in
if
(* TODO: (7g) instead *)
@@ -2066,9 +2275,10 @@
fixed_vars &&
(* (7f4) *)
not (List.exists (fun pos ->
- List.mem [pos] lead_neg_body
+ List.exists (fun (_,neg_conjs) ->
+ List.mem pos neg_conjs) lead_neg_body
) body) &&
- not (List.exists (fun neg ->
+ not (List.exists (fun (_,neg) ->
List.for_all
(fun neg->List.mem neg lead_body) neg
) neg_body)
@@ -2108,31 +2318,67 @@
let loc_toss_rules =
Array.mapi (fun loc rules_brs ->
Aux.concat_map (fun (lead, brs) ->
- let conjs_4b, brs =
- translate_branches struc masks static_rnames dyn_rels brs in
-
- (* 7l *)
+ (* we build synthetic branches so as to get a proper partition *)
let atoms =
- List.fold_left (fun acc (_,(_,body,neg_body))->
+ List.fold_left (fun acc (_,body,neg_body)->
List.fold_right Atoms.add body
- (List.fold_right (List.fold_right Atoms.add)
- neg_body acc)
+ (List.fold_right (function
+ | _, [neg] -> Atoms.add neg
+ | _ -> fun x -> x) neg_body acc)
) Atoms.empty brs in
let atoms = Atoms.elements atoms in
+ let atoms = List.filter
+ (fun (rel,_)->rel<>"_DOES_PLACEHOLDER_") atoms in
+ let synth_brs = Aux.concat_map (fun atom ->
+ (* so that RHS are ignored *)
+ [[Const "_IGNORE_RHS_"], [atom], [];
+ [Const "_IGNORE_RHS_"], [], [Aux.Strings.empty, [atom]]]
+ ) atoms in
+ let uni_vars, conjs_4b, brs =
+ translate_branches struc masks static_rnames dyn_rels
+ (brs @ synth_brs) in
+
+ (* 7l *)
let brs = Array.of_list brs in (* indexing branches *)
let full_set = Aux.ints_of_list
(Array.to_list (Array.mapi (fun i _ -> i) brs)) in
+ (* 7l2 *)
+ let does_set = Aux.ints_of_list
+ (Aux.map_some (fun x->x)
+ (Array.to_list (Array.mapi (fun i (_,(_,body,_)) ->
+ if List.exists (
+ function
+ | "_DOES_PLACEHOLDER_",args ->
+ (try ignore (
+ unify [] [loc_players.(loc); Aux.fst3 lead]
+ args); true
+ with Not_found -> false)
+ | _ -> false) body
+ then Some i else None) brs))) in
+ let brs = Array.map (fun (lead,(head,body,neg_body))->
+ let body = List.filter (
+ function "_DOES_PLACEHOLDER_",_ -> false | _ -> true) body in
+ lead, (head, body, neg_body)) brs in
let table = List.map (fun atom ->
let positives = Array.mapi (fun i (_,(_,body,_)) ->
if List.mem atom body then Some i else None) brs in
let positives = Aux.map_some (fun x->x)
(Array.to_list positives) in
let negatives = Array.mapi (fun i (_,(_,_,neg_body)) ->
- if List.exists (List.mem atom) neg_body then Some i
+ (* a disjunction is not enough a reason to exclude a branch *)
+ if List.exists (fun (_,neg)->[atom] = neg) neg_body
+ then Some i
else None) brs in
let negatives = Aux.map_some (fun x->x)
(Array.to_list negatives) in
- Printf.printf "\nd\n%!";
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "Entry for atom %s:\npositives: %s\nnegatives: %s\n%!"
+ (fact_str atom)
+ (String.concat ", "(List.map string_of_int positives))
+ (String.concat ", "(List.map string_of_int negatives))
+ );
+ (* }}} *)
(* first those that allow "P" then those that allow "not P" *)
[Aux.Ints.diff full_set (Aux.ints_of_list negatives);
Aux.Ints.diff full_set (Aux.ints_of_list positives)]
@@ -2140,23 +2386,66 @@
let cases = Aux.product table in
let cases =
List.map (List.fold_left Aux.Ints.inter full_set) cases in
+ let cases = List.filter (fun case ->
+ not (Aux.Ints.is_empty (Aux.Ints.inter does_set case)))
+ cases in
+ (* every partition point has different preconditions... *)
let cases =
- Aux.unique_sorted (List.map Aux.Ints.elements cases) in
- let cases = List.map (fun c_brs ->
+ (* Aux.unique_sorted *) (List.map Aux.Ints.elements cases) in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "CASES:\n%s\n%!" (String.concat "\n" (List.map (
+ fun l -> String.concat ", " (List.map string_of_int l)) cases))
+ );
+ (* }}} *)
+ (* 7l3 *)
+
+ let check_branch body =
+ Aux.array_existsi (fun ply states ->
+ if ply mod loc_n = loc then (
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ let posi =
+ Aux.map_some (function
+ | "true", [st_arg] -> Some st_arg
+ | _ -> None) body in
+ Printf.printf
+ "Checking branch at states:\n%s\npositives:\n%s\n"
+ (terms_str states) (terms_str posi)
+ );
+ (* }}} *)
+ let res =
+ List.for_all (function
+ | "true", [st_arg] ->
+ List.exists (unifies st_arg) states
+ | _ -> true) body in
+ (* {{{ log entry *)
+ if !debug_level > 4 then (
+ Printf.printf "result: %b\n%!" res
+ );
+ (* }}} *)
+ res
+ ) else false) agg_states in
+
+ let cases = Aux.map_try (fun c_brs ->
let c_brs = List.map (Array.get brs) c_brs in
List.fold_left (fun
- ((rhs_pos_acc, rhs_neg_acc, static_conjs_acc, conjs_acc),
- heads, bodies, neg_bodies)
+ (rhs_pos_acc, rhs_neg_acc, static_conjs_acc, conjs_acc)
((rhs_pos, rhs_neg, static_conjs, conjs),
- (head, body, neg_body)) ->
- (rhs_pos @ rhs_pos_acc, rhs_neg @ rhs_neg_acc,
- static_conjs @ static_conjs_acc, conjs @ conjs_acc),
- head::heads,body@bodies,neg_body@neg_bodies)
- (([],[],conjs_4b,conjs_4b),[],[],[]) c_brs
+ (_,body,_)) ->
+ if not (check_branch body)
+ then raise Not_found;
+ rhs_pos @ rhs_pos_acc, rhs_neg @ rhs_neg_acc,
+ static_conjs @ static_conjs_acc, conjs @ conjs_acc)
+ ([],[],conjs_4b,conjs_4b) c_brs
) cases in
(* 7m *)
- let cases = List.filter (fun ((_,_,static_phis,_),
- heads,bodies,neg_bodies) ->
+ let cases = Aux.map_some (fun (rhs_pos,rhs_neg,static_phis,phis) ->
+ if rhs_pos = [] && rhs_neg = [] then None
+ else Some (
+ Aux.unique_sorted rhs_pos, Aux.unique_sorted rhs_neg,
+ static_phis, phis)) cases in
+ let cases = Aux.map_some (fun (rhs_pos,rhs_neg,static_phis,phis) ->
let phi = Formula.And static_phis in
let rphi = Solver.M.register_formula phi in
(* {{{ log entry *)
@@ -2178,25 +2467,32 @@
(* }}} *)
let res = Solver.M.check_formula struc rphi in
(* {{{ log entry *)
- if !debug_level > 3 && res then (
+ if !debug_level > 4 && res then (
Printf.printf "holds\n%!"
);
(* }}} *)
- res) cases in
- List.map (fun case -> lead, case) cases
+ if res then Some (rhs_pos, rhs_neg, phis)
+ else None) cases in
+ List.map (fun (rhs_pos, rhs_neg, conjs) ->
+ lead, (rhs_pos, rhs_neg, lift_universal uni_vars conjs)) cases
) rules_brs
) loc_next_classes in
(* 7n *)
let terminal_brs =
List.map (function
- | [], body, neg_body -> [Const "_TERMINAL_"], body, neg_body
+ | [], body, neg_body -> [Const "_IGNORE_RHS_"], body, neg_body
| _ -> assert false) terminal_rules in
- let terminal_4b, terminal_brs =
+ let terminal_uni_vars, terminal_4b, terminal_brs =
translate_branches struc masks static_rnames dyn_rels terminal_brs in
+ (* lifting will drop spurious (4b) premises *)
let terminal_disjs = List.map (fun ((_,_,_,conjs),_) ->
- Formula.And conjs) terminal_brs in
- let terminal_phi =
- Formula.And [Formula.And terminal_4b; Formula.Or terminal_disjs] in
+ let disj_vars = FormulaOps.free_vars (Formula.And conjs) in
+ let disj_4b =
+ List.filter (fun a -> List.exists (fun v->List.mem v disj_vars)
+ (FormulaOps.free_vars a)) terminal_4b in
+ lift_universal terminal_uni_vars
+ (disj_4b @ conjs)) terminal_brs in
+ let terminal_phi = Formula.Or terminal_disjs in
(* {{{ log entry *)
if !debug_level > 1 then (
Printf.printf "GDL.translate_game: terminal condition -- %s\n%!"
@@ -2204,22 +2500,18 @@
);
(* }}} *)
(* let loc_toss_rules = *)
- Array.mapi (fun loc rules_brs ->
- List.map (fun (lead, brs) ->
- ignore (terminal_4b, terminal_brs)
-
- ) rules_brs
- ) loc_toss_rules;
-
(* {{{ log entry *)
if !debug_level > 1 then (
Array.iteri (fun loc rules_brs ->
Printf.printf "Rule translations for loc %d:\n%!" loc;
- List.iter (fun ((lead,_,_), (phis,heads,bodies,neg_bodies)) ->
- Printf.printf "Rule-translation: player %s move %s\n%s\n%!"
+ List.iter (fun ((lead,_,_), (rhs_pos,rhs_neg,precond)) ->
+ Printf.printf
+ "Rule-translation: player %s move %s precond:\n%s\naction:\nADD %s... DEL %s\n%!"
(term_str loc_players.(loc)) (term_str lead)
- (rule_pretransl_str (heads,bodies,neg_bodies))
+ (Formula.sprint precond)
+ (String.concat "; " (List.map proto_rel_str rhs_pos))
+ (String.concat "; " (List.map proto_rel_str rhs_neg))
) rules_brs;
) loc_toss_rules;
);
Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli 2011-02-09 03:37:28 UTC (rev 1315)
+++ trunk/Toss/GGP/GDL.mli 2011-02-10 12:16:07 UTC (rev 1316)
@@ -57,8 +57,10 @@
type gdl_rule = gdl_atom * gdl_atom list * gdl_atom list
(** Definition with expanded definitions: expansion of a negated
relation brings negated conjunctions. *)
+type exp_def_branch =
+ term list * gdl_atom list * (Aux.Strings.t * gdl_atom list) list
type exp_def =
- string * (term list * gdl_atom list * gdl_atom list list) list
+ string * exp_def_branch list
val func_graph : string -> term list -> term list list
Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml 2011-02-09 03:37:28 UTC (rev 1315)
+++ trunk/Toss/GGP/GDLTest.ml 2011-02-10 12:16:07 UTC (rev 1316)
@@ -111,5 +111,6 @@
let a () =
GDL.debug_level := 4;
let breakthrough = load_rules "./GGP/examples/breakthrough.gdl" in
- let gdef = GDL.translate_game breakthrough in
+ let connect5 = load_rules "./GGP/examples/connect5.gdl" in
+ let gdef = GDL.translate_game connect5 in
()
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2011-02-09 03:37:28 UTC (rev 1315)
+++ trunk/Toss/Play/GameTest.ml 2011-02-10 12:16:07 UTC (rev 1316)
@@ -863,8 +863,7 @@
\"" 0 in
Game.use_monotonic := false;
hard_case state 0 "should not attack"
- (fun mov_s -> Printf.printf "avoid: %s\n" mov_s;
- "Cross{1:f4}" <> mov_s && "Cross{1:f3}" <> mov_s);
+ (fun mov_s -> "Cross{1:f3}" <> mov_s);
Game.use_monotonic := true;
);
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|