[Toss-devel-svn] SF.net SVN: toss:[1507] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2011-07-09 10:28:24
|
Revision: 1507 http://toss.svn.sourceforge.net/toss/?rev=1507&view=rev Author: lukstafi Date: 2011-07-09 10:28:17 +0000 (Sat, 09 Jul 2011) Log Message: ----------- Reimplementation of GDL to Toss translation: untested work in progress. Modified Paths: -------------- trunk/Toss/Formula/Aux.ml trunk/Toss/Formula/Aux.mli trunk/Toss/Formula/AuxTest.ml trunk/Toss/GGP/GDL.ml trunk/Toss/GGP/GDL.mli trunk/Toss/GGP/GDLParser.mly trunk/Toss/GGP/Translate.ml trunk/Toss/Solver/Structure.ml trunk/Toss/Solver/Structure.mli trunk/Toss/www/reference/reference.tex Modified: trunk/Toss/Formula/Aux.ml =================================================================== --- trunk/Toss/Formula/Aux.ml 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/Formula/Aux.ml 2011-07-09 10:28:17 UTC (rev 1507) @@ -204,10 +204,14 @@ | hd::tl -> List.rev_append (List.map (fun e-> hd, e) tl) (pairs tl) -let all_tuples_for args elems = - List.fold_left (fun tups _ -> +let rec fold_n f accu n = + if n <= 0 then accu + else fold_n f (f accu) (n-1) + +let all_ntuples elems arity = + fold_n (fun tups -> concat_map (fun e -> (List.map (fun tup -> e::tup) tups)) - elems) [[]] args + elems) [[]] arity let rec remove_one e = function | hd::tl when hd = e -> tl @@ -486,11 +490,7 @@ | hd::tl -> aux (List.map (fun e->[e]) hd) tl -let rec fold_n f accu n = - if n <= 0 then accu - else fold_n f (f accu) (n-1) - (* Character classes. *) let is_uppercase c = c >= 'A' && c <= 'Z' let is_lowercase c = c >= 'a' && c <= 'z' Modified: trunk/Toss/Formula/Aux.mli =================================================================== --- trunk/Toss/Formula/Aux.mli 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/Formula/Aux.mli 2011-07-09 10:28:17 UTC (rev 1507) @@ -132,9 +132,8 @@ elements from the list. *) val pairs : 'a list -> ('a * 'a) list -(** An [n]th cartesian power of the second list, where [n] is the - length of the first list. Tail recursive. *) -val all_tuples_for : 'a list -> 'b list -> 'b list list +(** An [n]th cartesian power of the list. Tail recursive. *) +val all_ntuples : 'a list -> int -> 'a list list (** Remove an occurrence of a value (uses structural equality). *) val remove_one : 'a -> 'a list -> 'a list Modified: trunk/Toss/Formula/AuxTest.ml =================================================================== --- trunk/Toss/Formula/AuxTest.ml 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/Formula/AuxTest.ml 2011-07-09 10:28:17 UTC (rev 1507) @@ -140,7 +140,7 @@ (Aux.map_try f [`A;`B;`C;`D]); ); - "product, all_tuples_for, concat_foldr" >:: + "product, all_ntuples, concat_foldr" >:: (fun () -> let print_llist l = String.concat "; " (List.map (String.concat ", ") l) in @@ -154,11 +154,11 @@ assert_equal ~printer:print_llist [["a"; "a"]; ["a"; "b"]; ["a"; "c"]; ["b"; "a"]; ["b"; "b"]; ["b"; "c"]; ["c"; "a"]; ["c"; "b"]; ["c"; "c"]] - (Aux.all_tuples_for [();()] ["a";"b";"c"]); + (Aux.all_ntuples ["a";"b";"c"] 2); assert_equal ~printer:print_llist [["a"; "a"; "a"]; ["a"; "a"; "b"]; ["a"; "b"; "a"]; ["a"; "b"; "b"]; ["b"; "a"; "a"]; ["b"; "a"; "b"]; ["b"; "b"; "a"]; ["b"; "b"; "b"]] - (Aux.all_tuples_for [();(); ()] ["a";"b"]); + (Aux.all_ntuples ["a";"b"] 3); assert_equal ~printer:print_llist [["a1"; "b"; "c"; "a1"; "d"]; ["a2"; "b"; "c"; "a1"; "d"]; Modified: trunk/Toss/GGP/GDL.ml =================================================================== --- trunk/Toss/GGP/GDL.ml 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/GGP/GDL.ml 2011-07-09 10:28:17 UTC (rev 1507) @@ -1,33 +1,40 @@ (** {2 Game Description Language.} - Type definitions, helper functions, game specification. *) + Type definitions, operations on terms, saturation (i.e. Herbrand + model), clause inlining. *) + +(* ************************************************************ *) +(* ************************************************************ *) +(** {3 Datalog programs: Type definitions and saturation.} *) + open Aux.BasicOperators let debug_level = ref 0 let aggregate_drop_negative = ref false let aggregate_fixpoint = ref true -(** Expand static relations that do not have ground facts, are not - directly recursive, and have arity above the threshold. *) -let expand_arity_above = ref 0 - -(** Treat "next" clauses which introduce metavariables only for - variable-variable mismatch, as non-erasing frame clauses (to be - ignored). ("Wave" refers to the process of "propagating the frame - condition" that these clauses are assumed to do, if - [nonerasing_frame_wave] is set to [true].) *) -let nonerasing_frame_wave = ref true - type term = | Const of string | Var of string - | MVar of string (* meta-variable, not used in GDL *) - | Func of string * term list + | Func of string * term array +type rel_atom = string * term list +(** Positive and negative literals separated, disjunctions expanded-out. *) +type gdl_rule = rel_atom * rel_atom list * rel_atom list +(** Collect rules by relations. *) +type def_branch = term list * rel_atom list * rel_atom list +type gdl_defs = (string * def_branch list) list + +module Terms = Set.Make ( + struct type t = term let compare = Pervasives.compare end) +module Atoms = Set.Make ( + struct type t = rel_atom let compare = Pervasives.compare end) + type atom = | Distinct of term list - | Rel of string * term list - | Currently of term + | Rel of rel_atom + | Role of term + | True of term | Does of term * term type literal = @@ -35,51 +42,34 @@ | Neg of atom | Disj of literal list -type game_descr_entry = - | Datalog of string * term list * literal list - | Next of term * literal list - | Legal of term * term * literal list - | Goal of term * int * literal list - | GoalPattern of term * string * literal list - | Terminal of literal list - | Role of term - | Initial of term * literal list - | Atomic of string * term list +type clause = rel_atom * literal list type request = - | Start of string * term * game_descr_entry list * int * int - (* prepare game: match id, role, game, startclock, playclock *) + | Start of string * term * clause list * int * int + (** prepare game: match id, role, game, startclock, playclock *) | Play of string * term list - (* request a move: match id, actions on previous step *) + (** request a move: match id, actions on previous step *) | Stop of string * term list - (* game ends here: match id, actions on previous step *) + (** game ends here: match id, actions on previous step *) let rec term_str = function | Const c -> c | Var v -> "?"^v - | MVar v -> "@"^v | Func (f, args) -> "(" ^ f ^ " " ^ String.concat " " (List.map term_str args) ^ ")" let rec term_to_name ?(nested=false) = function | Const c -> c | Var v -> v - | MVar v -> v | Func (f, args) -> f ^ "_" ^ (if nested then "_S_" else "") ^ String.concat "_" (List.map (term_to_name ~nested:true) args) ^ (if nested then "_Z_" else "") -let rec vars ?(meta=false) = function - | Const _ -> [] - | Var x -> [x] - | MVar x -> if meta then [x] else [] - | Func (_, args) -> Aux.concat_map vars args - let rec term_vars = function | Const _ -> Aux.Strings.empty - | Var v | MVar v -> Aux.Strings.singleton v + | Var v -> Aux.Strings.singleton v | Func (f, args) -> terms_vars args and terms_vars args = @@ -87,166 +77,79 @@ (List.map term_vars args) -let fact_of_atom = function - | Distinct args -> assert false +let rel_of_atom = function + | Distinct args -> "distinct", args (* not a proper relation -- avoid *) | Rel (rel, args) -> rel, args - | Currently arg -> "true", [arg] + | Role arg -> "role", [arg] + | True arg -> "true", [arg] | Does (arg1, arg2) -> "does", [arg1; arg2] +let atom_of_rel = function + | "distinct", args -> Distinct args (* not a proper relation -- avoid *) + | "role", [arg] -> Role arg + | "true", [arg] -> True arg + | "does", [arg1; arg2] -> Does (arg1, arg2) + | rel, args -> Rel (rel, args) + let rec body_of_literal = function | Pos (Distinct args) -> [Aux.Right ("distinct", args)] (* not negated actually! *) | Neg (Distinct _) -> assert false - | Pos atom -> [Aux.Left (fact_of_atom atom)] - | Neg atom -> [Aux.Right (fact_of_atom atom)] + | Pos atom -> [Aux.Left (rel_of_atom atom)] + | Neg atom -> [Aux.Right (rel_of_atom atom)] | Disj disjs -> Aux.concat_map body_of_literal disjs let func_graph f terms = Aux.map_some (function Func (g, args) when f=g -> Some args | _-> None) terms -(* Type shortcuts (mostly for documentation). *) -type gdl_atom = string * term list -type gdl_rule = gdl_atom * gdl_atom list * gdl_atom list -(* Definition with collected relation branches and negation-local - variables found. *) -type lit_def_branch = - term list * gdl_atom list * (Aux.Strings.t * gdl_atom) list -type lit_def = string * lit_def_branch list -(* Definition with expanded definitions: expansion of a negated - relation brings negated (possibly locally existentially quantified) - conjunctions. *) -type exp_def_branch = - term list * gdl_atom list * (Aux.Strings.t * gdl_atom list) list -type exp_def = string * exp_def_branch list -module Terms = Set.Make ( - struct type t = term let compare = Pervasives.compare end) -module Atoms = Set.Make ( - struct type t = string * term list let compare = Pervasives.compare end) - - -let lit_def_br_vars (head, body, neg_body : lit_def_branch) = +let gdl_rule_vars (head, body, neg_body) = List.fold_left Aux.Strings.union Aux.Strings.empty (List.map terms_vars - (head::List.map snd body @ - List.map (snd -| snd) neg_body)) + (head::List.map snd (body @ neg_body))) -let exp_def_br_vars (head, body, neg_body : exp_def_branch) = +let gdl_rules_vars brs = List.fold_left Aux.Strings.union Aux.Strings.empty - (List.map terms_vars - (head::List.map snd body @ - Aux.concat_map (List.map snd -| snd) neg_body)) + (List.map gdl_rule_vars brs) -let lit_def_brs_vars brs = +let rels_vars body = List.fold_left Aux.Strings.union Aux.Strings.empty - (List.map lit_def_br_vars brs) + (List.map (fun (_,args)->terms_vars args) body) -let exp_def_brs_vars brs = - List.fold_left Aux.Strings.union Aux.Strings.empty - (List.map exp_def_br_vars brs) +let gdl_defs_vars defs = + List.fold_left + (fun acc rels -> Aux.Strings.union acc (rels_vars rels)) + Aux.Strings.empty + (Aux.concat_map (fun (hd,body,neg_body) -> + ("",hd)::body @ neg_body) (Aux.concat_map snd defs)) -let sdef_br_vars (head, body, neg_body) = - exp_def_br_vars ([head], body, neg_body) +let rules_of_clause (head, body) = + let body, neg_body = + Aux.partition_choice (Aux.concat_map body_of_literal body) in + head, body, neg_body -let sdef_brs_vars brs = - List.fold_left Aux.Strings.union Aux.Strings.empty - (List.map sdef_br_vars brs) -let rels_vars body = - List.fold_left Aux.Strings.union Aux.Strings.empty - (List.map (fun (_,args)->terms_vars args) body) +let clause_vars cl = gdl_rule_vars (rules_of_clause cl) -let rules_of_entry = function - | Datalog (rel, args, body) -> - let head = rel, args in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | Next (head, body) -> - let head = "next", [head] in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | Legal (arg1, arg2, body) -> - let head = "legal", [arg1; arg2] in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | Goal (arg, payoff, body) -> - let head = "goal", [arg; Const (string_of_int payoff)] in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | GoalPattern (arg, var, body) -> - let head = "goal", [arg; Var var] in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | Terminal body -> - let head = "terminal", [] in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | Role arg -> [("role", [arg]), [], []] - | Initial (arg, body) -> - let head = "init", [arg] in - let bodies = Aux.product (List.map body_of_literal body) in - List.map (fun body -> - let pos_body, neg_body = Aux.partition_choice body in - head, pos_body, neg_body) bodies - | Atomic (rel, args) -> [(rel, args), [], []] +let defs_of_rules rules = + Aux.map_reduce (fun ((rel, args), body, neg_body) -> + rel, (args, body, neg_body)) (fun y x->x::y) [] rules -let add_neg_body_vars global_vars neg_body : (Aux.Strings.t * gdl_atom) list = - List.map (fun (_, args as a)-> - let local_vs = Aux.Strings.diff (terms_vars args) global_vars in - local_vs, a) neg_body - -let lit_defs_of_rules rules : (string * lit_def_branch list) list = - Aux.map_reduce - (fun ((drel, params), body, 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 - -let rules_of_lit_defs (defs : lit_def list) = +let rules_of_defs defs = Aux.concat_map (fun (rel, branches) -> List.map (fun (args, body, neg_body) -> - let neg_body = - List.map snd neg_body in (rel, args), body, neg_body) branches) defs -let exp_brs_of_lit_brs brs = - List.map (fun (args, body, neg_body) -> - let neg_body = - List.map (fun (vs,a) -> vs,[a]) neg_body in - args, body, neg_body) brs - -let exp_defs_of_lit_defs defs : exp_def list = - List.map (fun (rel, branches) -> - rel, exp_brs_of_lit_brs branches) defs - - -(* Stratify either w.r.t. the dependency graph ([~def:true]) or its - subgraph the negation graph ([~def:false]). *) -let rec stratify ?(def=false) strata (defs : lit_def list) = +(* Stratify w.r.t. the negation call-graph. *) +let rec stratify strata defs = match List.partition (fun (_, branches) -> - List.for_all (fun (_, body, neg_body) -> - let neg_body = List.map snd neg_body in + List.for_all (fun (_, _, neg_body) -> List.for_all (fun (rel1,_) -> rel1 = "distinct" || rel1 = "true" || rel1 = "does" || - not (List.mem_assoc rel1 defs)) - (if def then body @ neg_body - else neg_body)) branches) defs + not (List.mem_assoc rel1 defs)) neg_body) + branches) defs with | [], [] -> (* {{{ log entry *) @@ -269,28 +172,22 @@ (* }}} *) List.rev (stratum::strata) | [], _ -> - if def then raise + raise (Lexer.Parsing_error - "GDL.stratify: recursive non-static definitions not handled yet") - else raise - (Lexer.Parsing_error "GDL.stratify: cyclic negation dependency") | 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 + stratify (stratum::strata) (more_rules @ rules) let rec subst_one (x, term as sb) = function | Var y when x=y -> term - | MVar y when x=y -> term - | (Const _ | Var _ | MVar _ as t) -> t + | (Const _ | Var _ as t) -> t | Func (f, args) -> Func (f, List.map (subst_one sb) args) @@ -321,73 +218,9 @@ | _ -> raise Not_found -(* Match the first argument as term against the second argument as - pattern. Allow nonlinear (object) variables. *) -let rec match_meta ?(ignore_meta=false) sb m_sb terms1 terms2 = - match terms1, terms2 with - | [], [] -> sb, m_sb - | (Const _ (* | Var _ *) as a)::terms1, - (Const _ (* | Var _ *) as b)::terms2 - when a=b -> match_meta ~ignore_meta sb m_sb terms1 terms2 - | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g -> - match_meta ~ignore_meta sb m_sb (args1 @ terms1) (args2 @ terms2) - | term::terms1, MVar x::terms2 -> - (* we don't substitute because metavariables are linear *) - match_meta ~ignore_meta sb ((x, term)::m_sb) terms1 terms2 - | MVar _::terms1, _::terms2 -> - if ignore_meta then match_meta ~ignore_meta sb m_sb terms1 terms2 - else raise Not_found - | term::terms1, Var x::terms2 -> - let sb1 = x, term in - let sb = - if List.mem_assoc x sb then - if List.assoc x sb = term then sb - else raise Not_found - else sb1::sb in - match_meta ~ignore_meta sb m_sb terms1 terms2 - | _ -> - (* {{{ log entry *) - if !debug_level > 4 then ( - Printf.printf "match_meta: unmatched (%s) against pattern (%s)\n%!" - (String.concat ", " (List.map term_str terms1)) - (String.concat ", " (List.map term_str terms2)) - ); - (* }}} *) - raise Not_found - - -let generalize term1 term2 = - let fresh_count = ref 0 in - let rec loop pf terms1 terms2 = - match terms1, terms2 with - | [], [] -> (0, 0), [], [] - | (Const a as cst)::terms1, Const b::terms2 when a=b -> - let (good_vars, good_csts), mism, gens = loop pf terms1 terms2 in - (good_vars, good_csts+1), mism, cst::gens - | Func (f,args1)::terms1, Func (g,args2)::terms2 when f=g -> - let (good_vars1, good_csts1), mism1, gen_args = loop f args1 args2 in - let (good_vars2, good_csts2), mism2, gens = loop pf terms1 terms2 in - (good_vars1+good_vars2, good_csts1+good_csts2), mism1 @ mism2, - (Func (f,gen_args))::gens - | (Var x as var)::terms1, Var y::terms2 when x=y -> - let (good_vars, good_csts), mism, gens = loop pf terms1 terms2 in - (good_vars+1, good_csts), mism, var::gens - | t1::terms1, t2::terms2 -> - let measure, mism, gens = loop pf terms1 terms2 in - incr fresh_count; - measure, (t1,t2)::mism, MVar ("MV"^string_of_int !fresh_count)::gens - | _::_, [] | [], _::_ -> raise - (Lexer.Parsing_error - ("GDL.generalize: arity mismatch at function "^pf)) in - let measure, mism, gens = loop "impossible" [term1] [term2] in - measure, !fresh_count, mism, List.hd gens - - let rec subst sb = function | Var y as t -> (try List.assoc y sb with Not_found -> t) - | MVar y as t -> - (try List.assoc y sb with Not_found -> t) | Const _ as t -> t | Func (f, args) -> Func (f, List.map (subst sb) args) @@ -409,6 +242,10 @@ if rel1 = rel2 then unify [] args1 args2 else raise Not_found +let rels_unify atom1 atom2 = + try ignore (unify_rels atom1 atom2); 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 @@ -418,12 +255,28 @@ let var_terms = List.map (fun v->Var v) (vars1 @ vars2) in unify [] var_terms (terms1 @ terms2) -let subst_br sb (head, body, neg_body) = - List.map (subst sb) head, +let subst_br sb (args, body, neg_body) = + List.map (subst sb) args, subst_rels sb body, List.map (fun (uni_vs,neg) -> uni_vs, subst_rels sb neg) neg_body -let fact_str (rel, args) = + +let subst_atom sb = function + | Distinct args -> Distinct (List.map (subst sb) args) + | Rel rel_atom -> Rel (subst_rel sb rel_atom) + | Role arg -> Role (subst sb arg) + | True arg -> True (subst sb arg) + | Does (arg1, arg2) -> Does (subst sb arg1, subst sb arg2) + +let rec subst_literal sb = function + | Pos atom -> Pos (subst_atom sb atom) + | Neg atom -> Neg (subst_atom sb atom) + | Disj disjs -> Disj (List.map (subst_literal sb) disjs) + +let subst_clause sb (head, body) = + subst_rel sb head, List.map (subst_literal sb) body + +let rel_atom_str (rel, args) = "(" ^ rel ^ " " ^ String.concat " " (List.map term_str args) ^ ")" let tuples_str tups = @@ -434,40 +287,22 @@ let terms_str facts = String.concat ", " (List.map term_str facts) -let facts_str facts = String.concat " " (List.map fact_str facts) +let rel_atoms_str body = String.concat " " (List.map rel_atom_str body) -let neg_lfacts_str negs = +let neg_rel_atoms_str neg_body = String.concat " " - (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 "^fact_str d^")") negs) + (List.map (fun a -> "(not " ^ rel_atom_str a ^")") neg_body) -let neg_facts_str negs = - String.concat " " - (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 ^ ")" + "("^ rel_atom_str (rel, args) ^ " <= " ^ rel_atoms_str body ^ + " " ^ neg_rel_atoms_str neg_body ^ ")" -let lit_def_str (rel, branches) = +let def_str (rel, branches) = String.concat "\n" (List.map (fun (args, body, neg_body) -> - "("^ fact_str (rel, args) ^ " <= " ^ facts_str body ^ - " " ^ neg_lfacts_str neg_body ^ ")" - ) branches) + "("^ rel_atom_str (rel, args) ^ " <= " ^ rel_atoms_str body ^ + " " ^ neg_rel_atoms_str neg_body) + branches) -let exp_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 sb_str sb = String.concat ", " (List.map (fun (v,t)->v^":="^term_str t) sb) @@ -486,7 +321,11 @@ if List.mem head tot_base then [] else if List.exists (fun (rel,args as neg_atom) -> rel = "distinct" && Aux.not_unique args || - List.mem neg_atom tot_base) neg_body then [] + (* faster option: *) + (* List.mem neg_atom tot_base *) + (* accurate option: *) + List.exists (unifies neg_atom) tot_base + ) neg_body then [] else [Aux.Left head] | head, cond1::body, neg_body -> Aux.map_try (fun fact -> @@ -494,7 +333,7 @@ if !debug_level > 5 then ( Printf.printf "instantiate_one: trying to unify %s and %s\n%!" - (fact_str fact) (fact_str cond1) + (rel_atom_str fact) (rel_atom_str cond1) ); (* }}} *) @@ -515,7 +354,7 @@ (* {{{ log entry *) if !debug_level > 4 then ( Printf.printf "inst_stratum: old_base = %s; cur_base = %s\n%!" - (facts_str old_base) (facts_str cur_base); + (rel_atoms_str old_base) (rel_atoms_str cur_base); Printf.printf "inst_stratum: #old_irules = %d, #cur_irules = %d\n%!" (List.length old_irules) (List.length cur_irules) @@ -528,7 +367,7 @@ (* {{{ log entry *) if !debug_level > 4 then ( Printf.printf "inst_stratum: cur-cur = %s\n%!" - (facts_str new_base1) + (rel_atoms_str new_base1) ); (* }}} *) let new_base2, new_irules2 = @@ -536,7 +375,7 @@ (* {{{ log entry *) if !debug_level > 4 then ( Printf.printf "inst_stratum: cur-old = %s\n%!" - (facts_str new_base2) + (rel_atoms_str new_base2) ); (* }}} *) let new_base3, new_irules3 = @@ -544,7 +383,7 @@ (* {{{ log entry *) if !debug_level > 4 then ( Printf.printf "inst_stratum: old-cur = %s\n%!" - (facts_str new_base3) + (rel_atoms_str new_base3) ); (* }}} *) let new_base = Aux.unique_sorted (new_base1 @ new_base2 @ new_base3) @@ -564,9 +403,117 @@ instantiate (inst_stratum [] [] base stratum) strata in instantiate base - (List.map rules_of_lit_defs (stratify [] (lit_defs_of_rules rules))) + (List.map rules_of_defs (stratify [] (defs_of_rules rules))) +(* ************************************************************ *) +(* ************************************************************ *) +(** {3 Transformations of GDL clauses: inlining, negation.} *) +(** Expand branches of a definition inlining the provided definitions, + only expand positive literals. Iterate expansion to support + nesting of definitions. *) +let expand_positive_lits defs brs = + let used_vars = ref (gdl_defs_vars (("",brs)::defs)) in + let freshen_brs brs = + let br_vars = gdl_defs_vars ["",brs] in + let sb = List.map + (fun v -> + v, Aux.not_conflicting_name ~truncate:true !used_vars v) + (Aux.Strings.elements br_vars) in + used_vars := Aux.add_strings (List.map snd sb) !used_vars; + List.map (subst_br sb) brs in + let expand_atom (rel, args as atom) result = + (let try def_brs = freshen_brs (List.assoc rel defs) in + Aux.concat_map (fun (sb, (head, r_body, r_neg_body)) -> + let args = subst_terms sb args in + List.map (fun (params,d_body,d_neg_body) -> + let sb = unify sb params args in + let r_br = + head, d_body @ r_body, d_neg_body @ r_neg_body in + sb, subst_br sb r_br + ) def_brs + ) result + with Not_found -> + List.map (fun (sb,(head,r_body,r_neg_body)) -> + sb, atom::r_body, r_neg_body) result) in + let expand_br (head, body, neg_body) = + let init = [[], (head, [], neg_body)] in + Aux.concat_foldr expand_atom body init in + let rec fix n_brs brs i = + let brs = Aux.concat_map expand_br brs in + let new_n_brs = List.length brs in + if new_n_brs > n_brs && i > 0 then fix new_n_brs brs (i-1) + else brs in + fix (List.length brs) brs 5 + + +(** Form clause bodies whose disjunction is equivalent to the + negation of disjunction of given clause bodies. *) +let negate_bodies conjs = + let placeholder = "", [] in + let clauses = List.map (fun body -> placeholder, body) conjs in + let clauses = List.map rules_of_clause clauses in + let clauses = List.map (fun (_,body,neg_body) -> + List.map (fun a -> Pos (atom_of_clause a)) body @ + List.map (fun a -> Neg (atom_of_clause a)) neg_body) clauses in + let negated = Aux.product clauses in + (* can raise [Not_found] in case of unsatisfiable "not distinct" *) + let nclause body = + let uniterms, lits = + Aux.partition_map (function + | Neg (Distinct terms) -> Left terms + | Neg atom -> Pos atom + | Pos atom -> Neg atom + | Disjunction _ -> assert false) body in + let sb = List.fold_left unify_all [] uniterms in + List.map (subst_literal sb) lits in + Aux.map_try nclause negated + + +(** Rename clauses so that they have disjoint variables. Return a cell + storing all variables. *) +let rename_clauses clauses = + let used_vars = ref Aux.Strings.empty in + let clauses = List.map (fun cl -> + let cl_vars = clause_vars cl in + let sb = + List.map (fun v -> + let nv = Aux.not_conflicting_name ~truncate:true !used_vars v in + used_vars := Aux.Strings.add nv !used_vars; + v, nv + ) cl_vars in + subst_clause sb cl + ) clauses in + used_vars, clauses + + +let flatten_disjs body = + let rec aux = function + | (Pos _ | Neg _) as lit -> [lit] + | Disj lits -> Aux.concat_map aux lits in + List.map (function + | (Pos _ | Neg _) as lit -> lit + | Disj _ as disj -> Disj (aux disj)) body + + +let nnf_dnf body = + List.map (function + | Pos a -> [Neg a] + | Neg a -> [Pos a] + | Disj lits -> + List.map (function + | Pos a -> Neg a + | Neg a -> Pos a + | _ -> assert false) lits + ) (List.map flatten_disjs body) + + +(* ************************************************************ *) +(* ************************************************************ *) +(** {3 GDL whole-game operations.} + + Aggregate playout, player-denoting variable elimination. *) + (* Collect the aggregate playout, but also the actions available in the state. *) exception Playout_over @@ -578,7 +525,7 @@ (* {{{ log entry *) if !debug_level > 4 then ( Printf.printf "GDL.aggregate_ply: updated base -- %s\n%!" - (String.concat " " (List.map fact_str base)) + (rel_atoms_str base) ); (* }}} *) let does = Aux.map_some (fun (rel, args) -> @@ -714,23 +661,258 @@ loop cycle trav [] cycle tail in loop [] [] [] [] cands -let cmp_masks t1 t2 = - (* {{{ log entry *) - if !debug_level > 4 then ( - Printf.printf "cmp_masks: %s <= %s .. " (term_str t1) (term_str t2); - ); - (* }}} *) - try ignore (match_meta [] [] [t2] [t1]); - (* {{{ log entry *) - if !debug_level > 4 then ( - Printf.printf "true\n%!"; - ); - (* }}} *) - true - with Not_found -> - (* {{{ log entry *) - if !debug_level > 4 then ( - Printf.printf "false\n%!"; - ); - (* }}} *) - false + +let expand_players clauses = + let players = + Aux.map_some (function + | ("role", [player]), _ -> Some player + | _ -> None + ) clauses in + let exp_clause (rel, _ as head, body as clause) = + (* determine variables standing for players *) + let plvars = + let head = if rel = "role" then [] else [head] in + Aux.concat_map player_vars_of + (head @ List.map rel_of_atom body) in + if plvars = [] then [clause] + else + let sbs = List.map (fun v -> + List.map (fun pl -> v, pl) players) plvars in + List.map (fun sb -> subst_clause sb clause) sbs in + Aux.concat_map exp_clause clauses + +(** Partition relations into stable (not depending, even indirectly, + on "true") and remaining ones. *) +let stable_rels defs = + let rec aux nonstable remaining = + let more = Aux.map_some (fun (rel, branches) -> + if List.exists + (fun (_, body, neg_body) -> + let called = List.map fst (body @ neg_body) in + List.exists (fun rel -> rel = "true" || + List.mem rel nonstable) called + ) branches + then Some rel else None + ) remaining in + if more = [] then List.map fst remaining, nonstable + else aux (more @ nonstable) + (List.filter (fun (rel,_) -> not (List.mem rel more)) remaining) + in + aux [] remaining + + +let state_terms body = + let rec aux = function + | Pos (True t) -> [t] + | Neg (True t) -> [t] + | Disj ls -> Aux.concat_map aux ls + | _ -> [] in + Aux.concat_map aux body + +let rec term_arities = + function + | Func (rel, args) -> + (rel, Array.length args):: + Aux.concat_map term_arities (Array.to_list args) + | _ -> [] + + +(* ************************************************************ *) +(* ************************************************************ *) +(** {3 Paths and operations involving terms and paths.} *) + +(** A path is a position in a tree together with labels on nodes from + the root to that position (but excluding the position). *) +type path = (string * int) list + +(** A trie representing a set of paths. *) +type path_set = + | Empty + | Here (** Singleton $\{\epsilon\}$. *) + | Below of (string * path_set array) list + | Here_and_below of (string * path_set array) list +(* Subtries are in sorted order. *) + +let path_str p = + String.concat "_" (List.map (fun (rel, arg) -> + rel ^ "_" ^ string_of_int arg) p) + +let paths_union ps1 ps2 = + let rec aux = function + | Empty, p | p, Empty -> p + | Here, Below ps | Below ps, Here -> Here_and_below ps + | Below ps1, Below ps2 -> Below (merge (ps1, ps2)) + | Below ps1, Here_and_below ps2 + | Here_and_below ps2, Below ps1 + | Here_and_below ps1, Here_and_below ps2 + -> Here_and_below (merge (ps1, ps2)) + and merge = function + | [], ps | ps, [] -> ps + | ((rel1, args1)::ps1), ((rel2, args2)::ps2) when rel1 = rel2 -> + let args = Aux.array_map2 aux args1 args2 in + (rel1, args)::merge (ps1, ps2) + | ((rel1, _ as rel_ps)::ps1), ((rel2, _)::_ as ps2) when rel1 < rel2 -> + rel_ps::merge (ps1, ps2) + | ((rel1, _)::_ as ps1), ((rel2, _ as rel_ps)::ps2) -> + rel_ps::merge (ps1, ps2) in + aux (ps1, ps2) + +let add_path arities p ps = + let rec aux = function + | [], Empty -> Here + | [], (Below ps | Here_and_below ps) -> Here_and_below ps + | (rel, pos)::suffix, Below ps -> + Below (add suffix rel pos ps) + | (rel, pos)::suffix, Here_and_below ps -> + Here_and_below (add suffix rel pos ps) + and add p rel pos ps = + (let try args, ps = Aux.pop_assoc rel ps in + (* Keeping functional... *) + let args = Array.copy args in + args.(pos) <- aux (p, args.(pos)); + (rel, args)::ps + with Not_found -> + let args = Array.make (arities rel) Empty in + args.(pos) <- aux (p, args.(pos)); + (rel, args)::ps) + in + aux (p, ps) + +(** Find a path in a term and substitute, raise [Not_found] if path + not present. [subst_at_path p s t] is $t[p \ot s]$. *) +let subst_at_path p s t = + let rec aux = function + | [], _ -> s + | (rel1, pos)::p, Func (rel2, args) when rel1 = rel2 -> + let args = Array.copy args in + args.(pos) <- aux (p, args.(pos)); + Func (rel1, args) + | _ -> raise Not_found in + aux (p, t) + +(** [simult_subst ps s t] substitutes [s] at all [t] paths that belong + to the set [ps], returns $t[ps \ot s]$. *) +let simult_subst ps s t = + let rec aux = function + | Empty, t -> t + | (Here | Here_and_below _), _ -> s + | Below subps, (Func (rel, args) as t) -> + (let try argps = List.assoc rel subps in + Func (rel, Aux.array_map2 (fun ps t -> aux (ps,t)) argps args) + with Not_found -> t) + | Below _, t -> t in + aux (ps, t) + +(** Find the subterm at given path, if the term does not have the + path, return [Not_found]; [at_path p t] is $t \tpos p$. *) +let at_path t p = + let rec aux = function + | [], t -> t + | (rel1, pos)::p, Func (rel2, args) when rel1 = rel2 -> + aux (p, args.(pos)) + | _ -> raise Not_found in + aux (p, t) + +(** Find the list of subterms at paths from the given set, if the term + does not have some of the paths, ignore them if [~fail_at_missing:false], + raise [Not_found] if [~fail_at_missing:true]. *) +let at_paths ?(fail_at_missing=false) ps t = + let miss () = + if fail_at_missing then raise Not_found else [] in + let rec aux = function + | Empty, t -> [] + | Here, t -> [t] + | Here_and_below subps, t -> t::(aux (Below subps, t)) + | Below subps, (Func (rel, args) as t) + when not fail_at_missing -> + (let try argps = List.assoc rel subps in + let res = Aux.array_map2 (fun ps t -> aux (ps,t)) argps args in + List.concat (Array.to_list res) + with Not_found -> []) + | Below [rel1, argps], (Func (rel2, args) as t) + when rel1 = rel2 (* && fail_at_missing *) -> + let res = Aux.array_map2 (fun ps t -> aux (ps,t)) argps args in + List.concat (Array.to_list res) + | Below _, t -> miss () in + aux (ps, t) + +(** Find the list of results of a function applied to paths from the + given set that are in the term, and to subterms at these paths. *) +let map_paths f ps t = + let rec aux revp = function + | Empty, t -> [] + | Here, t -> [f (List.rev revp) t] + | Here_and_below subps, t -> + f (List.rev revp) t::(aux path (Below subps, t)) + | Below subps, (Func (rel, args) as t) -> + (let try argps = List.assoc rel subps in + let res = + Array.mapi (fun i ps -> aux ((rel,i)::revp) (ps,args.(i))) argps in + List.concat (Array.to_list res) + with Not_found -> []) + | Below _, t -> [] in + aux [] (ps, t) + +(** All paths in a term pointing to subterms that satisfy a + predicate. With [~prefix_only:true], paths that contain a path + that has been included, are not included. *) +let rec term_paths ?(prefix_only=false) cond = function + | Func (rel, args) as t -> + let subps = Array.map (term_paths p) args in + let no_sub = Array.for_all (fun subp -> subp = Empty) subps in + let here = cond t in + if no_sub && not here then Empty + else if here && not no_sub && not prefix_only then Here_and_below subps + else if here then Here + else Below subps + | t -> if cond t then Here else Empty + +(** The number of nodes in a term tree. *) +let rec term_size = function + | Const _ | Var _ -> 1 + | Func (_, args) -> + Array.fold_left (fun acc t -> acc + term_size t) 1 args + +(** The set of paths that merges two terms, the cardinality of this + set, and the size of the largest common subtree. *) +let rec merge_terms s t = + match s, t with + | s, t when s = t -> Empty, 0, term_size t + | Func (rel1, args1), Func (rel2, args2) when rel1 = rel2 -> + let subr = Aux.array_map2 merge_terms args1 args2 in + let subps = Array.map Aux.fst3 subr + and subcard = Array.map Aux.snd3 subr + and subsize = Array.map Aux.trd3 subr in + Below [rel1, subps], Array.fold_left (+) 0 subcard, + Array.fold_left (+) 1 subsize + | _ -> Here, 1, 0 + + +(** List the paths in a set. *) +let paths_to_list ps = + let rec subpaths subps = + Aux.concat_map (fun (rel, subps) -> + Array.to_list + (Array.mapi (fun i ps -> + let sub_res = aux ps in + List.map (fun p -> (rel, i)::p) sub_res) subps)) subps + and aux = function + | Empty -> [] + | Here -> [[]] + | Here_and_below subps -> []::(subpaths subps) + | Below subps -> subpaths subps in + aux ps + + +(** Toss relations hold between subterms of GDL state terms: generate + Toss relation name. *) +let rel_on_paths rel paths_tup = + rel ^ "__" ^ String.concat "__" (List.map path_str paths_tup) + +(** Some Toss predicates are generated from a path and an expected + subterm at that path. *) +let pred_on_path_subterm path subterm = + path_str path ^ term_to_name subterm + +(** A "blank" term. *) +let blank = Const "_BLANK_" Modified: trunk/Toss/GGP/GDL.mli =================================================================== --- trunk/Toss/GGP/GDL.mli 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/GGP/GDL.mli 2011-07-09 10:28:17 UTC (rev 1507) @@ -19,13 +19,23 @@ type term = | Const of string | Var of string - | MVar of string | Func of string * term list +type rel_atom = string * term list +(** Positive and negative literals separated, disjunctions expanded-out. *) +type gdl_rule = rel_atom * rel_atom list * rel_atom list +(** Collect rules by relations. *) +type def_branch = term list * rel_atom list * rel_atom list +type gdl_defs = (string * def_branch list) list + +module Terms : Set.S with type elt = term +module Atoms : Set.S with type elt = rel_atom + type atom = | Distinct of term list - | Rel of string * term list - | Currently of term + | Rel of rel_atom + | Role of term + | True of term | Does of term * term type literal = @@ -33,71 +43,37 @@ | Neg of atom | Disj of literal list -type game_descr_entry = - | Datalog of string * term list * literal list - | Next of term * literal list - | Legal of term * term * literal list - | Goal of term * int * literal list - | GoalPattern of term * string * literal list - | Terminal of literal list - | Role of term - | Initial of term * literal list - | Atomic of string * term list +type clause = rel_atom * literal list type request = - | Start of string * term * game_descr_entry list * int * int + | Start of string * term * clause list * int * int (** prepare game: match id, role, game, startclock, playclock *) | Play of string * term list (** request a move: match id, actions on previous step *) | Stop of string * term list (** game ends here: match id, actions on previous step *) -(** Type shortcuts (mostly for documentation). *) -type gdl_atom = string * term list -type gdl_rule = gdl_atom * gdl_atom list * gdl_atom list -(** Definition with collected relation branches and negation-local - variables found. *) -type lit_def_branch = - term list * gdl_atom list * (Aux.Strings.t * gdl_atom) list -type lit_def = string * lit_def_branch 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 * exp_def_branch list - -module Terms : Set.S with type elt = term -module Atoms : Set.S with type elt = gdl_atom - val term_str : term -> string val terms_str : term list -> string val sb_str : (string * term) list -> string -val fact_str : string * term list -> string -val facts_str : (string * term list) list -> string -val exp_def_str : exp_def -> string +val rel_atom_str : rel_atom -> string +val rel_atoms_str : rel_atom list -> string +val def_str : + string * (term list * rel_atom list * rel_atom list) -> string val tuples_str : term list list -> string val proto_rel_str : string * string array -> string -val lit_def_br_vars : lit_def_branch -> Aux.Strings.t -val lit_def_str : lit_def -> string -val neg_facts_str : (Aux.Strings.t * gdl_atom list) list -> string +val gdl_rule_vars : gdl_rule -> Aux.Strings.t +val gdl_rules_vars : gdl_rule list -> Aux.Strings.t +val branch_str : string -> def_branch -> string -val exp_def_br_vars : exp_def_branch -> Aux.Strings.t -val branch_str : string -> exp_def_branch -> string - -val sdef_br_vars : term * gdl_atom list * (Aux.Strings.t * gdl_atom list) list-> - Aux.Strings.t -val sdef_brs_vars : - (term * gdl_atom list * (Aux.Strings.t * gdl_atom list) list) list -> - Aux.Strings.t - val func_graph : string -> term list -> term list list -val rules_of_entry : game_descr_entry -> gdl_rule list +val rules_of_clause : clause -> gdl_rule list val terms_vars : term list -> Aux.Strings.t -val rels_vars : gdl_atom list -> Aux.Strings.t +val rels_vars : rel_atom list -> Aux.Strings.t val term_to_name : ?nested:bool -> term -> string val term_vars : term -> Aux.Strings.t @@ -107,40 +83,24 @@ val subst_one : string * term -> term -> term val subst : (string * term) list -> term -> term -val subst_rel : (string * term) list -> gdl_atom -> gdl_atom -val subst_rels : (string * term) list -> gdl_atom list -> gdl_atom list -val subst_br : (string * term) list -> exp_def_branch -> exp_def_branch +val subst_rel : (string * term) list -> rel_atom -> rel_atom +val subst_rels : (string * term) list -> rel_atom list -> rel_atom list +val subst_br : (string * term) list -> def_branch -> def_branch -val add_neg_body_vars : Aux.Strings.t -> gdl_atom list -> - (Aux.Strings.t * gdl_atom) list +val defs_of_rules : gdl_rule list -> gdl_defs -val lit_defs_of_rules : - ((string * term list) * gdl_atom list * (string * term list) list) list -> - lit_def list - -val exp_defs_of_lit_defs : lit_def list -> exp_def list - -val match_meta : ?ignore_meta:bool -> (string * term) list -> - (string * term) list -> term list -> term list -> - (string * term) list * (string * term) list - val unify : (string * term) list -> term list -> term list -> (string * term) list val unifies : term -> term -> bool -val generalize : term -> term -> (int * int) * int * (term * term) list * term +val saturate : rel_atom list -> gdl_rule list -> rel_atom list -val saturate : gdl_atom list -> gdl_rule list -> gdl_atom list +val stratify : gdl_defs list -> gdl_defs -> gdl_defs list -val stratify : ?def:bool -> lit_def list list -> - lit_def list -> lit_def list list - val aggregate_playout : term array -> int -> gdl_rule list -> gdl_rule list * gdl_rule list * (string * term list) list * term list * (term list list list * term list list) val find_cycle : term option list -> term option list - -val cmp_masks : term -> term -> bool Modified: trunk/Toss/GGP/GDLParser.mly =================================================================== --- trunk/Toss/GGP/GDLParser.mly 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/GGP/GDLParser.mly 2011-07-09 10:28:17 UTC (rev 1507) @@ -17,7 +17,7 @@ %start parse_game_description parse_request parse_term %type <GDL.request> parse_request request %type <GDL.term> parse_term -%type <GDL.game_descr_entry list> parse_game_description game_description +%type <GDL.clause list> parse_game_description game_description %% @@ -44,11 +44,11 @@ | (Const "distinct" | Const "DISTINCT")::args -> Distinct args | [(Const "true" | Const "TRUE"); arg] -> - Currently arg + True arg | [(Const "does" | Const "DOES"); player; action] -> Does (player, action) | (Const "role" | Const "ROLE")::player -> - Rel ("role", player) + Role player | (Const "init" | Const "INIT")::state -> Rel ("init", state) | (Const "next" | Const "NEXT")::state -> @@ -71,38 +71,12 @@ | OPEN NOT a=atom CLOSE { Neg a } | OPEN OR disjs=list (literal) CLOSE { Disj disjs } -game_descr_entry: +clause: | OPEN REVIMPL head=atom body=list (literal) CLOSE { match head with - | Rel ("next", [t]) -> Next (t, body) - | Rel ("next", _) -> - raise (Lexer.Parsing_error "GDL next: not unary") - | Rel ("init", [arg]) -> Initial (arg, body) - | Rel ("init", _) -> - raise (Lexer.Parsing_error "GDL init: not unary") - | Rel ("terminal", []) -> Terminal body - | Rel ("terminal", _) -> - raise (Lexer.Parsing_error "GDL terminal: not nullary") - | Rel ("legal", [t1; t2]) -> - Legal (t1, t2, body) - | Rel ("legal", _) -> - raise (Lexer.Parsing_error "GDL legal: not binary") - | Rel ("goal", [t; Const gv]) -> - (try - let gv = int_of_string gv in - Goal (t, gv, body) - with Failure _ | Invalid_argument _ -> - raise (Lexer.Parsing_error "GDL goal: value not a constant int")) - | Rel ("goal", [t; Var gv]) -> - (try - GoalPattern (t, gv, body) - with Failure _ | Invalid_argument _ -> - raise (Lexer.Parsing_error "GDL goal: value not a constant int")) - | Rel ("goal", _) | Rel ("GOAL", _) -> - raise (Lexer.Parsing_error - "GDL goal: not binary or value not constant") - | Rel (r, args) -> Datalog (r, args, body) - | Currently _ -> + | Rel rel_atom -> rel_atom, body + | Role player -> ("role", [player]), body + | True _ -> raise (Lexer.Parsing_error "GDL rule: \"true\" in head") | Distinct _ -> raise (Lexer.Parsing_error "GDL rule: \"distinct\" in head") @@ -111,13 +85,8 @@ } | a=atom { match a with - | (Rel ("init", [arg])) -> Initial (arg, []) - | (Rel ("init", _)) -> - raise (Lexer.Parsing_error "GDL init: not unary") - | (Rel ("role", [arg])) -> Role arg - | (Rel ("role", _) | Rel ("ROLE", _)) -> - raise (Lexer.Parsing_error "GDL role: not unary") - | Rel (r, args) -> Atomic (r, args) + | Role player -> ("role", [player]), [] + | Rel rel_atom -> rel_atom, [] | _ -> raise (Lexer.Parsing_error "GDL atomic entry: not init, role nor fact") @@ -125,7 +94,7 @@ %public game_description: -| descr=list(game_descr_entry) +| descr=list(clause) { descr } %public request: Modified: trunk/Toss/GGP/Translate.ml =================================================================== --- trunk/Toss/GGP/Translate.ml 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/GGP/Translate.ml 2011-07-09 10:28:17 UTC (rev 1507) @@ -2072,8 +2072,8 @@ rname, List.map (fun _ -> ()) args) static_rules) in let static_rels = List.map (fun (rel,args) -> - rel, List.length args, - Aux.all_tuples_for args mask_paths) static_rels in + let ar = List.length args in + rel, ar, Aux.all_ntuples mask_paths ar) static_rels in let static_base = Aux.collect static_base in (* TODO: optimize by indexing elements by path position terms (currently, substitution values) *) @@ -3696,7 +3696,7 @@ let translate_last_action gdl_translation state actions = - if actions = [] then (* start of game -- Server will handle this as NOOP *) + if actions = [] then (* start of game -- Server will not perform a move *) "", [] else translate_incoming_move gdl_translation state actions Modified: trunk/Toss/Solver/Structure.ml =================================================================== --- trunk/Toss/Solver/Structure.ml 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/Solver/Structure.ml 2011-07-09 10:28:17 UTC (rev 1507) @@ -261,7 +261,32 @@ let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in { new_struc with relations = new_rel ; incidence = new_incidence } +(* Add tuple [tp] to relation [rn] in structure [struc]. *) +let add_rel_named_elems struc rn tp = + let new_struc, tp = + Array.fold_right (fun (struc, tp) e -> + let struc, e = find_or_new_elem struc e in + struc, e::tp) + (add_rel_name rn (Array.length tp) struc) tp in + let tp = Array.of_list tp in + let add_to_relmap rmap = + let tps = StringMap.find rn rmap in + StringMap.add rn (Tuples.add tp tps) rmap in + let new_rel = add_to_relmap new_struc.relations in + let add_to_imap imap e = + try + IntMap.add e (Tuples.add tp (IntMap.find e imap)) imap + with Not_found -> + IntMap.add e (Tuples.singleton tp) imap in + let new_incidence_imap = + try + Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp + with Not_found -> + Array.fold_left add_to_imap IntMap.empty tp in + let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in + { new_struc with relations = new_rel ; incidence = new_incidence } + (* Return a structure with a single relation, over a single tuple, of different elements. *) let free_for_rel rel arity = Modified: trunk/Toss/Solver/Structure.mli =================================================================== --- trunk/Toss/Solver/Structure.mli 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/Solver/Structure.mli 2011-07-09 10:28:17 UTC (rev 1507) @@ -167,6 +167,9 @@ (** Add tuple [tp] to relation [rn] in structure [struc]. *) val add_rel : structure -> string -> int array -> structure +(** Add tuple [tp] to relation [rn] in structure [struc]. *) +val add_rel_named_elems : structure -> string -> string array -> structure + (** Add tuple [tp] to relation [rn] in structure [struc] without checking whether it and its elements already exist in the structure and without checking arity. *) Modified: trunk/Toss/www/reference/reference.tex =================================================================== --- trunk/Toss/www/reference/reference.tex 2011-07-06 22:13:35 UTC (rev 1506) +++ trunk/Toss/www/reference/reference.tex 2011-07-09 10:28:17 UTC (rev 1507) @@ -1343,11 +1343,13 @@ of $s$ and $t$, the bigger its size the more similar $s$ and $t$ are. \end{definition} -Let $\mathrm{Next}_{e}$ be the set of \texttt{next} clauses in $G$ with all -atoms of \texttt{does} expanded (inlined) by the \texttt{legal} -clause definitions, duplicating the \texttt{next} clause when more -than one head of \texttt{legal} unifies with the \texttt{does} atom. -Intuitively, these are expanded forms of clauses defining game state change. +Let $\mathrm{Next}_{e}$ be the set of \texttt{next} clauses in $G$ +with all atoms of relations whose definitions use \texttt{true} +expanded (inlined) by their clause definitions, duplicating the +\texttt{next} clause when more than one clause of a relation unifies +with its atom. We expand \texttt{does} atoms by \texttt{legal} +clauses. We also expand disjunctions. Intuitively, these are expanded +forms of clauses defining game state change. For each clause $\calC \in \mathrm{Next}_{e}$, we select two terms $s_\calC$ and $t_\calC$ in the following way. The term $s_\calC$ is @@ -1420,7 +1422,7 @@ \begin{definition} We define the \emph{element mask equivalence} $\sim$ by: \[ t \sim s \quad \Leftrightarrow \quad - t[P_f \ot c] = s[P_f \ot c] \text{ for all terms } c.\] + t[\calP_f \ot c] = s[\calP_f \ot c] \text{ for all terms } c.\] The set of elements $A$ of the initial Toss structure $\frakA$ consists of equivalence classes of $\sim$. For $a \in A$ we write $\lsem a \rsem$ to denote the corresponding subset of equivalent terms from $\calS$. @@ -1488,19 +1490,21 @@ $p \in \calP_f$ and subterms $s = t\tpos_p, t \in \calS$, we introduce the \emph{fluent predicate} $Flu^s_p(a)$: \[ Flu^s_p(a) \ \ \iff \ \ t\tpos_p\ =\ s \text{ for some } - t \in \lsem a \rsem \cap \calS^{\text{init}}. \] +t \in \lsem a \rsem \cap \calS^{\text{init}}. +\] +Currently in the implementation, the string representing the path $p$ +alone is used as the predicate name, we use the prefixes $Anch$ and +$Flu$ in the reference for clarity. \noindent \textbf{Mask predicates.} -We say that a term $m$ is a \emph{mask term} if the paths to all variables -of $m$ are contained in $\calP_m \cup \calP_f$ and for each -$p \in \calP_m \cup \calP_f$ if $p$ exists in $m$ then $m \tpos_p$ is -a variable. We say that $m$ \emph{masks} a term $t$ if $m$ is a mask term -and there exists -a substitution $\sigma$ such that $\sigma(m) = t$. For all mask terms -$m \in \calS$ we introduce the \emph{mask predicate} $Mask_m$. +We define the mask root relation $\sim_m$ by: +\[ t \sim_m s \quad \Leftrightarrow \quad t[\calP_f \cup \calP_m \ot +c] = s[\calP_f \cup \calP_m \ot c] \text{ for all terms } c.\] We call +an equivalence class of $\sim_m$ a \emph{mask root}. For all mask +roots $m$ we introduce the \emph{mask predicate} $Mask_m$. Mask predicates are similar to the anchor predicates, but instead of -matching against a subterm, they match against the mask. -\[ Mask_m(a) \ \ \iff \ \ m \text{ masks all } t \in \lsem a \rsem. \] +matching against a subterm, they match against the mask root. +\[ Mask_m(a) \ \ \iff \ \ \lsem a \rsem \subset m. \] %Elements $a \in A$ can be represented as tuples consisting of a mask %term $m_a$ such that $Mask_{m_a}(a)$ and terms $s_p = a\tpos^m_p$ for @@ -1570,8 +1574,8 @@ \text{ and } \ \ Flu^{\mathtt{x}}_{(\mathtt{control},1)} = \{a_{ctrl}\}. \] \emph{Mask predicates.} -For the specification we consider, there are two mask terms: -$m_1 = (\mathtt{control}\ x)$ and $m_2 = (\mathtt{cell}\ x\ y\ z)$. +For the specification we consider, there are two mask roots: +$m_1 = \big\{(\mathtt{control}\ x) \ \big| \ (\mathtt{control}\ x) \in \calS \big\}$ and $m_2 = \big\{(\mathtt{cell}\ x\ y\ z) \ \big|\ (\mathtt{cell}\ x\ y\ z) \in \calS \big\}$. The predicate $Mask_{m_1} \ = \ \{ a_{ctrl} \}$ holds exactly for the control element, and $Mask_{m_2} = A \setminus \{a_{ctrl}\}$ contains these elements of $A$ which are not the control element, \ie the board elements. @@ -1690,8 +1694,13 @@ then for correctness, we need to preclude application of the first (more general) rule when the more concrete rule is applicable, adding \texttt{distinct} conditions to clauses of the otherwise more general -rule. In the current implementation, we only consider maximal sets of -\texttt{next} clauses. +rule. In the current implementation, we select a minimal covering +family of maximal sets of \texttt{next} clauses, where covering +means that every clause occurs in at least one set of the +family. (While in Section~\ref{subsec-rules} we describe additional +partition of the substituted clauses, in unlikely scenarios the +generated $\sigma_{\ol{\calC},\ol{\calN}}$ might be too specific to +capture all possible moves.) \begin{example} Let $\calC_1 = \mathtt{noop}$ and $\calC_2 = (\mathtt{mark}\ x\ y)$. @@ -1723,16 +1732,24 @@ will keep track of the elements that possibly lose fluents and ensure correct translation. +We determine which clauses are frame clauses prior to partitioning +into the rule clauses and computing the substitution +$\sigma_{\ol{\calC},\ol{\calN}}$ -- at the point where fluent paths +are computed. + From the frame clauses in $\sigma_{\ol{\calC}, \ol{\calN}}(\calN_1), \dots, -\sigma_{\ol{\calC}, \ol{\calN}}(\calN_m)$, we select all (maximal) subsets $J$ +\sigma_{\ol{\calC}, \ol{\calN}}(\calN_m)$, we select subsets $J$ such that, clauses in $J$ having the form $\mathtt{(<= (next\ s_i)\ b_i)}$, it holds -\[ s_1 \ \dot{=}_f \ \ldots \ \dot{=}_f \ s_{|J|}, \] -\ie the arguments of \texttt{next} unify. Note that we use $\dot{=}_f$ -instead of the standard unification, and by that we mean that the variables -shared with the \texttt{legal} clauses $\ol{\calC}$ are treated as constants. -The reason is that these variables are not local to the clauses and must -therefore remain intact. +\[ s_1 \ \dot{=}_f \ \ldots \ \dot{=}_f \ s_{|J|}, \] \ie the +arguments of \texttt{next} unify. Note that we use $\dot{=}_f$ instead +of the standard unification, and by that we mean that the variables +shared with the \texttt{legal} clauses $\ol{\calC}$ are treated as +constants. The reason is that these variables are not local to the +clauses and must therefore remain intact. As before, we select a +minimal covering family of maximal such subsets (possibly resulting, +in unlikely cases, in rules that do not remove fluent predicates over +elements that do not gain fluent predicates during rewriting.) Intuitively, the selected sets $J$ describe a partition of the state terms that could possibly be copied without change by the rule we will generate @@ -1751,8 +1768,8 @@ paths with \texttt{BLANK} and thus allow them to be deleted in case they are not preserved by other \texttt{next} clauses of the rule. Let us denote by $h$ the term $\rho(s_1)$ after the above replacement. The -erasure clauses $\calE_{\ol{\calC}, \ol{\calN}}(J) = \{ \mathtt{(<=\ - h\ e_1)} \dots \mathtt{(<=\ h\ e_l)} \},$ and we write +erasure clauses +$\calE_{\ol{\calC}, \ol{\calN}}(J) = \{ \mathtt{(<=\ h\ e_1)} \dots \mathtt{(<=\ h\ e_l)} \}$, and we write $\calE_{\ol{\calC}, \ol{\calN}}$ for the union of all $\calE_{\ol{\calC}, \ol{\calN}}(J)$, \ie for the set of all $\ol{\calC}, \ol{\calN}$ erasure clauses. @@ -1797,9 +1814,15 @@ rule clauses, and generate a Toss rule candidate for every partition of the groups into true and false ones: we collect the rule clauses that agree with the given partition. The selected atoms, some negated -according to the partition, form the separation condition. +according to the partition, form the separation condition. Currently, +we do not consider atoms under disjunction (mostly for simplicity +considerations; would this cause problems, the definition can be +extended to include disjunctions in making the partition). -For each candidate, we will construct the Toss rule in two steps. +We filter the rule candidates by checking for satisfiability (in the +same GDL model as used for building the initial Toss structure) of the +stable part of their clause bodies. For each remaining candidate, +we will construct the Toss rule in two steps. In the first step we generate the \emph{matching condition}: we translate the conjunction of the bodies of rule clauses and the @@ -1807,10 +1830,6 @@ atomic relations presented in Section~\ref{subsec-rels} and is described in Section~\ref{subsec-translate}. -Later we \emph{filter} the rule candidates by checking for -satisfiability in the initial structure of the stable part of the -matching condition. - In the second step, we build a Toss rewrite rule it... [truncated message content] |