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

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

Revision: 1534
          http://toss.svn.sourceforge.net/toss/?rev=1534&view=rev
Author:   lukstafi
Date:     2011-08-11 00:29:00 +0000 (Thu, 11 Aug 2011)

Log Message:
-----------
GDL translation fixing: two small bugs in preparing for formula translation (which somehow is very wrong but can be debugged now).

Modified Paths:
--------------
    trunk/Toss/GGP/GDLParser.mly
    trunk/Toss/GGP/TranslateFormula.ml
    trunk/Toss/GGP/TranslateFormula.mli
    trunk/Toss/GGP/TranslateFormulaTest.ml

Modified: trunk/Toss/GGP/GDLParser.mly
===================================================================
--- trunk/Toss/GGP/GDLParser.mly	2011-08-10 12:15:33 UTC (rev 1533)
+++ trunk/Toss/GGP/GDLParser.mly	2011-08-11 00:29:00 UTC (rev 1534)
@@ -14,9 +14,10 @@
 %token FORALL EXISTS EOF
 
 
-%start parse_game_description parse_request parse_term
+%start parse_game_description parse_request parse_term parse_literal_list
 %type <GDL.request> parse_request request
 %type <GDL.term> parse_term
+%type <GDL.literal list> parse_literal_list
 %type <GDL.clause list> parse_game_description game_description
 
 
@@ -146,3 +147,6 @@
 
 parse_term:
   | term EOF { $1 }
+
+parse_literal_list:
+  | body=list (literal) EOF { body }

Modified: trunk/Toss/GGP/TranslateFormula.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormula.ml	2011-08-10 12:15:33 UTC (rev 1533)
+++ trunk/Toss/GGP/TranslateFormula.ml	2011-08-11 00:29:00 UTC (rev 1534)
@@ -17,21 +17,26 @@
    splitting disjuncts if necessary, into "positive state terms",
    "negative state terms" and "reminder". *)
 let separate_disj disj =
+  (* FIXME see tests *)
   let aux conj =
     List.fold_right (fun lit acc -> match lit with
       | (Pos (True _) | Neg (True _)) as lit ->
         List.map (fun conj -> Aux.Left lit::conj) acc
       | Disj ls as lit ->
-        if List.for_all (function Pos _ -> true | _ -> false) ls
-          || List.for_all (function Neg _ -> true | _ -> false) ls
+        if List.for_all (function Pos (True _) -> true | _ -> false) ls
+          || List.for_all (function Neg (True _) -> true | _ -> false) ls
         then
           List.map (fun conj -> Aux.Left lit::conj) acc
-        else
+        else if List.exists
+            (function Pos (True _) | Neg (True _) -> true | _ -> false) ls
+        then
           Aux.concat_map (function
             | (Pos (True _) | Neg (True _)) as lit ->
               List.map (fun conj -> Aux.Left lit::conj) acc
             | lit -> List.map (fun conj -> Aux.Right lit::conj) acc
           ) ls
+        else                            (* none is [True _] *)
+          List.map (fun conj -> Aux.Right lit::conj) acc
       | lit -> List.map (fun conj -> Aux.Right lit::conj) acc
     ) conj [[]] in
   let disj = Aux.concat_map aux disj in
@@ -42,10 +47,10 @@
         | Pos _ as lit -> Aux.Left lit
         | Neg _ as lit -> Aux.Right lit
         | Disj ls as lit
-            when List.for_all (function Pos _ -> true | _ -> false) ls
+            when List.for_all (function Pos (True _) -> true | _ -> false) ls
               -> Aux.Left lit
         | Disj ls as lit
-            when List.for_all (function Neg _ -> true | _ -> false) ls
+            when List.for_all (function Neg (True _) -> true | _ -> false) ls
               -> Aux.Right lit
         | _ -> assert false
       ) state_terms in
@@ -130,15 +135,15 @@
       if sign then atoms
       else List.map (fun a -> Formula.Not a) atoms
     with Not_found -> [] in
-  let transl_defrel sign rel args =
+  let transl_posdefrel sign rel args =
     if List.mem rel data.defined_rels
     then
       [!translate_defrel data sterms_all sterms_in
           s_subterms sign rel args]
-    else transl_rel false rel args in
+    else transl_rel sign rel args in
   let rec aux = function
-    | Pos (Rel (rel, args)) -> transl_defrel true rel args
-    | Neg (Rel (rel, args)) -> transl_defrel false rel args
+    | Pos (Rel (rel, args)) -> transl_posdefrel true rel args
+    | Neg (Rel (rel, args)) -> transl_posdefrel false rel args
     | Pos (Does _ | Role _) | Neg (Does _ | Role _) ->
       []
     | Disj lits ->
@@ -147,6 +152,12 @@
   Formula.And (Aux.concat_map aux rels_phi)
 
 let transl_state data phi =
+  (* {{{ log entry *)
+  if !debug_level > 3 then (
+    Printf.printf "transl_state:\n%s\n%!"
+      (clause_str (("transl_state phi", [||]),phi))
+  );
+  (* }}} *)
   let transl_sterm sterm =
     let s_subterms =
       map_paths (fun path subt -> subt, path) data.all_paths sterm in
@@ -182,7 +193,7 @@
 let transl_disjunct data rels_phi pos_state_phi neg_state_phi ext_phi =
   let pos_terms = state_terms pos_state_phi in
   let pos_vars = List.map (var_of_term data) pos_terms in
-  let neg_terms = state_terms pos_state_phi in
+  let neg_terms = state_terms neg_state_phi in
   let neg_vars = List.map (var_of_term data) neg_terms in
   let all_terms = pos_terms @ neg_terms in
   let phi_vars = clause_vars
@@ -192,6 +203,15 @@
     List.map (fun v -> Pos (Rel ("EQ_", [|Var v; Var v|])))
       (Aux.Strings.elements phi_vars) in
   let rels_eqs = rels_phi @ eqs in
+  (* {{{ log entry *)
+if !debug_level > 2 then (
+    Printf.printf "\ntransl_disjunct:\n%s\n%s\n%s\n%s\n%!"
+      (clause_str (("rels_phi", [||]),rels_phi))
+      (clause_str (("pos_state_phi", [||]),pos_state_phi))
+      (clause_str (("neg_state_phi", [||]),neg_state_phi))
+      ("ext_phi="^Formula.str ext_phi)
+);
+(* }}} *)
   let negated_neg_state_transl =
     (* negation-normal-form of "not neg_state_phi" *)
     Formula.Or (
@@ -220,12 +240,9 @@
 (* **************************************** *)
 (* {3 Build and use defined relations.} *)
 
-let build_defrels data clauses =
-  let all_branches = Aux.concat_map
-    (fun ((rel,args),body) ->
-      List.map (fun phi -> rel, (args, phi)) (separate_disj [body]))
-    clauses in
-  let build_defrel rel =
+let select_defrel_argpaths data all_branches =
+  (* TODO: code-review this and [build_defrel] functions *)
+  let select_for_defrel rel =
     (* searching for ArgType = DefSide,S,p *)
     let branches = Aux.assoc_all rel all_branches in
     (* {{{ log entry *)
@@ -309,7 +326,25 @@
                    "TranslateFormula.build_defrels: could not \
   determine path for relation %s argument %d" rel i)
       ) p_defside in
+    let defrel_arg_type = Aux.array_map2
+      (fun defside path -> defside <> None, path)
+      p_defside arg_paths  in
+    data.defrel_arg_type :=
+      (rel, defrel_arg_type) :: !(data.defrel_arg_type);
+    rel, (p_defside, s_defside, arg_paths) in
+  List.map select_for_defrel data.defined_rels
+
+
+let build_defrels data clauses =
+  let all_branches = Aux.concat_map
+    (fun ((rel,args),body) ->
+      List.map (fun phi -> rel, (args, phi)) (separate_disj [body]))
+    clauses in
+  let sel_argpaths = select_defrel_argpaths data all_branches in
+  let build_defrel rel =
     (* now building the translation *)
+    let (p_defside, s_defside, arg_paths) =
+      List.assoc rel sel_argpaths in
     let defvars =
       Array.mapi (fun i _ -> "v"^string_of_int i) arg_paths in
     let defbody (args,(rels_phi,pos_state,neg_state)) s_defside =        
@@ -323,8 +358,7 @@
               | Some s -> var_of_term data s
               | None -> assert false in
             Formula.Eq (v, s_i)
-          else Formula.Eq (v,
-                           var_of_subterm data arg_paths.(i) args.(i)))
+          else Formula.Eq (v, var_of_subterm data arg_paths.(i) args.(i)))
         defvars in
       let arg_eqs = Formula.And (Array.to_list arg_eqs) in
       let callside_sterms =
@@ -338,17 +372,19 @@
         (Array.map (fun sterm -> Pos (True sterm)) callside_sterms) in
       transl_disjunct data rels_phi
         (callside_sterms @ pos_state) neg_state arg_eqs in
+    let branches = Aux.assoc_all rel all_branches in
     let def_disjuncts = List.map2 defbody branches s_defside in
-    let defrel_arg_type = Aux.array_map2
-      (fun defside path -> defside <> None, path)
-      p_defside arg_paths  in
-    data.defrel_arg_type :=
-      (rel, defrel_arg_type) :: !(data.defrel_arg_type);
     rel, (Array.to_list defvars, Formula.Or def_disjuncts) in
   List.map build_defrel data.defined_rels
 
 
 let transl_defrel data sterms_all sterms_in s_subterms sign rel args =
+  (* {{{ log entry *)
+  if !debug_level > 2 then (
+    Printf.printf "transl_defrel: phi=%s, sign=%b\n"
+      (rel_atom_str (rel, args)) sign
+  );
+  (* }}} *)
   let arg_type = List.assoc rel !(data.defrel_arg_type) in
   (* the $s \tpos_{p_{R,i}} = t_i$ state terms *)
   let arg_sterms = Array.mapi

Modified: trunk/Toss/GGP/TranslateFormula.mli
===================================================================
--- trunk/Toss/GGP/TranslateFormula.mli	2011-08-10 12:15:33 UTC (rev 1533)
+++ trunk/Toss/GGP/TranslateFormula.mli	2011-08-11 00:29:00 UTC (rev 1534)
@@ -21,6 +21,11 @@
 
 val empty_transl_data : transl_data
 
+(** Exposed for testing purposes only. *)
+val separate_disj :
+  GDL.literal list list ->
+  (GDL.literal list * GDL.literal list * GDL.literal list) list
+
 val translate :
   transl_data -> GDL.literal list list -> Formula.formula
 

Modified: trunk/Toss/GGP/TranslateFormulaTest.ml
===================================================================
--- trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-10 12:15:33 UTC (rev 1533)
+++ trunk/Toss/GGP/TranslateFormulaTest.ml	2011-08-11 00:29:00 UTC (rev 1534)
@@ -9,6 +9,10 @@
   GDLParser.parse_term KIFLexer.lex
     (Lexing.from_string s)
 
+let parse_literal_list s =
+  GDLParser.parse_literal_list KIFLexer.lex
+    (Lexing.from_string s)
+
 let pte = parse_term
 
 let state_of_file s =
@@ -69,6 +73,72 @@
 
 let tests = "TranslateFormula" >::: [
   
+  "separate_disj" >::
+    (fun () ->
+      let i2s = string_of_int in
+      let str_res disj = Array.mapi
+        (fun i (rels, pos_s, neg_s) ->
+          GDL.clause_str (("rels#"^i2s i, [||]),rels) ^"\n" ^
+            GDL.clause_str (("pos_s#"^i2s i, [||]),pos_s) ^"\n" ^
+          GDL.clause_str (("neg_s#"^i2s i, [||]),neg_s) ^"\n")
+        (Array.of_list disj) in
+
+      let phi = "(or (col ?r) (row ?r) (diag1 ?r) (diag2 ?r))" in
+      let conj = parse_literal_list phi in
+      let disj = separate_disj [conj] in
+      assert_equal ~msg:phi ~printer:(fun x->x)
+        "(<= (rels#0 )
+    (or (col ?r) (row ?r) (diag1 ?r) (diag2 ?r)))
+(<= (pos_s#0 )
+    )
+(<= (neg_s#0 )
+    )
+"
+        (String.concat "\n" (Array.to_list (str_res disj)));
+
+      let phi = "(or (arel x) (true s1)) (brel y)" in
+      let conj = parse_literal_list phi in
+      let disj = separate_disj [conj] in
+      assert_equal ~msg:phi ~printer:(fun x->x)
+        "(<= (rels#0 )
+    (arel x)
+    (brel y))
+(<= (pos_s#0 )
+    )
+(<= (neg_s#0 )
+    )
+
+(<= (rels#1 )
+    (brel y))
+(<= (pos_s#1 )
+    (true s1))
+(<= (neg_s#1 )
+    )
+"
+        (String.concat "\n" (Array.to_list (str_res disj)));
+
+      let phi = "(or (arel x) (true s1)) (not (true s2))" in
+      let conj = parse_literal_list phi in
+      let disj = separate_disj [conj] in
+      assert_equal ~msg:phi ~printer:(fun x->x)
+        "(<= (rels#0 )
+    (arel x))
+(<= (pos_s#0 )
+    )
+(<= (neg_s#0 )
+    (not (true s2)))
+
+(<= (rels#1 )
+    )
+(<= (pos_s#1 )
+    (true s1))
+(<= (neg_s#1 )
+    (not (true s2)))
+"
+        (String.concat "\n" (Array.to_list (str_res disj)));
+
+    ); 
+  
   "defined relations connect5" >::
     (fun () ->
       let descr = load_rules ("./GGP/examples/connect5.gdl") in
@@ -100,7 +170,7 @@
 
 let a () =
   TranslateFormula.debug_level := 5;
-  GDL.debug_level := 2;
+  (* GDL.debug_level := 2; *)
   ()
 
 let a () =


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