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

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

Revision: 1614
          http://toss.svn.sourceforge.net/toss/?rev=1614&view=rev
Author:   lukstafi
Date:     2011-10-23 20:28:50 +0000 (Sun, 23 Oct 2011)
Log Message:
-----------
GDL translation: small fix to translating as <not equal>.

Modified Paths:
--------------
    trunk/Toss/GGP/GDL.mli
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateGame.ml
    trunk/Toss/GGP/tests/pacman3p-raw.toss
    trunk/Toss/GGP/tests/pacman3p-simpl.toss
    trunk/Toss/www/reference/reference.tex

Modified: trunk/Toss/GGP/GDL.mli
===================================================================
--- trunk/Toss/GGP/GDL.mli	2011-10-23 18:48:09 UTC (rev 1613)
+++ trunk/Toss/GGP/GDL.mli	2011-10-23 20:28:50 UTC (rev 1614)
@@ -68,6 +68,8 @@
 type substitution = (string * term) list
 
 val unify : substitution -> term list -> term list -> substitution
+val unify_args :
+  ?sb:substitution -> term array -> term array -> substitution
 (** Match terms on the left to ground terms on the right, ignoring
     [Const "_BLANK_"] on the right. *)
 val match_nonblank : substitution -> term list -> term list -> substitution

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-10-23 18:48:09 UTC (rev 1613)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-10-23 20:28:50 UTC (rev 1614)
@@ -388,7 +388,9 @@
   | _ -> false
 
 (* A relation defined by a disjunction of differences on all paths of
-   a state term. *)
+   a state term. Disjunctions can have common part, which is
+   identified by unification of clause heads alone (no matching of
+   local variables). *)
 let is_distinctcell c_paths partition cls =
   try
     List.iter (fun (_, body) ->
@@ -426,6 +428,25 @@
         pv1 = pv2)
       v1
   with Not_found -> false  
+
+let try_if_common cls =
+  try
+    let bodies =  List.map
+      (fun (_, body) -> List.filter (not -| distinct_lit) body)
+      cls in
+    let acc_args, all_args = match List.map fst cls with
+      | hd::tl -> hd, tl | _ -> assert false in
+    let sb, acc_args = List.fold_left
+      (fun (sb, acc_args) args ->
+        let sb = unify_args ~sb args acc_args in
+        sb, Array.map (subst sb) acc_args)
+      ([], acc_args) all_args in
+    let bodies = List.map
+      (subst_literals sb -| Aux.unique_sorted) bodies in
+    (match Aux.unique_sorted bodies with
+      | [body] -> true, [acc_args, body]
+      | _ -> raise Not_found)
+  with Not_found | Invalid_argument _ -> false, cls
   
 
 let build_defrels data clauses =
@@ -449,9 +470,8 @@
       let distinctcell, r_clauses =
         if d_arity = 2 && (* DEBUG *) drel = "distinctcell" &&
           is_distinctcell data.c_paths partition r_clauses
-        then true,
-          List.map (fun (args, body) ->
-            args, List.filter (not -| distinct_lit) body) r_clauses
+        then
+          try_if_common r_clauses
         else false, r_clauses in
       (* {{{ log entry *)
       if !debug_level > 3 then (

Modified: trunk/Toss/GGP/TranslateGame.ml
===================================================================
--- trunk/Toss/GGP/TranslateGame.ml	2011-10-23 18:48:09 UTC (rev 1613)
+++ trunk/Toss/GGP/TranslateGame.ml	2011-10-23 20:28:50 UTC (rev 1614)
@@ -17,23 +17,10 @@
     defined relation: a Toss defined relation (i.e. does not normally
     occur in the structure)
 
-    TODO: filter out legal tuples that are not statically satisfiable
-
     TODO: perform "fluent path prediate inversion" by transforming
     single-argument state terms into two arguments of a "value" state
     term.
 
-    TODO-FIXME: add "preserved fluents" check, make rewrite rules
-    remove fluents that are not covered by any frame clause. (Erasure
-    clauses are only built from frame clauses, i.e. they handle only
-    fluents that are preserved elsewhere.) Unfortunately it cannot be
-    assumed that an element holding a non-preserved fluent is
-    different from an element where the fluent is to be added! Extract
-    one variable under non-preserved fluent from the precondition to
-    LHS, if present, and duplicate the rewrite rule generating one
-    copy where the variable is equal to the "target" variable (head of
-    the "next" clause).
-
     TODO-FIXME: limit translation as concurrent games to cases where
     rules do not check fluents affected by other rules to be performed
     concurrently.

Modified: trunk/Toss/GGP/tests/pacman3p-raw.toss
===================================================================
--- trunk/Toss/GGP/tests/pacman3p-raw.toss	2011-10-23 18:48:09 UTC (rev 1613)
+++ trunk/Toss/GGP/tests/pacman3p-raw.toss	2011-10-23 20:28:50 UTC (rev 1614)
@@ -1,15 +1,10 @@
 REL distinctcell(v0, v1) =
  (not v0 = v1 and
-  (ex location__BLANK__x33_y33, location__BLANK__x34_y34
-    (v0 = location__BLANK__x33_y33 and v1 = location__BLANK__x34_y34 and
-     cell(location__BLANK__x33_y33) and cell(location__BLANK__x34_y34) and
-      location__BLANK___BLANK___BLANK_(location__BLANK__x34_y34) and
-       location__BLANK___BLANK___BLANK_(location__BLANK__x33_y33)) or
-   ex location__BLANK__x35_y35, location__BLANK__x36_y36
-    (v0 = location__BLANK__x35_y35 and v1 = location__BLANK__x36_y36 and
-     cell(location__BLANK__x35_y35) and cell(location__BLANK__x36_y36) and
-      location__BLANK___BLANK___BLANK_(location__BLANK__x36_y36) and
-       location__BLANK___BLANK___BLANK_(location__BLANK__x35_y35))))
+  ex location__BLANK__x33_y33, location__BLANK__x34_y34
+   (v0 = location__BLANK__x33_y33 and v1 = location__BLANK__x34_y34 and
+    cell(location__BLANK__x33_y33) and cell(location__BLANK__x34_y34) and
+     location__BLANK___BLANK___BLANK_(location__BLANK__x33_y33) and
+      location__BLANK___BLANK___BLANK_(location__BLANK__x34_y34)))
 REL nextcell__east(v0, v1) =
  ex location__BLANK__x24_y24, location__BLANK__xnew1_y24
   (v0 = location__BLANK__x24_y24 and v1 = location__BLANK__xnew1_y24 and

Modified: trunk/Toss/GGP/tests/pacman3p-simpl.toss
===================================================================
--- trunk/Toss/GGP/tests/pacman3p-simpl.toss	2011-10-23 18:48:09 UTC (rev 1613)
+++ trunk/Toss/GGP/tests/pacman3p-simpl.toss	2011-10-23 20:28:50 UTC (rev 1614)
@@ -1,9 +1,6 @@
 REL distinctcell(v0, v1) =
- (not v0 = v1 and
-  ((location__BLANK___BLANK___BLANK_(v0) and
-    location__BLANK___BLANK___BLANK_(v1)) or
-   (location__BLANK___BLANK___BLANK_(v0) and
-    location__BLANK___BLANK___BLANK_(v1))))
+ (location__BLANK___BLANK___BLANK_(v0) and
+  location__BLANK___BLANK___BLANK_(v1) and not v0 = v1)
 REL nextcell__east(v0, v1) =
  (R(v0, v1) and location__BLANK___BLANK___BLANK_(v0) and
   location__BLANK___BLANK___BLANK_(v1))

Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex	2011-10-23 18:48:09 UTC (rev 1613)
+++ trunk/Toss/www/reference/reference.tex	2011-10-23 20:28:50 UTC (rev 1614)
@@ -2405,6 +2405,24 @@
 in the previous section. The move and player markers are erased by the
 game state transition rule of the ``environment'' player.
 
+\subsection{Translation-specific Simplification}
+
+In Section~\ref{sec-game-simpl}, we describe general game
+simplification in Toss. Here, we describe parts of the translation
+process that were added to make the translation result more compact
+and efficient.
+
+\paragraph{Introducing disequalities.} When a defined relation is
+built from clauses that contain a single \texttt{distinct} positive
+literal each, when the defined relation is translated as a binary
+relation, a disjunction of those \texttt{distinct} literals would be
+semantically equivalent to a disequality of the relation arguments,
+and the remaining literals are the same for all bodies (modulo
+renaming of variables), the disequality is introduced to the
+translation and the \texttt{distinct} literals are removed.
+
+\paragraph{}
+
 \section{Game Simplification in Toss} \label{sec-game-simpl}
 
 Games automatically translated from GDL, as described above, are verbose

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