[Toss-devel-svn] SF.net SVN: toss:[1310] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1310] trunk/Toss
|
From: <luk...@us...> - 2011-02-04 15:23:21
|
Revision: 1310
http://toss.svn.sourceforge.net/toss/?rev=1310&view=rev
Author: lukstafi
Date: 2011-02-04 15:23:14 +0000 (Fri, 04 Feb 2011)
Log Message:
-----------
GDL: progress (refactoring, terminal condition). Game: Reverting to payoff-scaled values in terminal nodes of alpha-beta.
Modified Paths:
--------------
trunk/Toss/GGP/GDL.ml
trunk/Toss/Play/Game.ml
trunk/Toss/Play/GameTest.ml
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-02-03 20:36:45 UTC (rev 1309)
+++ trunk/Toss/GGP/GDL.ml 2011-02-04 15:23:14 UTC (rev 1310)
@@ -284,10 +284,10 @@
(7h) Introduce a new element variable for each class of "next" and
"true" terms equal modulo mask (i.e. there is a mask matching them
and they differ only at-or-below metavariables). (Remember the
- atoms "corresponding variable".) From now on until (7m1) we keep
+ atoms "corresponding variable".) From now on until (7l1) we keep
both the (partially) Toss-translated versions and the (complete)
GDL-originals of branches (so to use GDL atoms for "subsumption
- checking" in (7m)).
+ checking" in (7l)).
(7i-4a) For all subterms of "next" and "true" atoms, identify the
sets of <mask-path, element variable> they "inhabit". Replace a
@@ -349,8 +349,8 @@
associated with every bit. The unique resulting sets are exactly
the Toss rules precursors.
- (7m) Filter the final rule candidates by satisfiability in at
- least one of aggregate playout states.
+ (7m) Filter the final rule candidates by satisfiability of the
+ static part (same as (7i1) conjoined).
(7n) Include translated negation of the terminal condition. (Now we
build rewrite rules for a refinement of an equivalence class of
@@ -363,6 +363,10 @@
precondition. Exactly the RHS variables are listed in the LHS
(other variables are existentially closed in the precondition).
+ (7o) After the rules are translated, perform an aggregated playout
+ of the Toss variant of the game. Remove the rules that were never
+ applied.
+
(8) We use a single payoff matrix for all locations. Goal patterns
are expanded to regular goals by instantiating the value variable
by all values in its domain (for example, as gathered from the
@@ -1116,6 +1120,290 @@
(term_str a) (term_str b);
assert false
+let triang_matrix elems =
+ let rec aux acc = function
+ | [] -> acc
+ | hd::tl -> aux (List.map (fun e->[|hd; e|]) tl @ acc) tl in
+ aux [] elems
+
+let term_to_blank masks next_arg =
+ let mask_cands =
+ Aux.map_try (fun mask ->
+ mask, match_meta [] [] [next_arg] [mask]
+ ) masks in
+ let mask, sb, m_sb = match mask_cands with
+ | [mask, (sb, m_sb)] -> mask, sb, m_sb
+ | _ -> assert false in
+ mask, sb, m_sb, blank_out (next_arg, mask)
+
+let toss_var masks term =
+ 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 =
+ (* 7i *)
+ (* Do not flatten the already built super-partition. *)
+ let state_terms =
+ List.fold_left (fun acc -> function
+ | [next_arg], body, neg_body ->
+ let res =
+ List.fold_left (fun acc -> function
+ | "true", [true_arg] -> Terms.add true_arg acc
+ | "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_"
+ then res
+ else Terms.add next_arg res
+ | _ -> assert false
+ ) Terms.empty brs in
+ let state_terms = Terms.elements state_terms in
+ (* {{{ log entry *)
+ if !debug_level > 2 then (
+ Printf.printf "state_terms: %s\n%!" (
+ String.concat ", " (List.map term_str state_terms))
+ );
+ (* }}} *)
+ let state_subterms =
+ Aux.concat_map (fun term ->
+ let mask, sb, m_sb, blanked = term_to_blank masks term in
+ List.map (fun (v,t) -> t, (mask, v, term)) sb
+ ) state_terms in
+ let conjs_4a rel args =
+ let ptups = List.map (fun arg ->
+ Aux.assoc_all arg state_subterms) args in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "conjs_4a: of %s = subterms %s\n%!"
+ (fact_str (rel,args)) (String.concat "; " (
+ List.map (fun l -> String.concat ", "
+ (List.map (fun (_,_,term)->term_str term) l)) ptups))
+ );
+ (* }}} *)
+ let ptups = Aux.product ptups in
+ let res =
+ List.map (fun ptup ->
+ let rname = rel ^ "__" ^ String.concat "__"
+ (List.map (fun (mask,v,_)->
+ term_to_name mask ^ "_" ^ v) ptup) in
+ let tup = List.map (fun (_,_,term) ->
+ snd (toss_var masks term)) ptup in
+ Formula.Rel (rname, Array.of_list tup)) ptups in
+ let res = Aux.unique_sorted res in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "conjs_4a: of %s = %s\n%!"
+ (fact_str (rel,args)) (Formula.str (Formula.And res))
+ );
+ (* }}} *)
+ res in
+ (* 7i-4b *)
+ let path_subterms =
+ Aux.concat_map (fun term ->
+ let mask, sb, m_sb, blanked = term_to_blank masks term in
+ Aux.map_some (function
+ | v, Var t -> Some ((mask, v), (t, term))
+ | _ -> None) sb
+ ) state_terms in
+ let path_subterms = Aux.collect path_subterms in
+ let conjs_4b =
+ Aux.concat_map (fun ((mask, v), terms) ->
+ let rname = "EQ___" ^ term_to_name mask ^ "_" ^ v in
+ let terms = Aux.collect terms in
+ Aux.concat_map (fun (_,terms) ->
+ let vars = List.map (fun t -> snd (toss_var masks t)) terms in
+ let tups = triang_matrix (Aux.unique_sorted vars) in
+ List.map (fun tup -> Formula.Rel (rname, tup)) tups
+ ) terms
+ ) path_subterms in
+ let conjs_4b = Aux.unique_sorted conjs_4b in
+ let brs = Aux.map_some (function
+ | [next_arg],body,neg_body ->
+ let phi, lvars =
+ if next_arg = Const "_TERMINAL_" then [], ref []
+ else
+ let mask, sb, m_sb, blanked = term_to_blank masks next_arg in
+ let rname = term_to_name mask in
+ let _, svar = toss_var masks next_arg in
+ let phi = Formula.Rel (rname, [|svar|]) in
+ let lvars = ref [svar] in
+ [phi], lvars in
+ let conjs =
+ Aux.concat_map (fun (rel, args) ->
+ if rel = "true" then
+ (* 7i-4c *)
+ 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
+ lvars := svar :: !lvars;
+ 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
+ phi::conjs
+ else if List.mem rel static_rnames then
+ (* 7i-4a *)
+ conjs_4a rel args
+ else []
+ ) body in
+ 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 conjs)]
+ *)
+ else if List.mem rel static_rnames then
+ (* 7i-4a *)
+ List.map (fun c -> Formula.Not c) (conjs_4a rel args)
+ else []
+ )) 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
+ let optim_conjs = List.filter (fun c->
+ List.for_all (fun v->List.mem v lvars)
+ (FormulaOps.free_vars c)) (conjs_4b @ all_conjs) in
+ let rphi = Solver.M.register_formula
+ (Formula.And optim_conjs) in
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ (* do not print, because it generates too many
+ answers -- too little constraints per number of
+ variables when considering a single branch *)
+ (*
+ let assgn = Solver.M.evaluate struc rphi in
+ let avars = List.map Formula.var_str
+ (FormulaOps.free_vars phi) in
+ let atups =
+ AssignmentSet.tuples struc.Structure.elements
+ avars assgn in *)
+ Printf.printf "evaluating: %s -- simpl %s\n%!"
+ (Formula.str phi)
+ (Solver.M.formula_str rphi)
+ (* (List.length atups) *)
+ );
+ (* }}} *)
+ if Solver.M.check_formula struc rphi
+ then (
+ (* {{{ log entry *)
+ if !debug_level > 3 then (
+ Printf.printf "holds\n%!"
+ );
+ (* }}} *)
+ Some (all_conjs, (next_arg,body,neg_body)))
+ else None
+ | _ -> assert false) brs in
+ (* 7j: TODO *)
+
+ (* 7k *)
+ 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 [], []
+ else
+ let mask, sb, m_sb, blanked = term_to_blank masks next_arg in
+ let rhs_elem = term_to_name blanked in
+ Aux.partition_map (fun (v,t as v_sb) ->
+ if t = Const "_BLANK_" then
+ let neg_rels = List.assoc (mask, v) dyn_rels in
+ Aux.Right (List.map (fun rel->rel, [|rhs_elem|]) neg_rels)
+ else
+ let rname = term_to_name (subst_one v_sb mask) in
+ Aux.Left (rname, [|rhs_elem|])
+ ) m_sb in
+ let rhs_possneg_preds = List.flatten rhs_possneg_preds in
+ let dyn_conjs =
+ Aux.concat_map (fun (rel, args) ->
+ if rel = "true" then
+ (* 7i-4c *)
+ let true_arg = List.hd args in
+ let mask, sb, m_sb, blanked = term_to_blank masks true_arg in
+ let _, svar = toss_var masks true_arg in
+
+ let lhs_pos_preds, lhs_possneg_preds =
+ Aux.partition_map (fun (v,t as v_sb) ->
+ if t = Const "_BLANK_" then
+ (*
+ let neg_rels = List.assoc (mask, v) dyn_rels in
+ Aux.Right (List.map (fun rel->
+ Formula.Rel (rel, [|svar|])) neg_rels)
+ *) assert false
+ else
+ let rname = term_to_name (subst_one v_sb mask) in
+ Aux.Left (Formula.Rel (rname, [|svar|]))
+ ) m_sb in
+ (*
+ let lhs_possneg_preds = List.flatten lhs_possneg_preds in
+ *)
+ lhs_pos_preds
+ else if List.mem rel static_rnames
+ then []
+ else (
+ Printf.printf "\nunexpected_dynamic: %s\n%!" rel;
+ (* dynamic relations have been expanded *)
+ 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
+
+ (* 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
+ 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
+
let translate_game game_descr =
freshen_count := 0;
let player_terms =
@@ -1239,6 +1527,7 @@
(* 3 *)
let legal_rules = List.assoc "legal" exp_defs in
let next_rules = List.assoc "next" exp_defs in
+ let terminal_rules = List.assoc "terminal" exp_defs in
(* 3b *)
let exp_next =
Aux.concat_map (subst_def_branch ["does", legal_rules]) next_rules in
@@ -1462,27 +1751,21 @@
) struc elements in
(* 5 *)
- let term_to_blank next_arg =
- let mask_cands =
- Aux.map_try (fun mask ->
- mask, match_meta [] [] [next_arg] [mask]
- ) masks in
- let mask, sb, m_sb = match mask_cands with
- | [mask, (sb, m_sb)] -> mask, sb, m_sb
- | _ -> assert false in
- mask, sb, m_sb, blank_out (next_arg, mask) in
- let struc = List.fold_left (fun struc term ->
- let mask, sb, m_sb, blanked = term_to_blank term in
+ let dyn_rels, struc = List.fold_left (fun (dyn_rels, struc) term ->
+ let mask, sb, m_sb, blanked = term_to_blank masks term in
let e =
let elems = List.assoc mask elements in
List.assoc sb elems in
- List.fold_left (fun struc (v,t as v_sb) ->
+ List.fold_left (fun (dyn_rels, struc) (v,t as v_sb) ->
let rname = term_to_name (subst_one v_sb mask) in
+ ((mask, v), rname)::dyn_rels,
if List.mem term init_state then
Structure.add_rel struc rname [|e|]
- else Structure.add_rel_name rname 1 struc) struc m_sb
- ) struc element_terms in
-
+ else Structure.add_rel_name rname 1 struc) (dyn_rels, struc) m_sb
+ ) ([], struc) element_terms in
+ let dyn_rels =
+ List.map (fun (path, subts) -> path, Aux.unique_sorted subts)
+ (Aux.collect dyn_rels) in
(* 7a *)
let legal_rules =
Aux.concat_map (function [Const _; _], _, _ as lrule -> [lrule]
@@ -1670,7 +1953,7 @@
let erasure_brs = Aux.concat_map
(function
| [next_arg] as next_args,multi_body ->
- let mask, _, _, blank_arg = term_to_blank next_arg in
+ let mask, _, _, blank_arg = term_to_blank masks next_arg in
(* {{{ log entry *)
if !debug_level > 2 then (
Printf.printf "Blanking-out of %s by %s\n%!"
@@ -1776,171 +2059,14 @@
) loc_next_classes;
);
(* }}} *)
+ let static_rnames = List.map (fun ((srel,_),_,_) -> srel) static_rules in
(* 7h *)
- let toss_var term =
- let mask, _, _, blank = term_to_blank term in
- mask, Formula.fo_var_of_string (term_to_name blank) in
let loc_toss_rules =
Array.mapi (fun loc rules_brs ->
Aux.concat_map (fun (lead, brs) ->
- (* 7i *)
- (* Do not flatten the already built super-partition. *)
- let state_terms =
- List.fold_left (fun acc -> function
- | [next_arg], body, neg_body ->
- let res =
- List.fold_left (fun acc -> function
- | "true", [true_arg] -> Terms.add true_arg acc
- | "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
- Terms.add next_arg res
- | _ -> assert false
- ) Terms.empty brs in
- let state_terms = Terms.elements state_terms in
- (* {{{ log entry *)
- if !debug_level > 2 then (
- Printf.printf "state_terms: %s\n%!" (
- String.concat ", " (List.map term_str state_terms))
- );
- (* }}} *)
- let state_subterms =
- Aux.concat_map (fun term ->
- let mask, sb, m_sb, blanked = term_to_blank term in
- List.map (fun (v,t) -> t, (mask, v, term)) sb
- ) state_terms in
- let conjs_4a rel args =
- let ptups = List.map (fun arg ->
- Aux.assoc_all arg state_subterms) args in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "conjs_4a: of %s = subterms %s\n%!"
- (fact_str (rel,args)) (String.concat "; " (
- List.map (fun l -> String.concat ", "
- (List.map (fun (_,_,term)->term_str term) l)) ptups))
- );
- (* }}} *)
- let ptups = Aux.product ptups in
- let res =
- List.map (fun ptup ->
- let rname = rel ^ "__" ^ String.concat "__"
- (List.map (fun (mask,v,_)->
- term_to_name mask ^ "_" ^ v) ptup) in
- let tup = List.map (fun (_,_,term) ->
- snd (toss_var term)) ptup in
- Formula.Rel (rname, Array.of_list tup)) ptups in
- let res = Aux.unique_sorted res in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "conjs_4a: of %s = %s\n%!"
- (fact_str (rel,args)) (Formula.str (Formula.And res))
- );
- (* }}} *)
- res in
- let brs = Aux.map_some (function
- | [next_arg],body,neg_body ->
- let mask, sb, m_sb, blanked = term_to_blank next_arg in
- let rname = term_to_name mask in
- let _, svar = toss_var next_arg in
- let phi = Formula.Rel (rname, [|svar|]) in
- let lvars = ref [svar] in
- let conjs =
- Aux.concat_map (fun (rel, args) ->
- if rel = "true" then
- (* 7i-4c *)
- let true_arg = List.hd args in
- let mask, sb, m_sb, blanked = term_to_blank true_arg in
- let rname = term_to_name mask in
- let _, svar = toss_var true_arg in
- lvars := svar :: !lvars;
- 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
- phi::conjs
- else if List.exists (fun ((srel,_),_,_) -> rel=srel)
- static_rules then
- (* 7i-4a *)
- conjs_4a rel args
- else
- (* TODO: 7i-4b *)
- []
- ) body in
- 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 true_arg in
- let rname = term_to_name mask in
- let _, svar = toss_var 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 conjs)]
- *)
- else if List.exists (fun ((srel,_),_,_) -> rel=srel)
- static_rules then
- (* 7i-4a *)
- List.map (fun c -> Formula.Not c) (conjs_4a rel args)
- else
- (* TODO: 7i-4b *)
- []
- )) 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
- let optim_conjs = List.filter (fun c->
- List.for_all (fun v->List.mem v lvars)
- (FormulaOps.free_vars c)) all_conjs in
- let rphi = Solver.M.register_formula
- (Formula.And optim_conjs) in
- (* {{{ log entry *)
- if !debug_level > 3 then (
- (* do not print, because it generates too many
- answers -- too little constraints per number of
- variables when considering a single branch *)
- (*
- let assgn = Solver.M.evaluate struc rphi in
- let avars = List.map Formula.var_str
- (FormulaOps.free_vars phi) in
- let atups =
- AssignmentSet.tuples struc.Structure.elements
- avars assgn in *)
- Printf.printf "evaluating: %s -- simpl %s\n%!"
- (Formula.str phi)
- (Solver.M.formula_str rphi)
- (* (List.length atups) *)
- );
- (* }}} *)
- if Solver.M.check_formula struc rphi
- then (
- (* {{{ log entry *)
- if !debug_level > 3 then (
- Printf.printf "holds\n%!"
- );
- (* }}} *)
- Some (phi, (next_arg,body,neg_body)))
- else None
- | _ -> assert false) brs in
- (* 7j: TODO *)
- (* 7k: TODO *)
+ let conjs_4b, brs =
+ translate_branches struc masks static_rnames dyn_rels brs in
+
(* 7l *)
let atoms =
List.fold_left (fun acc (_,(_,body,neg_body))->
@@ -1948,13 +2074,10 @@
(List.fold_right (List.fold_right Atoms.add)
neg_body acc)
) Atoms.empty brs in
- Printf.printf "\na\n%!";
let atoms = Atoms.elements atoms in
- Printf.printf "\nb\n%!";
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
- Printf.printf "\nc\n%!";
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
@@ -1970,42 +2093,44 @@
[Aux.Ints.diff full_set (Aux.ints_of_list negatives);
Aux.Ints.diff full_set (Aux.ints_of_list positives)]
) atoms in
- Printf.printf "\ne\n%!";
let cases = Aux.product table in
- Printf.printf "\nf\n%!";
let cases =
List.map (List.fold_left Aux.Ints.inter full_set) cases in
- Printf.printf "\ng\n%!";
let cases =
Aux.unique_sorted (List.map Aux.Ints.elements cases) in
- Printf.printf "\nh\n%!";
let cases = List.map (fun c_brs ->
let c_brs = List.map (Array.get brs) c_brs in
- List.fold_left (fun (phis,heads,bodies,neg_bodies)
- (phi,(head,body,neg_body)) ->
- phi::phis,head::heads,body@bodies,neg_body@neg_bodies)
- ([],[],[],[]) c_brs
+ List.fold_left (fun
+ ((rhs_pos_acc, rhs_neg_acc, static_conjs_acc, conjs_acc),
+ heads, bodies, neg_bodies)
+ ((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
) cases in
- Printf.printf "\ni\n%!";
- let cases = List.filter (fun (phis,heads,bodies,neg_bodies) ->
- let phi = Formula.And phis in
+ (* 7m *)
+ let cases = List.filter (fun ((_,_,static_phis,_),
+ heads,bodies,neg_bodies) ->
+ let phi = Formula.And static_phis in
let rphi = Solver.M.register_formula phi in
- (* {{{ log entry *)
+ (* {{{ log entry *)
if !debug_level > 3 then (
- (* do not print, because it generates too many
- answers -- too little constraints per number of
- variables when considering a single branch *)
- (*
- let assgn = Solver.M.evaluate struc rphi in
- let avars = List.map Formula.var_str
- (FormulaOps.free_vars phi) in
- let atups =
- AssignmentSet.tuples struc.Structure.elements
- avars assgn in *)
+ (* do not print, because it generates too many
+ answers -- too little constraints per number of
+ variables when considering a single branch *)
+ (*
+ let assgn = Solver.M.evaluate struc rphi in
+ let avars = List.map Formula.var_str
+ (FormulaOps.free_vars phi) in
+ let atups =
+ AssignmentSet.tuples struc.Structure.elements
+ avars assgn in *)
Printf.printf "evaluating: %s -- simpl %s\n%!"
(Formula.str phi)
(Solver.M.formula_str rphi)
- (* (List.length atups) *)
+ (* (List.length atups) *)
);
(* }}} *)
let res = Solver.M.check_formula struc rphi in
@@ -2015,11 +2140,27 @@
);
(* }}} *)
res) cases in
- Printf.printf "\nj\n%!";
List.map (fun case -> lead, case) cases
) rules_brs
) loc_next_classes in
- (* {{{ log entry *)
+ (* 7n *)
+ let terminal_brs =
+ List.map (function
+ | [], body, neg_body -> [Const "_TERMINAL_"], body, neg_body
+ | _ -> assert false) terminal_rules in
+ let terminal_4b, terminal_brs =
+ translate_branches struc masks static_rnames dyn_rels terminal_brs in
+
+ (* 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;
@@ -2106,6 +2247,7 @@
effort, horizon, heur_adv_ratio
let initialize_game state player game_descr startcl =
+ translate_game game_descr;
if (Some game_descr) = !tictactoe_descr then manual_game := "tictactoe";
if (Some game_descr) = !breakthrough_descr then manual_game := "breakthrough";
if (Some game_descr) = !connect5_descr then manual_game := "connect5";
Modified: trunk/Toss/Play/Game.ml
===================================================================
--- trunk/Toss/Play/Game.ml 2011-02-03 20:36:45 UTC (rev 1309)
+++ trunk/Toss/Play/Game.ml 2011-02-04 15:23:14 UTC (rev 1310)
@@ -781,14 +781,14 @@
gen_moves grid_size rules model location in
if moves = [| |] then (* terminal position *)
let res =
- (* *
+ (* *)
Array.map (fun expr ->
100000. *.
Solver.M.get_real_val expr model)
location.Arena.payoffs_pp (* see [let payoff] above *)
- * *)
+ (* *
play_evgame grid_size model time subgames.(loc)
- (* *)
+ * *)
in
(* {{{ log entry *)
if !debug_level > 4 then (
@@ -808,14 +808,14 @@
else if n = 0 then begin (* terminal after postconditions *)
let res =
(* play_evgame grid_size model time subgames.(loc) *)
- (* *
+ (* *)
Array.map (fun expr ->
100000. *.
Solver.M.get_real_val expr model)
location.Arena.payoffs_pp
- * *)
+ (* *
play_evgame grid_size model time subgames.(loc)
- (* *)
+ * *)
in
(* {{{ log entry *)
if !debug_level > 4 then (
Modified: trunk/Toss/Play/GameTest.ml
===================================================================
--- trunk/Toss/Play/GameTest.ml 2011-02-03 20:36:45 UTC (rev 1309)
+++ trunk/Toss/Play/GameTest.ml 2011-02-04 15:23:14 UTC (rev 1310)
@@ -131,7 +131,7 @@
lazy (None, 4.0, state_of_file "./examples/Gomoku19x19.toss")
let connect4_game =
- lazy (None, 6.0, state_of_file "./examples/Connect4.toss")
+ lazy (None, 2.0, state_of_file "./examples/Connect4.toss")
let chess_game =
lazy (Some 400, 2.0, state_of_file "./examples/Chess.toss")
@@ -843,7 +843,32 @@
Game.use_monotonic := true;
);
+ "connect4 avoid losing" >::
+ (fun () ->
+ let state = update_game connect4_game
+"[ | |
+ ] \"
+ ... ... ...
+ ... ... ...
+ ... ... ... ...
+ ... ... ... ...
+ ... ... ...
+ ... Q..Q ...
+ ... ... ... ...
+ ... ...P Q.. ...
+ ... ... ...
+ ... Q..P P..
+ ... ... ... ...
+ ... Q..P P..P Q..
+\"" 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);
+ Game.use_monotonic := true;
+);
+
"connect4 endgame" >::
(fun () ->
let state = update_game connect4_game
@@ -933,7 +958,7 @@
let a () =
match test_filter
- ["Game:2:alpha_beta_ord-time 8 16 32:15:connect4 simple"]
+ ["Game:2:alpha_beta_ord-time 8 16 32:16:connect4 avoid losing"]
tests
with
| Some tests -> ignore (run_test_tt ~verbose:true tests)
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
