[Toss-devel-svn] SF.net SVN: toss:[1688] trunk/Toss

[<luk...@us...>]

Revision: 1688
          http://toss.svn.sourceforge.net/toss/?rev=1688&view=rev
Author:   lukstafi
Date:     2012-03-09 22:49:49 +0000 (Fri, 09 Mar 2012)
Log Message:
-----------
Moving game simplification from working on state.struc to worknig on game.starting_struc.

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Arena.mli
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/GameSimpl.mli
    trunk/Toss/GGP/GameSimplTest.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/TranslateGameTest.ml
    trunk/Toss/Makefile

Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/Arena/Arena.ml	2012-03-09 22:49:49 UTC (rev 1688)
@@ -491,14 +491,14 @@
     else acc in
   acc
 
-let map_to_structures f (game, state) =
+let map_to_structures f game =
   {game with
-    rules = List.map (fun (rn, r) ->
-      rn, {r with ContinuousRule.discrete =
-          DiscreteRule.map_to_structures f r.ContinuousRule.discrete}
-    ) game.rules},
-  {state with
-    struc = f state.struc}
+    rules = List.map
+      (fun (rn, r) ->
+        rn, {r with ContinuousRule.discrete =
+            DiscreteRule.map_to_structures f r.ContinuousRule.discrete}
+      ) game.rules;
+    starting_struc = f game.starting_struc}
 
 let map_to_discrete f game =
   {game with

Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/Arena/Arena.mli	2012-03-09 22:49:49 UTC (rev 1688)
@@ -149,8 +149,8 @@
   (Formula.formula -> 'a -> 'a) -> game -> 'a -> 'a
 
 val map_to_structures :
-  (Structure.structure -> Structure.structure) -> game * game_state ->
-  game * game_state
+  (Structure.structure -> Structure.structure) -> game ->
+  game
 
 (** Map to the structure representation of discrete part of rules. *)
 val map_to_discrete :

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/GGP/GameSimpl.ml	2012-03-09 22:49:49 UTC (rev 1688)
@@ -203,10 +203,10 @@
       let nonspec = DiscreteRule.orig_rel_of rel in
       if nonspec = "" then rel else nonspec
 
-let simplify ?(keep_nonempty_predicates=true) (game, state) =
+let simplify ?(keep_nonempty_predicates=true) game =
   LOG 1 "GameSimpl: defined_rels = %s"
     (String.concat ", " (List.map fst game.Arena.defined_rels));
-  let struc = state.Arena.struc in
+  let struc = game.Arena.starting_struc in
   let signat = Structure.rel_signature struc in
   let nelems = Structure.nbr_elems struc in
   let tcard tups = Tups.cardinal tups in
@@ -381,8 +381,7 @@
   let game =
     Arena.map_to_formulas (FormulaMap.map_to_atoms repl_equiv_and_inv)
       game in
-  let state =
-    {state with Arena.struc = Structure.clear_rels struc removable} in
+  let struc = Structure.clear_rels struc removable in
   (* Also have to apply to LHS structures... Don't use
      {!ContinuousRule.apply_to_sides} as we don't need to
      recompile. *)
@@ -439,7 +438,7 @@
       (add_rels "")
       game Aux.Strings.empty in
   let used_rels = ref used_rels in
-  let struc = ref state.Arena.struc in
+  let struc = ref struc in
   let signat = ref signat in
   let glued = ref [] in              (* bindings introduced by [glue] *)
   let glued_inv = ref [] in          (* bingings introduced by [glue_inv] *)
@@ -628,7 +627,7 @@
     (String.concat "\n" (List.map (fun (k,v)->k^" = "^v) more_data));
   let game = {game with
     Arena.data = more_data @ game.Arena.data} in
-  let state = {state with Arena.struc = !struc} in
+  let struc = !struc in
   let signat = !signat in
   
   (* 
@@ -678,7 +677,9 @@
       else aux (now_used_in_def, defined_rels) in
     aux (used_in_def, game.Arena.defined_rels) in
   let used_rels = Aux.Strings.union used_in_def used_rels in
-  let game = {game with Arena.defined_rels = defined_rels} in
+  let game =
+    {game with Arena.defined_rels = defined_rels;
+      starting_struc = struc} in
   (* 4b, 4e *)
   let clear_rel rel =
     let rel = get_orig_if_special rel in
@@ -687,12 +688,12 @@
       DiscreteRule.special_rel_of rel = None &&      
       (not keep_nonempty_predicates ||
          (try List.assoc rel signat > 1 with Not_found -> false) ||
-         Structure.rel_size !struc rel = 0
+         Structure.rel_size struc rel = 0
       ) &&
         not (Aux.Strings.mem rel fluents) &&
         (not (Aux.Strings.mem rel used_rels) ||
            not (List.mem_assoc rel defined_rels) &&
-           Structure.rel_size !struc rel = 0) in
+           Structure.rel_size struc rel = 0) in
     if res then LOG 3 "GameSimpl: removing relation %s" rel;
     res in
   let remove_empty = FormulaMap.map_formula
@@ -702,12 +703,12 @@
           else Formula.Rel (rel, args)} in
   let game = Arena.map_to_formulas
     (!final_simplify -| remove_exist -| remove_empty) game in
-  let game, state =
+  let game =
     Arena.map_to_structures
       (fun struc ->
         let struc =
           List.fold_left (fun struc (rel, arity) ->
             Structure.add_rel_name rel arity struc) struc signat in
         Structure.clear_rels struc clear_rel)
-      (game, state) in
-  (game, state)
+      game in
+  game

Modified: trunk/Toss/GGP/GameSimpl.mli
===================================================================
--- trunk/Toss/GGP/GameSimpl.mli	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/GGP/GameSimpl.mli	2012-03-09 22:49:49 UTC (rev 1688)
@@ -12,5 +12,4 @@
 
 val simplify :
   ?keep_nonempty_predicates:bool ->
-  Arena.game * Arena.game_state ->
-  Arena.game * Arena.game_state
+  Arena.game -> Arena.game

Modified: trunk/Toss/GGP/GameSimplTest.ml
===================================================================
--- trunk/Toss/GGP/GameSimplTest.ml	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/GGP/GameSimplTest.ml	2012-03-09 22:49:49 UTC (rev 1688)
@@ -24,24 +24,10 @@
    {!GameSimpl.simplify} changes. *)
 let a () =
   let game_name = (* "breakthrough" *) (* "connect5" *) "tictactoe" in
-  let game = state_of_file ("./GGP/tests/"^game_name^"-raw.toss") in
-  AuxIO.printf "\nINPUT:\n%s\n%!" (Arena.state_str game);
+  let game, state = state_of_file ("./GGP/tests/"^game_name^"-raw.toss") in
+  AuxIO.printf "\nINPUT:\n%s\n%!" (Arena.state_str (game, state));
   let res = GameSimpl.simplify game in
-  let res_str = Arena.state_str res in
+  let state = {state with Arena.struc = res.Arena.starting_struc} in
+  let res_str = Arena.state_str (res, state) in
   AuxIO.output_file ~fname:("./GGP/tests/"^game_name^"-simpl.toss") res_str;
   AuxIO.printf "\nRESULT:\n%s\n%!" res_str
-
-
-let a () =
-  AuxIO.set_debug_level "GameSimpl" 5;
-  let connect5 = state_of_file "./GGP/tests/connect5-raw.toss" in
-  let res = GameSimpl.simplify connect5 in
-  let goal = state_of_file "./GGP/tests/connect5-simpl.toss" in
-  let res_str = Arena.state_str res in
-  AuxIO.output_file ~fname:"./GGP/tests/connect5-temp.toss" res_str;
-  let eq, msg = Arena.compare_diff goal res in
-  assert_bool
-    ("tests/connect5-raw.toss to tests/connect5-simpl.toss, see \
-          GGP/tests/connect5-temp.toss: "^msg)
-    eq;
-  Sys.remove "./GGP/tests/connect5-temp.toss"

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/GGP/TranslateGame.ml	2012-03-09 22:49:49 UTC (rev 1688)
@@ -2963,10 +2963,10 @@
     defined_rels = defined_rels;
     starting_struc = struc;
   } in
-  let result =
-    game, {Arena.struc = struc; history = []; time = 0.; cur_loc = 0} in
+  let state =
+    {Arena.struc = struc; history = []; time = 0.; cur_loc = 0} in
   LOG 4 "\n\ntranslate_game: before simplification --\n%s"
-    (Arena.sprint_state_full result);
+    (Arena.sprint_state_full (game, state));
 
   let tossrule_data = Aux.strmap_of_assoc tossrule_data in
   let playing_as =
@@ -2977,8 +2977,9 @@
     | None -> ()
     | Some game_name -> 
       AuxIO.output_file ~fname:("./GGP/tests/"^game_name^"-raw.toss")
-	(Arena.state_str result));
-  let result = GameSimpl.simplify result in
+	(Arena.state_str (game, state)));
+  let game = GameSimpl.simplify game in
+  let state = {state with Arena.struc = game.Arena.starting_struc} in
   let gdl_translation = {
     (* map between structure elements and their term representations;
        the reverse direction is by using element names *)
@@ -2997,16 +2998,15 @@
     | None -> ()
     | Some game_name ->
       AuxIO.output_file ~fname:("./GGP/tests/"^game_name^"-simpl.toss")
-	(Arena.state_str result)
+	(Arena.state_str (game, state))
   );
   LOG 2 "\n\ntranslate_game: simplified rel sizes --\n%s"
     (String.concat ", "(List.map (fun (rel,ar) ->
       rel^":"^string_of_int ar) (Structure.rel_sizes
-                                   (snd result).Arena.struc)));
+                                   game.Arena.starting_struc)));
   LOG 2 "\n\ntranslate_game: after simplification --\n%s"
-    (Arena.sprint_state_full result);
+    (Arena.sprint_state_full (game, state));
 
-  let game, state = result in
   let inl_game = Arena.map_to_formulas GameSimpl.remove_exist
     (inline_defined_rels game.Arena.defined_rels game) in
   gdl_translation, game, (inl_game, state)

Modified: trunk/Toss/GGP/TranslateGameTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateGameTest.ml	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/GGP/TranslateGameTest.ml	2012-03-09 22:49:49 UTC (rev 1688)
@@ -49,17 +49,18 @@
   let goal_name = game_name^"-simpl.toss" in
   (* let goal = state_of_file ("./GGP/tests/"^goal_name) in *)
   let goal_str = AuxIO.input_file ("./GGP/tests/" ^ goal_name) in
-  (* let resf = open_out ("./GGP/tests/"^game_name^"-temp.toss") in *)
+  (* * let resf = open_out ("./GGP/tests/"^game_name^"-temp.toss") in
+  * *)
   let res_str = Arena.state_str (r_game, r_struc) in
-  (* output_string resf res_str;
-  close_out resf; *)
+  (* * output_string resf res_str;
+  close_out resf; * *)
   (* let eq, msg = Arena.compare_diff goal res in *)
   let eq, msg = goal_str = res_str, "sorry, just comparing as strings" in
   assert_bool ("tests for " ^ game_name ^ " failed (" ^ goal_name ^ ")")
 	(* "GGP/examples/"^game_name^".gdl to GGP/tests/"^goal_name^
            ", see GGP/tests/"^game_name^"-temp.toss: "^msg *)
     eq;
-  (* Sys.remove ("./GGP/tests/"^game_name^"-temp.toss"); *)
+  (* * Sys.remove ("./GGP/tests/"^game_name^"-temp.toss"); * *)
   let rname = loc0_rule_name in
   let emb =
     Arena.matching_of_names res rname loc0_emb in
@@ -140,17 +141,18 @@
   let goal_name = game_name^"-simpl.toss" in
   (* let goal = state_of_file ("./GGP/tests/"^goal_name) in *)
   let goal_str = AuxIO.input_file ("./GGP/tests/"^goal_name) in
-  (* let resf = open_out ("./GGP/tests/"^game_name^"-temp.toss") in *)
+  (* * let resf = open_out ("./GGP/tests/"^game_name^"-temp.toss")
+        in * *)
   let res_str = Arena.state_str (r_game, r_struc) in
-  (* output_string resf res_str;
-  close_out resf; *)
+  (* * output_string resf res_str;
+  close_out resf; * *)
   (* let eq, msg = Arena.compare_diff goal res in *)
   let eq, msg = goal_str = res_str, "sorry, just comparing as strings" in
   assert_bool ("tests for " ^ game_name ^ " failed (" ^ goal_name ^ ")")
 	(*"GGP/examples/"^game_name^".gdl to GGP/tests/"^goal_name^
           ", see GGP/tests/"^game_name^"-temp.toss: "^msg*)
     eq;
-  (* Sys.remove ("./GGP/tests/"^game_name^"-temp.toss"); *)
+  (* * Sys.remove ("./GGP/tests/"^game_name^"-temp.toss"); * *)
   let embs = Array.map
     (fun (rname, emb) -> Arena.matching_of_names res rname emb)
     rules_and_embs in
@@ -237,7 +239,7 @@
           "control__BLANK_", "control__BLANK_"]
         ~loc1_noop:"noop" ~loc1_move:"(mark f g)" ()
     );
-(*
+(* *
   "breakthrough" >::
     (fun () ->
       game_test_case ~game_name:"breakthrough" ~player:"white"
@@ -349,7 +351,7 @@
           "control__BLANK_", "control__BLANK_"]
         ~loc1_noop:"noop" ~loc1_move:"(move 7 7 7 6)" ()
     );
-*)
+* *)
 ]
 
 let set_debug_level i =

Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile	2012-03-09 18:42:39 UTC (rev 1687)
+++ trunk/Toss/Makefile	2012-03-09 22:49:49 UTC (rev 1688)
@@ -114,6 +114,7 @@
 FormulaINCSatINC=MenhirLib,Formula
 FormulaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll
 SolverINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
+SolverINCNumINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
 SolverINCRealQuantElimINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
 ArenaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver
 PlayINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena
@@ -158,6 +159,8 @@
 	_build/$<
 	gprof _build/$< > $@.log
 
+pi_5000: Solver/Num/pi_num.native
+	time _build/Solver/Num/pi_num.native 5000
 
 # Formula tests
 FormulaTests: TossServer

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.