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

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

Revision: 1338
          http://toss.svn.sourceforge.net/toss/?rev=1338&view=rev
Author:   lukaszkaiser
Date:     2011-03-01 02:15:08 +0000 (Tue, 01 Mar 2011)

Log Message:
-----------
Correcting FormulaOps.tnf_fv bug found during GDL translation, real_expr cache in Solver.

Modified Paths:
--------------
    trunk/Toss/Formula/FormulaOps.ml
    trunk/Toss/Formula/FormulaOps.mli
    trunk/Toss/Formula/FormulaOpsTest.ml
    trunk/Toss/Server/ServerTest.ml
    trunk/Toss/Solver/Solver.ml

Modified: trunk/Toss/Formula/FormulaOps.ml
===================================================================
--- trunk/Toss/Formula/FormulaOps.ml	2011-02-28 22:04:19 UTC (rev 1337)
+++ trunk/Toss/Formula/FormulaOps.ml	2011-03-01 02:15:08 UTC (rev 1338)
@@ -147,6 +147,9 @@
 let map_to_atoms_full f g phi =
   map_to_literals (function Not (x) -> Not (f x) | x -> f x) g phi
 
+let map_to_atoms_full_re f g re =
+  map_to_literals_expr (function Not (x) -> Not (f x) | x -> f x) g re
+
 let map_to_atoms f phi =
   map_to_literals (function Not (x) -> Not (f x) | x -> f x) (fun x -> x) phi
 
@@ -919,27 +922,30 @@
   | [] -> [] 
   | [f] -> [order_by_fv_phi acc_fv f]
   | l ->
-    let cross x = List.exists (fun v -> List.mem v acc_fv) (free_vars x) in
+    let cross x = 
+      let fv = free_vars x in
+      fv = [] || List.exists (fun v -> List.mem v acc_fv) fv in
     let (cf, o) = List.partition cross l in
-    if cf = [] then 
+    if cf = [] then (
       let new_fv = free_vars (List.hd l) in
       order_by_fv new_fv l
-    else
+    ) else (
       let new_fv = acc_fv @ (free_vars_fo (And cf)) in
       (List.map (order_by_fv_phi acc_fv) cf) @ (order_by_fv new_fv o)
+    )
 
 and order_by_fv_phi acc_fv = function
   | And fl ->
     let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
     let (p, np) = List.partition is_pred fl in 
     let res = And (order_by_fv acc_fv (p @ np)) in
-    if !debug_level > 0 then print_endline ("fvordered and: " ^ (str res));
+    if !debug_level > 1 then print_endline ("fvordered and: " ^ (str res));
     res
   | Or fl ->
     let is_pred = function Rel (_, [|_|]) -> true | _ -> false in
     let (p, np) = List.partition is_pred fl in 
     let res = Or (order_by_fv acc_fv (p @ np)) in
-    if !debug_level > 0 then print_endline ("fvordered or: " ^ (str res));
+    if !debug_level > 1 then print_endline ("fvordered or: " ^ (str res));
     res
   | Ex (vs, phi) -> Ex (vs, order_by_fv_phi acc_fv phi)
   | All (vs, phi) -> All (vs, order_by_fv_phi acc_fv phi)

Modified: trunk/Toss/Formula/FormulaOps.mli
===================================================================
--- trunk/Toss/Formula/FormulaOps.mli	2011-02-28 22:04:19 UTC (rev 1337)
+++ trunk/Toss/Formula/FormulaOps.mli	2011-03-01 02:15:08 UTC (rev 1338)
@@ -29,6 +29,8 @@
 (** Map [f] to all atoms in the given formula. *)
 val map_to_atoms_full : (formula -> formula) -> (real_expr -> real_expr) -> 
   formula -> formula
+val map_to_atoms_full_re : (formula -> formula) -> (real_expr -> real_expr) -> 
+  real_expr -> real_expr
 val map_to_atoms : (formula -> formula) -> formula -> formula
 val map_to_atoms_expr : (formula -> formula) -> real_expr -> real_expr
 

Modified: trunk/Toss/Formula/FormulaOpsTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaOpsTest.ml	2011-02-28 22:04:19 UTC (rev 1337)
+++ trunk/Toss/Formula/FormulaOpsTest.ml	2011-03-01 02:15:08 UTC (rev 1338)
@@ -114,6 +114,20 @@
       ((not P(x) and not Q(x)) <-> RT(p, r)) )";
     );
 
+   "tnf fv" >::
+    (fun () ->
+      let tnffv_eq phi1 phi2 = formula_eq id phi2 FormulaOps.tnf_fv phi1 in
+      tnffv_eq "P(x) and (P(x) or Q(x))" "P(x)";
+      tnffv_eq ("ex x_3_3, x_2_2, x_1_1 (" ^
+	"(R_1_Y_MV1(x_1_1) and R_2_Y_MV1(x_2_2) and R_3_Y_MV1(x_3_3) " ^
+	"and R_X_1_MV1(x_1_1) and R_X_2_MV1(x_2_2) and R_X_3_MV1(x_3_3) " ^ 
+	"and R_X_Y_XP(x_1_1) and R_X_Y_XP(x_2_2) and R_X_Y_XP(x_3_3)))")
+	("ex x_1_1 ((R_1_Y_MV1(x_1_1) and R_X_1_MV1(x_1_1) and " ^ 
+	    "R_X_Y_XP(x_1_1))) and ex x_2_2 ((R_2_Y_MV1(x_2_2) and " ^ 
+	    "R_X_2_MV1(x_2_2) and R_X_Y_XP(x_2_2))) and ex x_3_3 (" ^ 
+	    "(R_3_Y_MV1(x_3_3) and R_X_3_MV1(x_3_3) and R_X_Y_XP(x_3_3)))")
+    );
+
    "subst free and all" >::
      (fun () ->
        let subst phi = FormulaOps.subst_vars [("x", "a"); ("y", "b")] phi in

Modified: trunk/Toss/Server/ServerTest.ml
===================================================================
--- trunk/Toss/Server/ServerTest.ml	2011-02-28 22:04:19 UTC (rev 1337)
+++ trunk/Toss/Server/ServerTest.ml	2011-03-01 02:15:08 UTC (rev 1338)
@@ -47,7 +47,8 @@
 
   "ServerGDLTest.in GDL Tic-Tac-Toe automatic" >::
     (fun () ->
-      todo "real soon now...";
+      (* todo "real soon now..."; *)
+      (* Solver.set_debug_level 2; *)
       let old_det_suggest = !Game.deterministic_suggest in
       Game.deterministic_suggest := true;
       let old_translation = !GDL.manual_translation in

Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml	2011-02-28 22:04:19 UTC (rev 1337)
+++ trunk/Toss/Solver/Solver.ml	2011-03-01 02:15:08 UTC (rev 1338)
@@ -15,6 +15,7 @@
 
 let cache_struc = ref (empty_structure ())
 let cache_results = ref (Hashtbl.create 15)
+let re_cache_results = ref (Hashtbl.create 15)
 
 let get_cache () = (!cache_struc, Hashtbl.copy !cache_results)
 let set_cache (struc, res) = cache_struc := struc; cache_results := res
@@ -47,8 +48,8 @@
     if !debug_level > 0 then print_endline ("Found " ^ (str phi));
     (Hashtbl.find solver.formulas_eval res, res)
   with Not_found ->
+    if !debug_level > 0 then print_endline ("Entered " ^ (str phi));
     let psi = FormulaOps.tnf_fv phi in
-    if !debug_level > 0 then print_endline ("Entered " ^ (str phi));
     if !debug_level > 0 then print_endline ("Registering " ^ (str psi));
     let id = Hashtbl.length solver.formulas_eval + 1 in
     Hashtbl.add solver.reg_formulas phi id;
@@ -263,26 +264,50 @@
     Some rs
   with Not_found -> None
 
+let re_rels re =
+  let rels = ref [] in
+  let app_rel = function Rel (s, _) as r -> rels := s :: !rels; r | x -> x in
+  let app_re = function Fun _ -> raise Not_found | x -> x in
+  try 
+    let _ = FormulaOps.map_to_atoms_full_re app_rel app_re re in
+    let rs = Aux.unique_sorted !rels in
+    if !debug_level > 1 then
+      print_endline ("FR: " ^ (Formula.real_str re) ^ " " ^ 
+			(String.concat ", " rs));
+    Some rs
+  with Not_found -> None
+
+
+let update_cache struc =
+  if not (Structure.equal !cache_struc struc) then
+    match diffrels_struc struc !cache_struc with
+      | None -> 
+	cache_struc := struc;
+	Hashtbl.clear !cache_results;
+	Hashtbl.clear !re_cache_results;
+      | Some rs ->
+	cache_struc := struc;
+	let is_bad (_, prs_opt) = 
+	  match prs_opt with
+	    | None -> true
+	    | Some prs -> List.exists (fun r -> List.mem r rs) prs in
+	let ok = ref [] in
+	Hashtbl.iter (fun p r -> if is_bad r then () else ok := (p, r)::!ok)
+	  !cache_results;
+	Hashtbl.clear !cache_results;
+	List.iter (fun (p, r) -> Hashtbl.add !cache_results p r) !ok;
+	let ok_re = ref [] in
+	Hashtbl.iter 
+	  (fun p r -> if is_bad r then () else ok_re := (p, r)::!ok_re)
+	  !re_cache_results;
+	Hashtbl.clear !re_cache_results;
+	List.iter (fun (p, r) -> Hashtbl.add !re_cache_results p r) !ok_re
+
+
 (* Eval with very basic caching. *)
 let eval_m struc phi = 
   if phi = And [] then Any else (
-    if not (Structure.equal !cache_struc struc) then (
-      match diffrels_struc struc !cache_struc with
-	| None -> 
-	  cache_struc := struc;
-	  Hashtbl.clear !cache_results;
-	| Some rs ->
-	  cache_struc := struc;
-	  let is_bad (_, prs_opt) = 
-	    match prs_opt with
-	      | None -> true
-	      | Some prs -> List.exists (fun r -> List.mem r rs) prs in
-	  let ok = ref [] in
-	  Hashtbl.iter (fun p r -> if is_bad r then () else ok := (p, r)::!ok)
-	    !cache_results;
-	  Hashtbl.clear !cache_results;
-	  List.iter (fun (p, r) -> Hashtbl.add !cache_results p r) !ok
-    );
+    update_cache struc;
     try
       let (res, _) = Hashtbl.find !cache_results phi in
       if !debug_level > 1 then (
@@ -396,7 +421,27 @@
                   AssignmentSet.str ev_assgn) in
       get_rval (join asg (evaluate_real "#" expr struc))
 
+let rec get_real_val_cache solver struc = function
+  | Const c -> c 
+  | Plus (e1, e2) ->
+    (get_real_val_cache solver struc e1) +. (get_real_val_cache solver struc e2)
+  | Times (e1, e2) -> 
+    (get_real_val_cache solver struc e1) *. (get_real_val_cache solver struc e2)
+  | re ->
+    update_cache struc;
+    try
+      let (res, _) = Hashtbl.find !re_cache_results re in
+      if !debug_level > 1 then (
+	print_endline ("found in re cache: " ^ (Formula.real_str re));
+      );
+      res
+    with Not_found ->
+      if !debug_level > 0 then print_endline ("Get real val " ^ (real_str re));
+      let re_val = get_real_val solver Any re struc in
+      Hashtbl.add !re_cache_results re (re_val, re_rels re);
+      re_val
 
+
 (* Evaluate i-th formula on j-th structure. *)
 let evaluate solver ~formula struc =
   let phi = Hashtbl.find solver.formulas_eval formula in
@@ -441,7 +486,7 @@
 
   let check_formula struc formula =
     check solver ~formula struc
-  let get_real_val = get_real_val solver Any
+  let get_real_val re struc = get_real_val_cache solver struc re
   let formula_str phi =
     let phi = Hashtbl.find solver.formulas_check phi in
     Formula.str phi


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