[Toss-devel-svn] SF.net SVN: toss:[1455] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1455] trunk/Toss
|
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.
|
