[Toss-devel-svn] SF.net SVN: toss:[1455] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2011-05-23 01:33:05
|
Revision: 1455 http://toss.svn.sourceforge.net/toss/?rev=1455&view=rev Author: lukaszkaiser Date: 2011-05-23 01:32:57 +0000 (Mon, 23 May 2011) Log Message: ----------- Generating Breakthrough from pictures, without winning condition for now. Modified Paths: -------------- trunk/Toss/Formula/FormulaOps.ml trunk/Toss/Formula/FormulaOps.mli trunk/Toss/Formula/FormulaOpsTest.ml trunk/Toss/Server/Picture.ml trunk/Toss/Server/Picture.mli trunk/Toss/Server/def_pics/Makefile trunk/Toss/Solver/Structure.ml trunk/Toss/Solver/Structure.mli Modified: trunk/Toss/Formula/FormulaOps.ml =================================================================== --- trunk/Toss/Formula/FormulaOps.ml 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Formula/FormulaOps.ml 2011-05-23 01:32:57 UTC (rev 1455) @@ -615,6 +615,47 @@ fp_n real_str (List.length defs) (subst_once_rels_expr defs) r +(* --- AType with variables over given relations, no repetition, equality --- *) + +let atp rels vars_in = + if vars_in = [] then [] else + let vars = List.rev_map fo_var_of_string vars_in in + let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in + let prod i = + if i < 1 then [] else if i = 1 then + List.map (fun v -> [|v|]) vars + else let arr l = + if List.length (Aux.unique_sorted l) = i then + Some (Array.of_list l) + else None in + Aux.map_some arr (Aux.product (rept i vars)) in + let atom (rel, i) = List.rev_map (fun vs -> Rel (rel, vs)) (prod i) in + let atoms = Array.of_list (List.concat (List.map atom rels)) in + let choices = Aux.product (rept (Array.length atoms) [true; false]) in + let atom_choice i c = if c then atoms.(i) else Not (atoms.(i)) in + let tp_of_choice l = And (Array.to_list (Array.mapi atom_choice l)) in + List.rev_map tp_of_choice (List.rev_map Array.of_list choices) + +let mintp f rels vars = + let (add_vars, cur_tp) = (ref [], ref (List.filter f (atp rels vars))) in + let rec rept i l = if i < 1 then [] else l :: (rept (i-1) l) in + let mk_tp () = + if !debug_level > 0 then Format.printf "Making new tp.\n%!"; + let atoms = atp rels (vars @ !add_vars) in + if !debug_level > 0 then Format.printf "Atomic %i\n%!" (List.length atoms); + let add_vars_v = List.map (fun v -> var_of_string v) !add_vars in + let qex = Aux.product (rept (List.length !add_vars) [false; true]) in + let qphi phi v b = if b then Ex ([v], phi) else All ([v], phi) in + let quant c phi = List.fold_left2 qphi phi add_vars_v c in + let qatoms c = List.filter f (List.rev_map (quant c) atoms) in + List.fold_left (fun l c -> if l = [] then qatoms c else l) [] qex in + let new_var () = snd (subst_name_avoiding_str (vars @ !add_vars) "x0") in + while !cur_tp = [] do + add_vars := new_var () :: !add_vars; cur_tp := mk_tp () + done; + !cur_tp + + (* ------------------------------------------------------------------------- *) (* Prenex normal form. *) (* ------------------------------------------------------------------------- *) Modified: trunk/Toss/Formula/FormulaOps.mli =================================================================== --- trunk/Toss/Formula/FormulaOps.mli 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Formula/FormulaOps.mli 2011-05-23 01:32:57 UTC (rev 1455) @@ -134,7 +134,14 @@ (** Assign emptyset to an MSO-variable. *) val assign_emptyset : string -> formula -> formula +(** AType with variables over given relations, no repetition, equality. *) +val atp : (string * int) list -> string list -> formula list +(** Minimal type satisfying f over rels extending vars. *) +val mintp : (formula -> bool) -> (string * int) list -> string list -> + formula list + + (** {2 Transitive Closure} *) Modified: trunk/Toss/Formula/FormulaOpsTest.ml =================================================================== --- trunk/Toss/Formula/FormulaOpsTest.ml 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Formula/FormulaOpsTest.ml 2011-05-23 01:32:57 UTC (rev 1455) @@ -319,6 +319,30 @@ "R (y, x)" "S(y, x) and ex x0 (S(x, x0))"; ); + "atp, mintp" >:: + (fun () -> + let report phis = + (* List.iter (fun f -> Format.printf "\n%!"; Formula.print f) phis; *) + phis in + + let phis = report (FormulaOps.atp [("R", 2); ("P", 1)] []) in + assert_equal ~printer:string_of_int 0 (List.length phis); + + let phis = report (FormulaOps.atp [("R", 2); ("P", 1)] ["x"]) in + assert_equal ~printer:string_of_int 2 (List.length phis); + + let phis = report (FormulaOps.atp [("R", 2); ("P", 1)] ["x"; "y"]) in + assert_equal ~printer:string_of_int 16 (List.length phis); + + let nv n phi = List.length (FormulaOps.all_vars phi) = n in + + let phis = report (FormulaOps.mintp (nv 1) [("R", 2); ("P", 1)] []) in + assert_equal ~printer:string_of_int 2 (List.length phis); + + let phis = report (FormulaOps.mintp (nv 2) [("R", 2); ("P", 1)] []) in + assert_equal ~printer:string_of_int 16 (List.length phis); + ); + "transitive closure creation" >:: (fun () -> let tc_eq x y phi1 phi2 = Modified: trunk/Toss/Server/Picture.ml =================================================================== --- trunk/Toss/Server/Picture.ml 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Server/Picture.ml 2011-05-23 01:32:57 UTC (rev 1455) @@ -234,8 +234,76 @@ (s, !maxdx, !maxdy) + +(* Minimal types differentiating two structures. *) +let difftp rels s1 s2 = + let ok phi = Solver.M.check s1 phi && not (Solver.M.check s2 phi) in + FormulaOps.mintp ok rels [] + +(* Minimal type of elements in a structure which is part-positive. *) +let postp s rels els = + let app_rel_phi (st, fos, vs, i) e = + let r, v = "Elem" ^ (string_of_int i), Structure.elem_name st e in + (Structure.add_rel st r [|e|], + Formula.Rel (r, [|Formula.fo_var_of_string v|]) :: fos, v :: vs, i+1) in + let (struc, els_phis, vars, _) = List.fold_left app_rel_phi (s,[],[],0) els in + let neg_true = function Formula.Not _ -> Formula.And [] | x -> x in + let pos phi = + Formula.flatten (FormulaOps.map_to_literals neg_true (fun x->x) phi) in + let pos_ok phi = let psi = pos phi in if psi = Formula.And [] then false else + Solver.M.check struc (Formula.And (psi :: els_phis)) in + let ts = List.map pos (FormulaOps.mintp pos_ok rels vars) in + let tfvs = List.map (fun f -> (f,List.length (FormulaOps.free_vars f))) ts in + let maxfv = List.fold_left (fun m (_, x) -> max m x) 0 tfvs in + List.map fst (List.filter (fun (f, x) -> x = maxfv) tfvs) + +let tp_rule drels (left, right, delems) = + let not_drel (r,_) = not (List.mem r drels) in + let crels = List.filter not_drel (Structure.rel_signature left) in + if !debug_level > 0 then Printf.printf "CRels %i\n%!" (List.length crels); + let tp = postp left crels delems in + if !debug_level > 0 then + Format.printf "@[%a@]@ \n%!" Formula.fprint (Formula.And tp); + let cut s = List.fold_left Structure.del_elem s + (List.filter (fun e -> not (List.mem e delems)) (Structure.elements s)) in + (cut left, cut right, tp) + +let geom_rule drels (left, right, delems) = + let get_dim s e = (Structure.fun_val s "x" e, Structure.fun_val s "y" e) in + let rect s els = + let upd_rect (x1, y1, x2, y2) e = + let (x, y) = get_dim s e in (min x1 x, min y1 y, max x2 x, max y2 y) in + let (x, y) = get_dim s (List.hd els) in + List.fold_left upd_rect (x, y, x, y) (List.tl els) in + let in_rect s (x1, y1, x2, y2) e = + let (x, y) = get_dim s e in (x1 < x && x < x2 && y1 < y && y < y2) in + let (x1, y1, x2, y2) = rect left delems in + let r = (x1 -. 0.5, y1 -. 0.5, x2 +. 0.5, y2 +. 0.5) in + let els = List.filter (in_rect left r) (Structure.elements left) in + let new_els = List.filter (fun e -> not (List.mem e delems)) els in + if !debug_level > 0 then + Format.printf "%s\n%!" (String.concat ", " (List.map string_of_int els)); + let cut s = List.fold_left Structure.del_elem s + (List.filter (fun e -> not (List.mem e els)) (Structure.elements s)) in + let is_unary r = List.assoc r (Structure.rel_signature left) = 1 in + let un_drels = Aux.unique_sorted (List.filter is_unary drels) in + let un_opt_drels = List.map (fun r -> "_opt_" ^ r) un_drels in + let addopt s r = Structure.add_rels s r (List.map (fun e -> [|e|]) new_els) in + let addopts s = List.fold_left addopt s un_opt_drels in + let delopt s r = Structure.del_rels s r (List.map (fun e -> [|e|]) new_els) in + let delopts s = List.fold_left delopt s un_drels in + (addopts (delopts (cut left)), addopts (delopts (cut right)), []) + +let print_rule emb (name, (l, r, pre_l)) = + let emb_s = String.concat ", " (Aux.unique_sorted emb) in + let pre_s = Formula.sprint (Formula.And pre_l) in + let sprints () s = Structure.sprint s in + Format.sprintf "RULE %s:@ @[<2>%a@]@ ->@ @[<2>%a@]@ emb %s pre %s" + name sprints l sprints r emb_s pre_s + + (* Make a game from sequence of pictures. *) -let make_game ?(rels=[]) ?(offset=2) ?(threshold=70.) fname = +let make_game ?(rels=[]) ?(offset=2) ?(threshold=70.) ?(geom=true) fname = let formula_of_string s = FormulaParser.parse_formula Lexer.lex (Lexing.from_string s) in let get_struc fn = @@ -260,6 +328,41 @@ while Sys.file_exists (name ~suffix:"Win" !i) do win_strucs := get_struc (name ~suffix:"Win" !i) :: !win_strucs; incr i done; - (List.rev !seq_strucs, List.rev !win_strucs) in + (List.rev !seq_strucs, Array.of_list (List.rev !win_strucs)) in let (seq, wins) = read_strucs () in - Printf.sprintf "Read %i seq, %i win." (List.length seq) (List.length wins) + if seq = [] then failwith "Empty picture sequence for game play."; + let diff_struc (s, drels, prev) cur = + let dels, drels_l = List.split (Structure.diff_elems prev cur) in + ((prev, cur, dels) :: s, (List.concat drels_l) @ drels, cur) in + if !debug_level > 0 then Printf.printf "Diffstruc computed.\n%!"; + let (s, dr,_) = List.fold_left diff_struc ([],[],List.hd seq) (List.tl seq) in + let rules = if geom then List.rev_map (geom_rule dr) s else + List.rev_map (tp_rule dr) s in + let wi i = + formula_of_string (if i mod 2 = 0 then "not Win2()" else "not Win1()") in + let add_win i (l, r, pre) = (Printf.sprintf "Mv%i" i, (l, r, (wi i)::pre)) in + let wrs = Array.mapi (fun i r -> add_win i r) (Array.of_list rules) in + let emb = List.map fst (Structure.rel_signature (List.hd seq)) @ dr in + let rs = String.concat "\n" (List.map (print_rule emb) (Array.to_list wrs)) in + let allms = Array.to_list (Array.mapi (fun i _ -> i) (Array.of_list rules)) in + let (mvi1, mvi2) = List.partition (fun i -> i mod 2 = 0) allms in + let make_mv loc i = Printf.sprintf "[Mv%i -> %s]" i loc in + let mvs1 = String.concat "; " (List.map (make_mv "1") mvi1) in + let mvs2 = String.concat "; " (List.map (make_mv "0") mvi2) in + let pay1 = "PAYOFF :(Win1()) - :(Win2())" in + let pay2 = "PAYOFF :(Win2()) - :(Win1())" in + let loc0 = Printf.sprintf "LOC 0 {\n PLAYER 1 { %s }\n PLAYER 2 { %s }\n}" + (pay1 ^ "\n MOVES " ^ mvs1 ^ "\n") pay2 in + let loc1 = Printf.sprintf "LOC 1 {\n PLAYER 1 { %s }\n PLAYER 2 { %s }\n}" + pay1 (pay2 ^ "\n MOVES " ^ mvs2 ^ "\n") in + let model_s = Structure.sprint (List.hd seq) in + (* Printf.printf "DiffTp\n%!"; + FormulaOps.set_debug_level 1; + let w = difftp (Structure.rel_signature wins.(0)) wins.(0) wins.(1) in + if !debug_level > -1 then + Format.printf "@[%a@]@ \n%!" Formula.fprint (Formula.And w); + FormulaOps.set_debug_level 0; *) + let (win0, win1) = (Formula.Or [], Formula.Or []) in + let beg = Printf.sprintf "PLAYERS 1, 2\nREL Win0() = %s\nREL Win1() = %s" + (Formula.sprint win0) (Formula.sprint win1) in + Printf.sprintf "%s\n%s\n%s\n%s\nMODEL \n%s\n" beg rs loc0 loc1 model_s Modified: trunk/Toss/Server/Picture.mli =================================================================== --- trunk/Toss/Server/Picture.mli 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Server/Picture.mli 2011-05-23 01:32:57 UTC (rev 1455) @@ -51,4 +51,4 @@ (** Create a game from sequence of images. *) val make_game : ?rels : (string * string list * Formula.formula) list -> - ?offset : int -> ?threshold : float -> string -> string + ?offset : int -> ?threshold : float -> ?geom : bool -> string -> string Modified: trunk/Toss/Server/def_pics/Makefile =================================================================== --- trunk/Toss/Server/def_pics/Makefile 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Server/def_pics/Makefile 2011-05-23 01:32:57 UTC (rev 1455) @@ -14,7 +14,8 @@ Breakthrough06.ppm Breakthrough07.ppm Breakthrough08.ppm \ Breakthrough09.ppm Breakthrough10.ppm Breakthrough11.ppm \ Breakthrough12.ppm BreakthroughWin00.ppm BreakthroughWin01.ppm - ../../PictureTest.native -g Breakthrough > Breakthrough.toss + OCAMLRUNPARAM=b; export OCAMLRUNPARAM; ../../PictureTest.native \ + -g Breakthrough | sed "s/P1/W/g" | sed "s/P2/B/g" > Breakthrough.toss clean: rm -rf *.ppm *.png *.toss *~ Modified: trunk/Toss/Solver/Structure.ml =================================================================== --- trunk/Toss/Solver/Structure.ml 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Solver/Structure.ml 2011-05-23 01:32:57 UTC (rev 1455) @@ -54,7 +54,11 @@ let equal s1 s2 = (compare s1 s2 = 0) +let elements s = Elems.elements s.elements +let elem_nbr s el = StringMap.find el s.names +let elem_name s e = IntMap.find e s.inv_names + (* ----------------------- BASIC HELPER FUNCTIONS --------------------------- *) (* Number of tuples in a relation. *) @@ -342,19 +346,19 @@ (* ---------- REMOVING RELATION TUPLES AND ELEMENTS FROM A STRUCTURE -------- *) -(* Remove the tuple [tp] from relation [rn] in structure [struc]. May - raise [Not_found] if the tuple is not in the relation. *) +(* Remove the tuple [tp] from relation [rn] in structure [struc]. *) let del_rel struc rn tp = let del_rmap rmap = - StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap in + try StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap + with Not_found -> rmap in let new_rel = del_rmap struc.relations in let del_imap imap e = - IntMap.add e (Tuples.remove tp (IntMap.find e imap)) imap in + try IntMap.add e (Tuples.remove tp (IntMap.find e imap)) imap + with Not_found -> imap in let new_incidence = - let imap = - Array.fold_left del_imap (StringMap.find rn struc.incidence) tp in - StringMap.add rn imap struc.incidence in - { struc with relations = new_rel ; incidence = new_incidence } + let imap=Array.fold_left del_imap (StringMap.find rn struc.incidence) tp in + StringMap.add rn imap struc.incidence in + { struc with relations = new_rel ; incidence = new_incidence } (* Remove the tuples [tps] from relation [rn] in structure [struc]. *) let del_rels struc rn tps = @@ -1136,6 +1140,16 @@ true, "equal" with Diff_result expl -> false, expl +let diff_elems s1 s2 = + let rels, _ = List.split (rel_signature s1) in + let elems = Elems.elements s1.elements in + let inc s r e = try IntMap.find e (StringMap.find r s.incidence) with + Not_found -> Tuples.empty in + let diff_elem_rel e r = not (Tuples.equal (inc s1 r e) (inc s2 r e)) in + let diff_rels e = (e, List.filter (diff_elem_rel e) rels) in + List.filter (fun (_, rs) -> rs <> []) (List.rev_map diff_rels elems) + + (* -------------------- PARSER HELPERS -------------------- *) let is_uppercase c = c >= 'A' && c <= 'Z' Modified: trunk/Toss/Solver/Structure.mli =================================================================== --- trunk/Toss/Solver/Structure.mli 2011-05-22 14:52:01 UTC (rev 1454) +++ trunk/Toss/Solver/Structure.mli 2011-05-23 01:32:57 UTC (rev 1455) @@ -31,7 +31,11 @@ val compare : structure -> structure -> int val equal : structure -> structure -> bool +val elements : structure -> int list +val elem_nbr : structure -> string -> int +val elem_name : structure -> int -> string + (** {2 Basic helper functions} *) (** Size of a relation, i.e. number of tuples in it. *) @@ -126,6 +130,9 @@ ?cmp_funs:(float -> float -> bool) -> structure -> structure -> bool * string +(** Elements from s1 which differ in s2, with differing relation names. *) +val diff_elems : structure -> structure -> (int * string list) list + (** {2 Adding elements possibly with string names} *) @@ -197,18 +204,14 @@ (** {2 Removing relation tuples and elements from a structure} *) -(** Remove the tuple [tp] from relation [rn] in structure [struc]. May - raise [Not_found] if the tuple is not in the relation (but is not - guaranteed to). *) +(** Remove the tuple [tp] from relation [rn] in structure [struc]. *) val del_rel : structure -> string -> int array -> structure -(** Remove the tuples [tps] from relation [rn] in structure [struc]. May - raise [Not_found] if some tuple is not in the relation (but is not - guaranteed to). *) +(** Remove the tuples [tps] from relation [rn] in structure [struc]. *) val del_rels : structure -> string -> int array list -> structure -(** Remove all relations matching the predicate. By default, also remove - them from the signature. *) +(** Remove all relations matching the predicate. + By default, also remove them from the signature. *) val clear_rels : ?remove_from_sig:bool -> structure -> (string -> bool) -> structure This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |