[Toss-devel-svn] SF.net SVN: toss:[1329] trunk/Toss/GGP/GDL.ml
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2011-02-24 17:09:05
|
Revision: 1329 http://toss.svn.sourceforge.net/toss/?rev=1329&view=rev Author: lukstafi Date: 2011-02-24 17:08:59 +0000 (Thu, 24 Feb 2011) Log Message: ----------- GDL translation: remaining uses of expansion of unfixed variables. Modified Paths: -------------- trunk/Toss/GGP/GDL.ml Modified: trunk/Toss/GGP/GDL.ml =================================================================== --- trunk/Toss/GGP/GDL.ml 2011-02-24 02:15:08 UTC (rev 1328) +++ trunk/Toss/GGP/GDL.ml 2011-02-24 17:08:59 UTC (rev 1329) @@ -357,12 +357,11 @@ (7j) Identify variables in "next" & "true" terms that are at-or-below meta-variables in the corresponding mask. (Most of such variables should be already removed as belonging to "frame" - branches.) Expand them by duplicating given branch for all - instantiations (all (5) predicates derived from the considered - position). (Note that since branches do not have unfixed variables - anymore, we do not rename variables during duplication.) + branches.) Such fixed variables should be expanded by duplicating + the whole set of branches together with the "lead legal" term. - Implementation: TODO. + Implementation: TODO; currently, we check for such fixed + variables and fail if they're present. (7k) Replace the "next" and "true" atoms by the conjunction of (4c) and (5) predicates over their corresponding variable. (For @@ -411,7 +410,7 @@ 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. + meta-variables in "terminal" branches, as in (7j). The rewrite rule is generated by joining the derived conjunctions from "next" atoms as RHS, and from bodies as the @@ -1433,7 +1432,76 @@ let mask, _, _, blank = term_to_blank masks term in mask, Formula.fo_var_of_string (String.lowercase (term_to_name blank)) -let translate_branches struc masks static_rnames dyn_rels + +(* Expand branch variables. If [freshen_unfixed=Right fixed], expand + all variables that don't belong to [fixed]. If + [freshen_unfixed=Left freshen], then expand all variables below + meta-variables of masks. If [freshen] is true, rename other + (i.e. non-expanded) variables while duplicating branches. (When + [freshen] is false, all remaining variables should be fixed.) + + With each branch, also return the instantiation used to derive it??? + + As in the expansion of relation definitions, branches are + duplicated for instantiations of positive literals, and + additionally of heads. For instantiations of atoms in negated + subformulas, the subformulas are duplicated within a branch, with + instantiations kept local to the subformula. Final substitution is + re-applied to catch up with later instantiations. *) +let expand_branch_vars masks playout_terms ~freshen_unfixed brs = + let expand sb arg = + let arg = subst sb arg in + let is_inst_var = + match freshen_unfixed with + | Aux.Left _ -> + let mask, sb, m_sb, blank = term_to_blank masks arg in + let ivars = Aux.concat_map (fun (_,t) -> + Aux.Strings.elements (term_vars t)) m_sb in + (fun v -> List.mem v ivars) + | Aux.Right fixed -> fun v -> not (List.mem v fixed) in + Aux.unique_sorted + (Aux.map_try (fun term -> + let sb1, _ = match_meta [] [] [term] [arg] in + let sb1 = List.sort Pervasives.compare + (List.filter (fun (v,_)->is_inst_var v) sb1) in + extend_sb sb1 sb, subst sb1 arg + ) playout_terms) in + let expand_rel atom (sb, acc) = + match atom with + | "true", [arg] -> + List.map (fun (sb,arg) -> sb, ("true",[arg])::acc) (expand sb arg) + | rel, args -> [sb, (rel, List.map (subst sb) args)::acc] in + let expand_neg sb (vs, neg_conj) = + let neg_conjs = + Aux.concat_foldr expand_rel neg_conj [sb, []] in + List.map (fun (sb, neg_conj) -> + let vs = List.filter (fun v -> not (List.mem_assoc v sb)) + (Aux.Strings.elements vs) in + Aux.strings_of_list vs, neg_conj + ) neg_conjs in + let brs = + Aux.concat_map (function ([head],body,neg_body) -> + Aux.concat_map (fun (sb,head) -> + let bodies = Aux.concat_foldr expand_rel body [sb, []] in + Aux.map_some (fun (sb, body) -> + let head = subst sb head in + let body = List.map (subst_rel sb) body in + let neg_body = + Aux.concat_map (expand_neg sb) neg_body in + if List.exists (function _, [] -> true | _ -> false) + neg_body then None + (* need to pack head into a list for [freshen_branch] *) + else Some (sb, ([head], body, neg_body))) bodies) + (if head = Const "_IGNORE_RHS_" then [[], head] + else expand [] head) + | _ -> assert false) brs in + match freshen_unfixed with + | Aux.Left true -> + List.map (fun (sb, br) -> sb, freshen_branch br) brs + | _ -> brs + + +let translate_branches struc masks playout_terms static_rnames dyn_rels (brs : exp_def_branch list) = (* 7i *) let state_terms = @@ -1612,8 +1680,16 @@ Some (all_conjs, (next_arg,body,neg_body))) else None | _ -> assert false) brs in - (* 7j: TODO *) - + (* 7j *) + let check_brs = + expand_branch_vars masks playout_terms + ~freshen_unfixed:(Aux.Left false) + (List.map (fun (_,(head,body,neg_body))-> + [head], body, neg_body) brs) in + if List.exists (fun (sb,_)-> sb <> []) check_brs + then failwith + ("GDL.translate_game: expanding variables resulting in "^ + "duplicating Toss rules not implemented yet"); (* 7k *) let brs = List.map (fun (static_conjs, (next_arg,body,neg_body)) -> @@ -1731,73 +1807,6 @@ (* }}} *) res -(* Expand branch variables. If [freshen_unfixed=Right fixed], expand - all variables that don't belong to [fixed]. If - [freshen_unfixed=Left freshen], then expand all variables below - meta-variables of masks. If [freshen] is true, rename other - (i.e. non-expanded) variables while duplicating branches. (When - [freshen] is false, all remaining variables should be fixed.) - - With each branch, also return the instantiation used to derive it??? - - As in the expansion of relation definitions, branches are - duplicated for instantiations of positive literals, and - additionally of heads. For instantiations of atoms in negated - subformulas, the subformulas are duplicated within a branch, with - instantiations kept local to the subformula. Final substitution is - re-applied to catch up with later instantiations. *) -let expand_branch_vars masks playout_terms ~freshen_unfixed brs = - let expand sb arg = - let arg = subst sb arg in - let is_inst_var = - match freshen_unfixed with - | Aux.Left _ -> - let mask, sb, m_sb, blank = term_to_blank masks arg in - let ivars = Aux.concat_map (fun (_,t) -> - Aux.Strings.elements (term_vars t)) m_sb in - (fun v -> List.mem v ivars) - | Aux.Right fixed -> fun v -> not (List.mem v fixed) in - Aux.unique_sorted - (Aux.map_try (fun term -> - let sb1, _ = match_meta [] [] [term] [arg] in - let sb1 = List.sort Pervasives.compare - (List.filter (fun (v,_)->is_inst_var v) sb1) in - extend_sb sb1 sb, subst sb1 arg - ) playout_terms) in - let expand_rel atom (sb, acc) = - match atom with - | "true", [arg] -> - List.map (fun (sb,arg) -> sb, ("true",[arg])::acc) (expand sb arg) - | rel, args -> [sb, (rel, List.map (subst sb) args)::acc] in - let expand_neg sb (vs, neg_conj) = - let neg_conjs = - Aux.concat_foldr expand_rel neg_conj [sb, []] in - List.map (fun (sb, neg_conj) -> - let vs = List.filter (fun v -> not (List.mem_assoc v sb)) - (Aux.Strings.elements vs) in - Aux.strings_of_list vs, neg_conj - ) neg_conjs in - let brs = - Aux.concat_map (function ([head],body,neg_body) -> - Aux.concat_map (fun (sb,head) -> - let bodies = Aux.concat_foldr expand_rel body [sb, []] in - Aux.map_some (fun (sb, body) -> - let head = subst sb head in - let body = List.map (subst_rel sb) body in - let neg_body = - Aux.concat_map (expand_neg sb) neg_body in - if List.exists (function _, [] -> true | _ -> false) - neg_body then None - (* need to pack head into a list for [freshen_branch] *) - else Some ((* sb, *)([head], body, neg_body))) bodies) - (if head = Const "_IGNORE_RHS_" then [[], head] - else expand [] head) - | _ -> assert false) brs in - match freshen_unfixed with - | Aux.Left true -> - List.map (fun ((* sb, *) br) -> (* sb, *) freshen_branch br) brs - | _ -> brs - let translate_game player_term game_descr = var_support := Aux.Strings.empty; let player_terms = @@ -2401,10 +2410,12 @@ ) frame_brs in let unfixed_brs = to_expand @ more_to_expand in - if unfixed_brs <> [] then failwith - ("GDL.translate_game: parametric non-frame actions "^ - "not implemented yet (7g):\n" ^ - def_str ("action",unfixed_brs)); + (* 7g1 *) + let expanded_brs = + expand_branch_vars masks element_terms + ~freshen_unfixed:(Aux.Right (Aux.Strings.elements fixed_vars)) + unfixed_brs in + let expanded_brs = List.map snd expanded_brs in (* 7f2 *) let leq3 (head1, _, _) (head2, _, _) = try @@ -2525,18 +2536,17 @@ head, Aux.unique_sorted body, Aux.unique_sorted neg_body) erasures) in erasures - (* TODO: (7g) *) + (* TODO: (7g2) *) | _ -> assert false) frames in (* TODO: (7f5) we ignore the possibility that "lead" is instantiated by some of erasure substitutions, since we already ignore non-maximal "legal" classes *) - lead_head, fixed_brs @ erasure_brs + lead_head, fixed_brs @ expanded_brs @ erasure_brs ) rules_brs in (* let rules_inds = Array.of_list rules_brs in *) rules_brs ) joint_legal_branches ) loc_joint_legal in - (* 7g: (7g1) and (7g2) TODO *) (* {{{ log entry *) if !debug_level > 1 then ( Array.iteri (fun loc rules_brs -> @@ -2571,8 +2581,8 @@ [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 + translate_branches struc masks element_terms 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 @@ -2742,8 +2752,10 @@ let terminal_brs = expand_branch_vars masks element_terms ~freshen_unfixed:(Aux.Left true) terminal_brs in + let terminal_brs = List.map snd terminal_brs in let terminal_uni_vars, terminal_4b, terminal_brs = - translate_branches struc masks static_rnames dyn_rels terminal_brs in + translate_branches struc masks element_terms static_rnames + dyn_rels terminal_brs in let terminal_disjs = List.map (fun ((_,_,conjs),_) -> let disj_vars = FormulaOps.free_vars (Formula.And conjs) in let disj_4b = @@ -2793,8 +2805,11 @@ | Const pay -> (try float_of_string pay with _ -> assert false) | _ -> assert false in + (* FIXME: should we expand before, + with [~freshen_unfixed:(Aux.Left true)]? *) let goal_uni_vars, goal_4b, brs = - translate_branches struc masks static_rnames dyn_rels brs in + translate_branches struc masks element_terms static_rnames + dyn_rels brs in let goal_disjs = List.map (fun ((_,_,conjs),_) -> let disj_vars = FormulaOps.free_vars (Formula.And conjs) in let disj_4b = This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |