[Toss-devel-svn] SF.net SVN: toss:[1313] trunk/Toss/GGP/GDL.ml
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2011-02-05 16:36:23
|
Revision: 1313 http://toss.svn.sourceforge.net/toss/?rev=1313&view=rev Author: lukstafi Date: 2011-02-05 16:36:17 +0000 (Sat, 05 Feb 2011) Log Message: ----------- GDL: Correcting a stupid addition. GDL translation further progress. Modified Paths: -------------- trunk/Toss/GGP/GDL.ml Modified: trunk/Toss/GGP/GDL.ml =================================================================== --- trunk/Toss/GGP/GDL.ml 2011-02-05 16:14:05 UTC (rev 1312) +++ trunk/Toss/GGP/GDL.ml 2011-02-05 16:36:17 UTC (rev 1313) @@ -151,7 +151,7 @@ but do not contain ground facts, by duplicating the branch in which body an atom of the relation occurs, for each branch of the relation definition, unifying and applying the unifier. (If the - duplication turns out prohibitive, this will be a *huge* TODO for + duplication turns out prohibitive, this will be a huge TODO for this translation framework.) (6a) The definition: @@ -160,14 +160,16 @@ provides a DNF defining formula (using negation-as-failure): - [(r, args) <=> exist vars1 (args = params1 /\ body1) \/ ... - \/ exist vars_n (args = params_n /\ body_n)] + [(r, args) <=> exist vars1 (params1 = args /\ body1) \/ ... + \/ exist vars_n (params_n = args /\ body_n)] which expands in a natural way for positive occurrences. We duplicate the branch where [(r, args)] is substitued for each - disjunct and apply the unifier of [args = params_i] in the whole - [i]th cloned branch. We freshen each [vars_i] to avoid capture. If - unification fails, we drop the corresponding branch clone. + disjunct and apply the unifier of [params_i = args] in the whole + [i]th cloned branch, eliminating the [params] (rather than the + [args]) when possible. We freshen each [vars_i] to avoid + capture. If unification fails, we drop the corresponding branch + clone. (6b) For negative occurrences we transform the defining formula to: @@ -184,12 +186,14 @@ (and (...(r args)...))]) into the conjunction of negations, with no branch duplication (in general, duplicating the negated subformula inside a branch). We only apply the unifier of [args = - params_i] to [body_i] (in general, the whole negated - subformula). Still, we freshen each [vars_i] to avoid capture. 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. + params_i] to [body_i] (in general, the whole negated subformula), + 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. (6b1) The general case is not implemented yet since it slightly complicates the code, and expressivity gain is very small. @@ -565,8 +569,26 @@ (if def then body @ List.concat neg_body else List.concat neg_body)) branches) defs with - | [], [] -> List.rev strata - | stratum, [] -> List.rev (stratum::strata) + | [], [] -> + (* {{{ log entry *) + if !debug_level > 3 then ( + Printf.printf "stratify: %d strata -- %s\n%!" + (List.length strata) (String.concat "; " (List.map (fun l -> + String.concat ", " (List.map fst l)) (List.rev strata))) + ); + (* }}} *) + List.rev strata + | stratum, [] -> + (* {{{ log entry *) + if !debug_level > 3 then ( + Printf.printf "stratify: %d strata -- %s\n%!" + (List.length (stratum::strata)) (String.concat "; " ( + List.map (fun l -> + String.concat ", " (List.map fst l)) + (List.rev (stratum::strata)))) + ); + (* }}} *) + List.rev (stratum::strata) | [], _ -> if def then raise (Lexer.Parsing_error @@ -574,7 +596,16 @@ else raise (Lexer.Parsing_error "GDL.stratify: cyclic negation dependency") - | stratum, rules -> stratify (stratum::strata) rules + | stratum, rules -> + if not def then + let stratum, more_rules = List.partition (fun (_, branches) -> + List.for_all (fun (_, body, neg_body) -> + List.for_all (fun (rel1,_) -> + rel1 = "distinct" || rel1 = "true" || rel1 = "does" || + not (List.mem_assoc rel1 rules)) + body) branches) stratum in + stratify ~def (stratum::strata) (more_rules @ rules) + else stratify ~def (stratum::strata) rules let rec subst_one (x, term as sb) = function @@ -864,7 +895,7 @@ let subst_def_branch (defs : exp_def list) (head, body, neg_body as br : exp_def_branch) : exp_def_branch list = (* {{{ log entry *) - if !debug_level > 3 then ( + if !debug_level > 4 then ( Printf.printf "Expanding branch %s\n%!" (def_str ("BRANCH", [br])); ); (* }}} *) @@ -874,7 +905,7 @@ (let try def = freshen_def_branches (List.assoc rel defs) in (* {{{ log entry *) - if !debug_level > 3 then ( + if !debug_level > 4 then ( Printf.printf "Expanding positive %s by %s\n%!" rel (def_str (rel, def)) ); @@ -930,9 +961,21 @@ let rec loop base = function | [] -> base | stratum::strata -> + (* {{{ log entry *) + if !debug_level > 3 then ( + Printf.printf "expand_def_rules: step base rels = %s\n%!" + (String.concat ", " (List.map fst base)) + ); + (* }}} *) let step = List.map (fun (rel, branches) -> rel, Aux.concat_map (subst_def_branch (more_defs@base)) branches) stratum in + (* {{{ log entry *) +if !debug_level > 3 then ( + Printf.printf "expand_def_rules: step result = %s\nexpand_def_rules: end step\n%!" + (String.concat "\n" (List.map def_str step)) +); +(* }}} *) loop (base @ step) strata in match stratify ~def:true [] (defs_of_rules rules) with | [] -> [] @@ -1274,11 +1317,13 @@ 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)] + [phi; Formula.Not (Formula.And/Or conjs)] *) else if List.mem rel static_rnames then (* 7i-4a *) + (* FIXME: And / Or semantics? *) List.map (fun c -> Formula.Not c) (conjs_4a rel args) + (* [Formula.Not (Formula.And (conjs_4a rel args))] *) else [] )) neg_body in let all_conjs = phi @ conjs @ neg_conjs in @@ -1290,7 +1335,7 @@ let rphi = Solver.M.register_formula (Formula.And optim_conjs) in (* {{{ log entry *) - if !debug_level > 3 then ( + if !debug_level > 4 then ( (* do not print, because it generates too many answers -- too little constraints per number of variables when considering a single branch *) @@ -1301,9 +1346,8 @@ let atups = AssignmentSet.tuples struc.Structure.elements avars assgn in *) - Printf.printf "evaluating: %s -- simpl %s\n%!" + Printf.printf "evaluating: %s\n%!" (Formula.str phi) - (Solver.M.formula_str rphi) (* (List.length atups) *) ); (* }}} *) @@ -2116,7 +2160,7 @@ let phi = Formula.And static_phis in let rphi = Solver.M.register_formula phi in (* {{{ log entry *) - if !debug_level > 3 then ( + if !debug_level > 4 then ( (* do not print, because it generates too many answers -- too little constraints per number of variables when considering a single branch *) @@ -2127,9 +2171,8 @@ let atups = AssignmentSet.tuples struc.Structure.elements avars assgn in *) - Printf.printf "evaluating: %s -- simpl %s\n%!" + Printf.printf "evaluating: %s\n%!" (Formula.str phi) - (Solver.M.formula_str rphi) (* (List.length atups) *) ); (* }}} *) @@ -2150,7 +2193,16 @@ | _ -> assert false) terminal_rules in let terminal_4b, terminal_brs = translate_branches struc masks static_rnames dyn_rels terminal_brs in - + 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 + (* {{{ log entry *) + if !debug_level > 1 then ( + Printf.printf "GDL.translate_game: terminal condition -- %s\n%!" + (Formula.sprint terminal_phi) + ); + (* }}} *) (* let loc_toss_rules = *) Array.mapi (fun loc rules_brs -> List.map (fun (lead, brs) -> @@ -2160,7 +2212,7 @@ ) rules_brs ) loc_toss_rules; - (* {{{ log entry *) + (* {{{ log entry *) if !debug_level > 1 then ( Array.iteri (fun loc rules_brs -> Printf.printf "Rule translations for loc %d:\n%!" loc; @@ -2247,7 +2299,6 @@ 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"; This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |