[Toss-devel-svn] SF.net SVN: toss:[1461] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
From: <luk...@us...> - 2011-05-26 23:14:28
|
Revision: 1461 http://toss.svn.sourceforge.net/toss/?rev=1461&view=rev Author: lukaszkaiser Date: 2011-05-26 23:14:21 +0000 (Thu, 26 May 2011) Log Message: ----------- Support for recursively defined relations. Modified Paths: -------------- trunk/Toss/Formula/FormulaOps.ml trunk/Toss/Formula/FormulaOps.mli trunk/Toss/Formula/FormulaOpsTest.ml trunk/Toss/Server/Picture.ml Modified: trunk/Toss/Formula/FormulaOps.ml =================================================================== --- trunk/Toss/Formula/FormulaOps.ml 2011-05-26 22:02:48 UTC (rev 1460) +++ trunk/Toss/Formula/FormulaOps.ml 2011-05-26 23:14:21 UTC (rev 1461) @@ -382,7 +382,13 @@ let map_to_atoms_expr f r = map_to_literals_expr (function Not (x) -> Not (f x) | x -> f x) (fun x -> x) r +let get_atoms phi = + let atoms = ref [] in + let add_atom x = atoms := x :: !atoms; x in + ignore (map_to_atoms add_atom phi); + Aux.unique_sorted !atoms + let rec fold_over_literals f phi acc = match phi with | Rel _ | Eq _ | In _ | SO _ as x -> f x acc @@ -581,7 +587,7 @@ let subst_r defs = function (* Helper function for atoms. *) | Rel (rn, vs) -> ( try - let (dvs, dphi) = List.assoc rn defs in + let (_, dvs, dphi) = List.assoc rn defs in let ovs = List.map var_str (Array.to_list vs) in subst_vars (List.combine dvs ovs) dphi with Not_found -> Rel (rn, vs) ) @@ -590,11 +596,13 @@ (* Substitute once in [phi] relations in [defs] by corresponding subformulas (with instantiated parameters). *) let subst_once_rels defs phi = - map_to_atoms (subst_r defs) phi + let cdefs = List.map (fun (n, (v, f)) -> (n, ([], v, f))) defs in + map_to_atoms (subst_r cdefs) phi (* Substitute once in [r] relations defined in [defs] by their definitions. *) let subst_once_rels_expr defs r = - map_to_atoms_expr (subst_r defs) r + let cdefs = List.map (fun (n, (v, f)) -> (n, ([], v, f))) defs in + map_to_atoms_expr (subst_r cdefs) r (* Helper function: fixed-point up to [n] *) let rec fp_n print n f x = @@ -606,15 +614,63 @@ else fp_n print (n-1) f nx -(* Substitute recursively in [phi] relations defined in [defs]. *) -let subst_rels defs phi = - fp_n str (List.length defs) (subst_once_rels defs) phi - (* Substitute recursively in [r] relations defined in [defs]. *) let subst_rels_expr defs r = fp_n real_str (List.length defs) (subst_once_rels_expr defs) r +(* Substitute recursively in [phi] relations defined in [defs]. *) +let subst_rels defs phi = + let rels f = + Aux.map_some (function Rel (r, _) -> Some r | _ -> None) (get_atoms f) in + let rels_def defs f = List.filter (fun r -> List.mem_assoc r defs) (rels f) in + let cdefs = List.map (fun (n, (vs,f)) -> (n, (rels_def defs f, vs,f))) defs in + let cdfstr (n, (rs, _, _)) = + Printf.sprintf "rel %s calls %s" n + (if (List.length rs) = 0 then "nothing" else + let rstr = String.concat ", " rs in + if List.mem n rs then "self, " ^ rstr else rstr) in + if !debug_level > 1 then + Printf.printf "Subst:\n %s\n" (String.concat "\n " (List.map cdfstr cdefs)); + let is_basic (_, (rs, _, _)) = List.length rs = 0 in + let self_calls (n, (rs, _, _)) = List.mem n rs in + let subst_once_fm defs phi = map_to_atoms (subst_r defs) phi in + let subst_once rdefs defs (n, (rs, v, f)) = + let nf = subst_once_fm defs f in + (n, (rels_def rdefs nf, v, nf)) in + let subst_once_defs defs lst = List.map (subst_once lst defs) lst in + let rec rec_subst_rels cdefs phi = + if cdefs = [] then phi else + let (basic, other) = List.partition is_basic cdefs in + if basic <> [] then + rec_subst_rels (subst_once_defs basic other) (subst_once_fm basic phi) + else + let cdefss = List.sort Pervasives.compare cdefs in (* repeatability *) + let (selfc, otherc) = List.partition self_calls cdefss in + if otherc <> [] then + let (d, ds) = (List.hd otherc, (List.tl otherc) @ selfc) in + rec_subst_rels (subst_once_defs [d] ds) (subst_once_fm [d] phi) + else + let sovar n = so_var_of_string ("|" ^ n) in + let sorels rels = function + | Rel (m, rvs) when List.mem m rels -> SO (sovar m, rvs) + | x -> x in + let do_lfp (n, (calls, vs, f)) = + let va = Array.of_list (List.map fo_var_of_string vs) in + let nf = map_to_atoms (sorels [n]) f in + (n, ([], vs, Lfp ((sovar n :> [mso_var | so_var]), va, nf))) in + let (d, ds) = do_lfp (List.hd selfc), List.tl selfc in + rec_subst_rels (subst_once_defs [d] ds) (subst_once_fm [d] phi) in + let res_phi = rec_subst_rels cdefs phi in + let simpfpvars = List.map (fun (n, _) -> "|" ^ n) cdefs in (*TODO:reoccurs?*) + let rec simp_def_lfp acc fpvar fpvs fpdef = + if List.mem fpvar acc && List.mem (var_str fpvar) simpfpvars then + SO (to_so (fpvar :> var), fpvs) + else + let smap = { identity_map with map_Lfp = simp_def_lfp (fpvar :: acc) } in + Lfp (fpvar, fpvs, map_formula smap fpdef) in + map_formula { identity_map with map_Lfp = simp_def_lfp []} res_phi + (* --- AType with variables over given relations, no repetition, equality --- *) let atp rels vars_in = Modified: trunk/Toss/Formula/FormulaOps.mli =================================================================== --- trunk/Toss/Formula/FormulaOps.mli 2011-05-26 22:02:48 UTC (rev 1460) +++ trunk/Toss/Formula/FormulaOps.mli 2011-05-26 23:14:21 UTC (rev 1461) @@ -105,6 +105,7 @@ real_expr -> real_expr val map_to_atoms : (formula -> formula) -> formula -> formula val map_to_atoms_expr : (formula -> formula) -> real_expr -> real_expr +val get_atoms : formula -> formula list val fold_over_literals : (formula -> 'a -> 'a) -> formula -> 'a -> 'a Modified: trunk/Toss/Formula/FormulaOpsTest.ml =================================================================== --- trunk/Toss/Formula/FormulaOpsTest.ml 2011-05-26 22:02:48 UTC (rev 1460) +++ trunk/Toss/Formula/FormulaOpsTest.ml 2011-05-26 23:14:21 UTC (rev 1461) @@ -317,6 +317,21 @@ defs_eq [("R", (["x"; "y"], formula_of_string "S (x, y) and ex x S(y, x)"))] "R (y, x)" "S(y, x) and ex x0 (S(x, x0))"; + defs_eq + [("R", (["x"; "y"], formula_of_string "P(x) or R(x, y)"))] + "R (x, y)" "lfp |R (x, y) = (P(x) or |R(x, y))"; + defs_eq + [("R", (["x"; "y"], formula_of_string "P(x) or S(x, y)")); + ("S", (["x"; "y"], formula_of_string "Q(x) or R(x, y)"))] + "R (x, y)" "P (x) or lfp |S (x, y) = (Q(x) or P(x) or |S(x, y))"; + defs_eq + [("R", (["x"; "y"], formula_of_string "R(x, y) or P(x) or S(x, y)")); + ("S", (["x"; "y"], formula_of_string "S(x, y) or Q(x) or R(x, y)"))] + "R(x, y) and S(x, y)" + ("lfp |R(x,y) = ((|R(x, y) or P(x) or lfp |S(x, y) =" ^ + " (|S(x, y) or Q(x) or |R(x, y)))) and " ^ + "lfp |S(x, y) = ((|S(x, y) or Q(x) or lfp |R(x, y) =" ^ + " (|R(x, y) or P(x) or |S(x, y))))"); ); "atp, mintp" >:: Modified: trunk/Toss/Server/Picture.ml =================================================================== --- trunk/Toss/Server/Picture.ml 2011-05-26 22:02:48 UTC (rev 1460) +++ trunk/Toss/Server/Picture.ml 2011-05-26 23:14:21 UTC (rev 1461) @@ -349,16 +349,14 @@ Solver.M.check right_el psi && not (Solver.M.check wrong_el phi) in let w = FormulaOps.mintp ok csg vars in let minimize phi = - let atoms = ref [] in - let add_atom x = atoms := x :: !atoms; x in - ignore (FormulaOps.map_to_atoms add_atom phi); + let atoms = FormulaOps.get_atoms phi in let subst_atom a b x = if x = a then b else x in let phi0 f a = FormulaOps.map_to_atoms (subst_atom a (Formula.Or[])) f in let phi1 f a = FormulaOps.map_to_atoms (subst_atom a (Formula.And[])) f in let mini f a = let (f0, f1) = (phi0 f a, phi1 f a) in Formula.flatten (if ok f0 then f0 else if ok f1 then f1 else f) in - List.fold_left mini phi (Aux.unique_sorted !atoms) in + List.fold_left mini phi atoms in let mw = List.map minimize w in if !debug_level > 0 then Format.printf "@[%a@]@ \n%!" Formula.fprint (Formula.And mw); This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site. |