Thread: [Toss-devel-svn] SF.net SVN: toss:[1366] trunk/Toss (Page 5)

SourceForge Headquarters 1320 Columbia Street Suite 310 San Diego, CA 92101 +1 (858) 422-6466

Revision: 1366
          http://toss.svn.sourceforge.net/toss/?rev=1366&view=rev
Author:   lukstafi
Date:     2011-03-17 22:03:28 +0000 (Thu, 17 Mar 2011)

Log Message:
-----------
FormulaOps: Generalized maps over formulas and real expressions; fixed flatten_ands. Arena: print game data; refined game comparison. GameSimpl: fixed and improved reduction of equal and complement relations (stage 1); stage 3: intersections of relations and of a relation with inverse of another (remaining: handling of superfluous EQ equivalences).

Modified Paths:
--------------
    trunk/Toss/Arena/Arena.ml
    trunk/Toss/Arena/Arena.mli
    trunk/Toss/Arena/DiscreteRule.ml
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Formula/Formula.mli
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/GGP/GDL.ml
    trunk/Toss/GGP/GDLTest.ml
    trunk/Toss/GGP/GameSimpl.ml
    trunk/Toss/GGP/GameSimpl.mli
    trunk/Toss/GGP/GameSimplTest.ml
    trunk/Toss/GGP/tests/breakthrough-raw.toss
    trunk/Toss/GGP/tests/breakthrough-simpl.toss
    trunk/Toss/GGP/tests/connect5-raw.toss
    trunk/Toss/GGP/tests/connect5-simpl.toss
    trunk/Toss/Solver/Structure.ml
    trunk/Toss/Solver/Structure.mli

Modified: trunk/Toss/Arena/Arena.ml
===================================================================

--- trunk/Toss/Arena/Arena.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Arena/Arena.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -341,6 +341,11 @@
   Format.fprintf ppf "@[<1>PLAYERS@ %a@]@ "
     (Aux.fprint_sep_list "," Format.pp_print_string)
     (List.map fst (List.sort (fun (_,x) (_,y) -> x-y) player_names));
+  if data <> [] then
+    Format.fprintf ppf "@[<1>DATA@ %a@]@ "
+      (Aux.fprint_sep_list ","
+         (fun ppf (k,v) -> Format.fprintf ppf "@[<1>%s@,:@ %s@]" k v))
+      data;
   List.iter (fun (rname, r) ->
     Format.fprintf ppf "@[<1>RULE %s:@ %a@]@ " rname
       ContinuousRule.fprint r) rules;
@@ -420,6 +425,12 @@
           }}) game.rules},
   {state with
     struc = f state.struc}
+
+let map_to_discrete f game =
+  {game with
+    rules = List.map (fun (rn, r) ->
+      rn, {r with ContinuousRule.discrete =
+          f r.ContinuousRule.discrete}) game.rules}
       
 (* Compare two (game, state) pairs and explain the first difference
    met. Formulas and expressions are compared for syntactical
@@ -458,14 +469,38 @@
     let pnames2 = List.sort cmp_pn g2.player_names in
     if pnames1 <> pnames2 then
       raise (Diff_result "Game players are given in different order.");
-    let norm_loc loc =
-      {loc with
-        moves = List.sort Pervasives.compare loc.moves;
-        payoffs = Array.map (
-          FormulaOps.map_to_formulas_expr FormulaOps.flatten_formula)
-          loc.payoffs} in
-    if Array.map norm_loc g1.graph <> Array.map norm_loc g2.graph
-    then raise (Diff_result "Games have different graphs");
+    Array.iteri (fun i loc1 ->
+      let loc2 = g2.graph.(i) in
+      let dmoves1 = Aux.list_diff loc1.moves loc2.moves in
+      if dmoves1 <> [] then raise (Diff_result (
+        let label, dest = List.hd dmoves1 in
+        Printf.sprintf
+          "At location %d, only the first game has label %s->%d"
+          i label.rule dest));
+      let dmoves2 = Aux.list_diff loc2.moves loc1.moves in
+      if dmoves2 <> [] then raise (Diff_result (
+        let label, dest = List.hd dmoves1 in
+        Printf.sprintf
+          "At location %d, only the second game has label %s->%d"
+          i label.rule dest));
+      if loc1.player <> loc2.player then raise (Diff_result (
+        Printf.sprintf
+          "At location %d, the first game has player %d, second %d"
+          i loc1.player loc2.player));
+      Array.iteri (fun p poff1 ->
+        let poff1 =
+          FormulaOps.map_to_formulas_expr FormulaOps.flatten_formula
+            poff1 in
+        let poff2 =
+          FormulaOps.map_to_formulas_expr FormulaOps.flatten_formula
+            loc2.payoffs.(p) in
+        if poff1 <> poff2 then raise (Diff_result (
+          Printf.sprintf
+            "At location %d, payffs for player %d differ:\n%s\nvs.\n%s"
+            i p (Formula.real_str poff1)
+            (Formula.real_str poff2)));
+      ) loc1.payoffs
+    ) g1.graph;
     if List.sort Pervasives.compare g1.defined_rels <>
       List.sort Pervasives.compare g2.defined_rels
     then raise (Diff_result "Games have different defined relations");

Modified: trunk/Toss/Arena/Arena.mli
===================================================================
--- trunk/Toss/Arena/Arena.mli	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Arena/Arena.mli	2011-03-17 22:03:28 UTC (rev 1366)
@@ -116,6 +116,10 @@
   (Structure.structure -> Structure.structure) -> game * game_state ->
   game * game_state
 
+(** Map to the structure representation of discrete part of rules. *)
+val map_to_discrete :
+  (DiscreteRule.rule -> DiscreteRule.rule) -> game -> game
+
 (** Compare two (game, state) pairs and explain the first difference
     met. Formulas and expressions are compared for syntactical
     equality. Players need to be given in the same order. Data is

Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Arena/DiscreteRule.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -425,7 +425,7 @@
       | None -> false
       | Some sp ->
         sp = "new" || sp = "del" || sp = "right" || sp = "lhs") in
-  (* We name the new elements with their rule correspondents (note
+  (* We name the matched elements with their rule correspondents (note
      that in the nonstruct case the LHS and RHS elements have the same
      names due to renaming during rule compilation). *)
   let model = 
@@ -920,6 +920,17 @@
     | phi -> Right phi) conjs in
   let lhs_extracted = posi @ nega in
   let precond = Formula.And conjs in
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf
+      "translate_from_precond:\nposi=\n%s\nnega=\n%s\nprecond=\n%s\n%!"
+      (Formula.sprint (Formula.And (List.map (fun (rel,args) ->
+        Formula.Rel (rel,args)) posi)))
+      (Formula.sprint (Formula.And (List.map (fun (rel,args) ->
+        Formula.Rel (rel,args)) nega)))
+      (Formula.sprint precond)
+  );
+  (* }}} *)
   let fvars = FormulaOps.free_vars precond in
   let local_vars =
     List.filter (fun v->

Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Formula/Formula.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -106,6 +106,10 @@
 ;;
 
 
+let is_atom = function
+    Rel _ | Eq _ | In _ | RealExpr _ -> true
+  | _ -> false
+
 (* Helper power function, used in parser. *)
 let rec pow p n = 
   if n = 0 then Const 1. else if n = 1 then p else Times (p, pow p (n-1))

Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Formula/Formula.mli	2011-03-17 22:03:28 UTC (rev 1366)
@@ -70,6 +70,7 @@
 
 val compare : formula -> formula -> int
 
+val is_atom : formula -> bool
 
 (** {2 Printing Functions} *)
 

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -123,6 +123,72 @@
   | Rel _ | Eq _ | In _ -> true
   | _ -> false
 
+(* Generalized map over formula and real expression types. *)
+type formula_and_expr_map = {
+  map_Rel : string -> fo_var array -> formula;
+  map_Eq : fo_var -> fo_var -> formula;
+  map_In : fo_var -> mso_var -> formula;
+  map_RealExpr : real_expr -> sign_op -> formula;
+  map_Not : formula -> formula;
+  map_And : formula list -> formula;
+  map_Or : formula list -> formula;
+  map_Ex : var list -> formula -> formula;
+  map_All : var list -> formula -> formula;
+
+  map_RVar : string -> real_expr;
+  map_Const : float -> real_expr;
+  map_Times : real_expr -> real_expr -> real_expr;
+  map_Plus : real_expr -> real_expr -> real_expr;
+  map_Fun : string -> fo_var -> real_expr;
+  map_Char : formula -> real_expr;
+  map_Sum : fo_var list -> formula -> real_expr -> real_expr
+}
+
+let identity_map = {
+  map_Rel = (fun rel args -> Rel (rel, args));
+  map_Eq = (fun x y -> Eq (x, y));
+  map_In = (fun x ys -> In (x, ys));
+  map_RealExpr = (fun expr sign -> RealExpr (expr, sign));
+  map_Not = (fun phi -> Not phi);
+  map_And = (fun conjs -> And conjs);
+  map_Or = (fun disjs -> Or disjs);
+  map_Ex = (fun vs phi -> Ex (vs, phi));
+  map_All = (fun vs phi -> All (vs, phi));
+
+  map_RVar = (fun v -> RVar v);
+  map_Const = (fun c -> Const c);
+  map_Times = (fun expr1 expr2 -> Times (expr1, expr2));
+  map_Plus = (fun expr1 expr2 -> Plus (expr1, expr2));
+  map_Fun = (fun f v -> Fun (f, v));
+  map_Char = (fun phi -> Char phi);
+  map_Sum = (fun vs guard expr -> Sum (vs, guard, expr))
+}
+
+let rec map_formula gmap = function
+  | Rel (rel, args) -> gmap.map_Rel rel args
+  | Eq (x, y) -> gmap.map_Eq x y
+  | In (x, ys) -> gmap.map_In x ys
+  | RealExpr (expr, sign) ->
+    gmap.map_RealExpr (map_real_expr gmap expr) sign
+  | Not phi -> gmap.map_Not (map_formula gmap phi)
+  | And conjs -> gmap.map_And (List.map (map_formula gmap) conjs)
+  | Or disjs -> gmap.map_Or (List.map (map_formula gmap) disjs)
+  | Ex (vs, phi) -> gmap.map_Ex vs (map_formula gmap phi)
+  | All (vs, phi) -> gmap.map_All vs (map_formula gmap phi)
+
+and map_real_expr gmap = function
+  | RVar v -> gmap.map_RVar v
+  | Const c -> gmap.map_Const c
+  | Times (expr1, expr2) ->
+    gmap.map_Times (map_real_expr gmap expr1) (map_real_expr gmap expr2)
+  | Plus (expr1, expr2) ->
+    gmap.map_Plus (map_real_expr gmap expr1) (map_real_expr gmap expr2)
+  | Fun (f, v) -> gmap.map_Fun f v
+  | Char phi -> gmap.map_Char (map_formula gmap phi)
+  | Sum (vs, guard, expr) ->
+    gmap.map_Sum vs (map_formula gmap guard) (map_real_expr gmap expr)
+
+
 (* Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
    formula. Preserves order of subformulas. *)
 let rec map_to_literals f g = function
@@ -534,10 +600,6 @@
 (* Simplify.                                                                 *)
 (* ------------------------------------------------------------------------- *)
 
-let is_atom = function
-    Rel _ | Eq _ | In _ | RealExpr _ -> true
-  | _ -> false
-
 let str_contains c s =
   try let _ = String.index s c in true with Not_found -> false
 
@@ -694,43 +756,37 @@
     if simp_p = p && simp_q = q then Times (p, q) else 
       simplify_re ~do_pnf ~do_formula (Times (simp_p, simp_q))
 
+
 (* Flatten "and"s and "or"s in a formula --
    i.e. associativity. Remove double negation along the way. *)
-let  rec flatten_formula phi =
-  let rec flat_and = function
-    | And conjs -> Aux.concat_map flat_and conjs
-    | phi ->
-      match flatten_formula phi with
-        | And _ as phi -> flat_and phi
-        | phi -> [phi] in
-  let rec flat_or = function
-    | Or disjs -> Aux.concat_map flat_or disjs
-    | phi ->
-      match flatten_formula phi with
-        | Or _ as phi -> flat_or phi
-        | phi -> [phi] in
-  match phi with
-    | Or [phi] -> flatten_formula phi
-    | And [phi] -> flatten_formula phi
-    | Or _ -> Or (flat_or phi)
-    | And _ -> And (flat_and phi)
-    | All (vs, phi) -> All (vs, flatten_formula phi)
-    | Ex (vs, phi) -> Ex (vs, flatten_formula phi)
-    | Not (Not phi) -> flatten_formula phi
-    | Not phi -> Not (flatten_formula phi)
-    | (Rel _ | Eq _ | In _ | RealExpr _) as atom -> atom
+let flatten_formula =
+  let flat_and = function And conjs -> conjs | phi -> [phi] in
+  let flat_or = function Or disjs -> disjs | phi -> [phi] in
+  map_formula {identity_map with
+    map_And = (function
+      | [conj] -> conj
+      | conjs -> And (Aux.concat_map flat_and conjs));
+    map_Or = (function
+      | [disj] -> disj
+      | disjs -> Or (Aux.concat_map flat_or disjs));
+    map_Not = (function Not phi -> phi | phi -> Not phi)}
 
-let rec flatten_ors = function
-  | Or disjs -> Aux.concat_map flatten_ors disjs
+let rec flatten_or = function
+  | Or disjs -> Aux.concat_map flatten_or disjs
+  | Not (Not phi) | Not (And [Not phi]) | Not (Or [Not phi]) ->
+    flatten_or phi
   | phi -> [phi]
 
 (* Formula as a list of conjuncts, with one level of distributing
    negation over disjunction and pushing quantifiers inside. *)
 let rec flatten_ands = function
   | And conjs -> Aux.concat_map flatten_ands conjs
+  | Or [phi] -> flatten_ands phi
+  | Not (And [phi]) -> flatten_ands (Not phi)
   | Not (Or disjs) ->
-    List.map (fun d -> Not d)
-      (Aux.concat_map flatten_ors disjs)
+    Aux.concat_map flatten_ands
+      (List.map (fun d -> Not d)
+         (Aux.concat_map flatten_or disjs))
   | All (vs, phi) ->
     List.map (fun phi -> All (vs, phi)) (flatten_ands phi)
   | Ex (vs, phi) as arg ->
@@ -742,6 +798,7 @@
         let bound_phi = match bound_conjs with
           | [phi] -> phi | _ -> And bound_conjs in
         free_conjs @ [Ex (vs, bound_phi)])
+  | Not (Not phi) -> flatten_ands phi
   | phi -> [phi]
 
 (* Simplify the formula by removing relational literals, depending on
@@ -750,7 +807,9 @@
    track of the sign (variance) of a position. (Does not descend the
    real part currently.) [implies] is applied to atoms only. Repeat
    the removal till fixpoint since it can "unpack" literals e.g. from
-   conjunctions to disjunctions. *)
+   conjunctions to disjunctions.
+
+   TODO: traverse the real part too. *)
 let remove_redundant ?(implies=(=)) phi =
   let implied_by x y = implies y x in
   let literal neg phis =

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-03-17 22:03:28 UTC (rev 1366)
@@ -19,6 +19,34 @@
 
 (** {2 Mapping to atoms and variable substitution.} *)
 
+(** Generalized map over formula and real expression types. *)
+type formula_and_expr_map = {
+  map_Rel : string -> fo_var array -> formula;
+  map_Eq : fo_var -> fo_var -> formula;
+  map_In : fo_var -> mso_var -> formula;
+  map_RealExpr : real_expr -> sign_op -> formula;
+  map_Not : formula -> formula;
+  map_And : formula list -> formula;
+  map_Or : formula list -> formula;
+  map_Ex : var list -> formula -> formula;
+  map_All : var list -> formula -> formula;
+
+  map_RVar : string -> real_expr;
+  map_Const : float -> real_expr;
+  map_Times : real_expr -> real_expr -> real_expr;
+  map_Plus : real_expr -> real_expr -> real_expr;
+  map_Fun : string -> fo_var -> real_expr;
+  map_Char : formula -> real_expr;
+  map_Sum : fo_var list -> formula -> real_expr -> real_expr
+}
+
+(** Identity map to be refined using the [with] clause. *)
+val identity_map : formula_and_expr_map
+
+(** Map through the structure adjusting subformulas/subexpressions. *)
+val map_formula : formula_and_expr_map -> formula -> formula
+val map_real_expr : formula_and_expr_map -> real_expr -> real_expr
+
 (** Map [f] to all literals (i.e. atoms or not(atom)'s) in the given
    formula. Preserves order of subformulas. *)
 val map_to_literals : (formula -> formula) -> (real_expr -> real_expr) -> 

Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/GGP/GDL.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -540,7 +540,7 @@
 (** Generate all tuples for equivalences, to faciliate further
     transformations of formulas in the game definition (outside of
     translation). *)
-let equivalences_all_tuples = ref false (* true *)
+let equivalences_all_tuples = ref (* false *) true
 
 open Aux.BasicOperators
 

Modified: trunk/Toss/GGP/GDLTest.ml
===================================================================
--- trunk/Toss/GGP/GDLTest.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/GGP/GDLTest.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -140,9 +140,9 @@
     | None -> ()
         
 let a () =
-  GDL.debug_level := 4;
-  GameSimpl.debug_level := 4;
-  DiscreteRule.debug_level := 4;
+  (* GDL.debug_level := 4; *)
+  (* GameSimpl.debug_level := 4; *)
+  (* DiscreteRule.debug_level := 4; *)
   let breakthrough = load_rules "./GGP/examples/breakthrough.gdl" in
   let connect5 = load_rules "./GGP/examples/connect5.gdl" in
   let tictactoe = load_rules "./GGP/examples/tictactoe.gdl" in

Modified: trunk/Toss/GGP/GameSimpl.ml
===================================================================
--- trunk/Toss/GGP/GameSimpl.ml	2011-03-17 18:58:07 UTC (rev 1365)
+++ trunk/Toss/GGP/GameSimpl.ml	2011-03-17 22:03:28 UTC (rev 1366)
@@ -5,17 +5,28 @@
 
     The simplification of structures, associated formulas and Toss
     rules is specified by transformations described below. Rules can
-    be refined or new rules added to each stage.
+    be refined or new simplification rules added to each stage.
 
-    (1) Identify relations in the structure that are not fluents nor
+    TODO: use [DiscreteRule.special_rel_of rel = Some "opt"]
+    instead of [DiscreteRule.special_rel_of rel <> None]? (To protect
+    against GDL using identifiers starting with underscore.)
+
+    (1) Reduce equivalent or complement relations.
+
+    (1a) If [introduce_complement] is on, for each (unary) predicate
+    that does not have its complement in the structure, introduce the
+    complement.
+
+    (1b) Identify relations in the structure that are not fluents nor
     defined relations and that are equal to or are complements of
     other relations in the structure. Select a single relation / a
     predicate (called "the original" below), that is smaller than its
-    complement (if the complement is in the signature), and replace
-    all selected relations with it (or its negation), in all formulas
-    of the definition. Remove the other relations from the structure.
+    complement (if the complement is in the signature, but see (1a)),
+    and replace all selected relations with it (or its negation), in
+    all formulas of the definition. Remove the other relations from
+    the structure.
 
-    (1a) We need to update LHS structures of rules (for presentation
+    (1c) We need to update LHS structures of rules (for presentation
     and game modification purposes, since the simple transformation
     above of the "embedding formula" suffices for the "compiled" rule
     representation). Replace the identified relations in the "embedded
@@ -23,9 +34,9 @@
     that occur positively in the LHS and are complements of their
     original. Derive all the tuples of embedded relations that are
     required to be absent for a match (not present, even optionally,
-    in the LHS). (1a1) Rename relations equivalent to their
-    originals. (1a2) Remove the non-optional tuples for relations that
-    are complements of their originals and (1a3) add tuples of
+    in the LHS). (1c1) Rename relations equivalent to their
+    originals. (1c2) Remove the non-optional tuples for relations that
+    are complements of their originals and (1c3) add tuples of
     originals that are complements of relations that are required to
     be absent.
 
@@ -35,18 +46,43 @@
     that are weaker/stronger than another present over the same tuple
     in the given conjunction/disjunction.
 
-    (3) For each pair of static unary predicates with nonempty
-    intersection, introduce new predicate for their conjunction. For
-    each pair of static binary predicates, introduce two new
-    predicates: one for their conjunction and the other for
-    conjunction of one of the predicates and the inverse of the other.
+    (3) Add intersections of non-fluent relations to the structure
+    when they co-occur in formulas. For binary relations, also add
+    intersections of a relation and an inverse of another.
 
-    (3a) Replace each conjunction of pair of unary/binary predicates
-    over the same variables, with one of introduced predicates. For
-    several possibilities of replacement pick one arbitrarily
-    (currently, in the order of occurrence in the formula).
+    (3a) Eliminate conjoined static (non-fluents and not defined)
+    relations in formulas that are applied to the same arguments and
+    introduce a new relation for their conjunction (by intersetcting
+    their tuples).
 
-    (4) Remove from the structure relations that are no longer used.
+    (3b) For binary static relations, collect pairs such that one
+    relation is applied to arguments in reverse order than the other
+    one, and introduce a new relation for intersection of one with the
+    inverse of the other.
+
+    (3c) Repeat till no more atoms can be glued in this way.
+
+    (3d) Since too long names would be unreadable anyway, introduce
+    fresh relation names for the glued relations and remember the
+    correspondence in game data.
+
+    (3e) The eliminated co-occurrences are relevant only for tuples
+    present in rewrite rules (LHS structures), not for absent ones
+    (since these are conjoined negations). Replace them in the LHS
+    structures as in (3a)-(3b), but only if all of replaced relations
+    occur as non-embedded (i.e. "tau_h") (since embedded relations
+    will have reuired-to-be-absent occurrences, and these cannot be
+    handled by conjoining).
+
+    TODO or warning: with the current specification (and
+    implementation), inconsistency between the structure-based
+    representation and the "embedding formula"-based representation of
+    discrete rules is possible: when the optimization replaces (in the
+    embedding formula) a conjunction of relations considered embedded.
+
+    (4) Update rewrite rule signatures to contain all introduced
+    relations. Remove from the structures relations that are no longer
+    used.
 *)
 
 open Formula
@@ -54,6 +90,7 @@
 
 let debug_level = ref 0
 
+let introduce_complement = ref true
 
 
 (* Collect universally quantified subformulas and compute the size of
@@ -80,12 +117,13 @@
   let trunk, univs = separate_univ phi in
   trunk - List.fold_left (+) 0 (List.map FormulaOps.size univs)
 
+module Tups = Structure.Tuples
   
-let simplify ?(join_rel_names=fun x _ -> x) (game, state) =
+let simplify (game, state) =
   let struc = state.Arena.struc in
   let signat = Structure.rel_signature struc in
   let nelems = Structure.Elems.cardinal struc.Structure.elements in
-  let tcard tups = Structure.Tuples.cardinal tups in
+  let tcard tups = Tups.cardinal tups in
   let fluents =
     Aux.unique_sorted
       (Aux.concat_map (fun (_,r) ->
@@ -97,7 +135,71 @@
       (String.concat ", " fluents)
   );
   (* }}} *)
-  (* prepare for (1) and (2) *)
+  (* 1 *)
+  let add_rel rel acc =
+    match rel with
+      | Rel (rel,_) -> Aux.Strings.add rel acc
+      | _ -> acc in
+  let used_rels =
+    Arena.fold_over_formulas ~include_defined_rels:false
+      (FormulaOps.fold_over_atoms add_rel)
+      game Aux.Strings.empty in
+  let complemented = ref [] in
+  let predicate_tups =
+    Structure.Elems.fold (fun e tups -> Tups.add [|e|] tups)
+      struc.Structure.elements Tups.empty in
+  let struc = ref struc in
+  let signat = ref signat in
+  let used_rels = ref used_rels in
+  let complements =
+    List.fold_left (fun table (rel,arity) ->
+      let rel_tups =
+        Structure.StringMap.find rel !struc.Structure.relations in
+      let ntups = tcard rel_tups in
+      let crel =
+        Structure.StringMap.fold (fun rel2 rel2_tups crel ->
+          let arity2 = List.assoc rel2 !signat in
+          if crel <> None || arity2 <> arity then crel
+          else
+            let ntups2 = tcard rel2_tups in
+            if ntups >= ntups2 &&
+              ntups + ntups2 = Aux.int_pow nelems arity &&
+                not (List.mem rel2 fluents) &&
+                Tups.is_empty (Tups.inter rel_tups rel2_tups)
+            then (
+              (* {{{ log entry *)
+              if !debug_level > 3 then (
+                Printf.printf "Complements: rel=%s; crel=%s\n%!" rel rel2
+              );
+              (* }}} *)
+              Some rel2
+            ) else None
+        ) !struc.Structure.relations None in
+      let crel =
+        if not !introduce_complement || arity <> 1 ||
+          crel <> None || ntups <= nelems / 2
+        then crel
+        else
+           (* 1a *)
+           let crel =
+             Aux.not_conflicting_name ~truncate:true !used_rels "C" in
+           (* {{{ log entry *)
+           if !debug_level > 3 then (
+             Printf.printf "Complemented: crel=%s\n%!" crel
+           );
+           (* }}} *)
+           complemented := (crel, rel) :: !complemented;
+           struc := Structure.add_rels !struc crel
+             (Tups.elements (Tups.diff predicate_tups rel_tups));
+           signat := (crel, arity) :: !signat;
+           used_rels := Aux.Strings.add crel !used_rels;
+           Some crel in
+      Aux.StrMap.add rel crel table
+    ) Aux.StrMap.empty !signat in
+  let struc = !struc in
+  let signat = !signat in
+  let complements rel = Aux.StrMap.find rel complements in
+  (* prepare for (1bc) and (2) *)
   let subset_table =
     List.fold_left (fun table (rel,arity) ->
       let rel_tups =
@@ -105,7 +207,7 @@
       let row =
         List.fold_left (fun row (rel2,arity2) ->
           if arity2 = arity &&
-            Structure.Tuples.subset rel_tups
+            Tups.subset rel_tups
             (Structure.StringMap.find rel2 struc.Structure.relations)
           then Aux.Strings.add rel2 row
           else row
@@ -122,42 +224,22 @@
   (* }}} *)
   let included_in rel1 rel2 =
     Aux.Strings.mem rel2 (Aux.StrMap.find rel1 subset_table) in
-  let compl_table =
-    List.fold_left (fun table (rel,arity) ->
-      let rel_tups =
-        Structure.StringMap.find rel struc.Structure.relations in
-      let row =
-        List.fold_left (fun row (rel2,arity2) ->
-          if arity2 <> arity then row
-          else
-            let rel2_tups =
-              Structure.StringMap.find rel2 struc.Structure.relations in
-            let ntups = tcard rel_tups and ntups2 = tcard rel2_tups in
-            if ntups >= ntups2 &&
-              ntups + ntups2 = Aux.int_pow nelems arity &&
-                Structure.Tuples.is_empty
-                (Structure.Tuples.inter rel_tups rel2_tups)
-            then Aux.Strings.add rel2 row
-            else row
-        ) Aux.Strings.empty signat in
-      Aux.StrMap.add rel row table
-    ) Aux.StrMap.empty signat in
-  let complement rel1 rel2 =
-    Aux.Strings.mem rel2 (Aux.StrMap.find rel1 compl_table) in
-  (* 1 *)
+  (* 1b *)
   let equivalent =
     List.map (fun (rel1, arity) ->
-      try
-        let rel2, _ =
-          List.find (fun (rel2, arity2) ->
-            arity = arity2 &&
-              not (List.mem rel2 fluents ||
-                     List.mem_assoc rel2 game.Arena.defined_rels) &&
-              (complement rel1 rel2 ||
-                 (included_in rel1 rel2 && included_in rel2 rel1))
-          ) signat in
-        rel1, (rel2, complement rel1 rel2)
-      with Not_found -> rel1, (rel1, false)
+      match complements rel1 with
+        | Some rel2 -> rel1, (rel2, true)
+        | None ->
+          try
+            let rel2, _ =
+              List.find (fun (rel2, arity2) ->
+                arity = arity2 &&
+                  not (List.mem rel2 fluents ||
+                         List.mem_assoc rel2 game.Arena.defined_rels) &&
+                  included_in rel1 rel2 && included_in rel2 rel1
+              ) signat in
+            rel1, (rel2, false)
+          with Not_found -> rel1, (rel1, false)
     ) signat in
   let removable rel =
     let spec = DiscreteRule.special_rel_of rel in
@@ -165,6 +247,7 @@
       match spec with
         | None -> rel
         | Some spec -> DiscreteRule.orig_rel_of rel in
+    rel <> "" &&
     not (List.mem rel fluents) &&
       not (List.mem_assoc rel game.Arena.defined_rels) &&
       not (List.exists (fun (_,(rel2,_)) -> rel2=rel) equivalent) &&
@@ -195,7 +278,7 @@
   (* Also have to apply to LHS structures... Don't use
      {!ContinuousRule.apply_to_sides} as we don't need to
      recompile. *)
-  (* 1a *)
+  (* 1c *)
   let map_rhs rhs = Structure.clear_rels rhs removable in
   let game =
     {game with
@@ -216,9 +299,9 @@
                 let tups =
                   try Structure.StringMap.find rel
                         lhs_struc.Structure.relations
-                  with Not_found -> Structure.Tuples.empty in
+                  with Not_found -> Tups.empty in
                 if removable rel &&
-                  not (Structure.Tuples.is_empty tups) &&
+                  not (Tups.is_empty tups) &&
                   snd (List.assoc rel equivalent) (* is complement *)
                 then (
                   (* {{{ log entry *)
@@ -236,10 +319,10 @@
             Aux.unique_sorted (kept_emb_rels @ added_emb_rels) in
           let new_emb_rels =
             Aux.list_diff added_emb_rels kept_emb_rels in
-          let ltups = Structure.Tuples.elements in
+          let ltups = Tups.elements in
           let lhs_neg_tups =
             r.ContinuousRule.compiled.DiscreteRule.lhs_neg_tups in
-          (* 1a1: renaming removable relations to their originals *)
+          (* 1c1: renaming removable relations to their originals *)
           let lhs_struc =
             Structure.StringMap.fold (fun rel tups lhs_struc ->
               let spec = DiscreteRule.special_rel_of rel in
@@ -254,13 +337,13 @@
                   match spec with
                     | None -> orig
                     | Some spec -> "_"^spec^"_"^orig in
-                if not neg              (* 1a1 *)
-                  || (neg && spec = Some "opt") (* not-1a2 *)
+                if not neg              (* 1c1 *)
+                  || (neg && spec = Some "opt") (* not-1c2 *)
                 then
                   Structure.add_rels lhs_struc...
 
[truncated message content]

Thread: [Toss-devel-svn] SF.net SVN: toss:[1366] trunk/Toss (Page 5)

toss-devel-svn