Commit aeeb436f authored by bguillaum's avatar bguillaum
Browse files

split bound on rewriting depth into det/non-det bounds, add functions to change the bounds

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/semagramme/libcaml-grew/trunk@8970 7838e531-6607-4d57-9587-6c381814729c
parent 203d3238
...@@ -189,6 +189,11 @@ end (* module Array_ *) ...@@ -189,6 +189,11 @@ end (* module Array_ *)
(* ================================================================================ *) (* ================================================================================ *)
module List_ = struct module List_ = struct
let rec cut size = function
| [] -> []
| _ when size=0 -> []
| x::t -> x:: (cut (size-1) t)
let rec set position elt = function let rec set position elt = function
| [] -> failwith "List_.set" | [] -> failwith "List_.set"
| _::t when position = 0 -> elt::t | _::t when position = 0 -> elt::t
...@@ -256,6 +261,10 @@ module List_ = struct ...@@ -256,6 +261,10 @@ module List_ = struct
| [] -> "" | [] -> ""
| h::t -> List.fold_left (fun acc elt -> acc ^ sep ^ (string_of_item elt)) (string_of_item h) t | h::t -> List.fold_left (fun acc elt -> acc ^ sep ^ (string_of_item elt)) (string_of_item h) t
let rev_to_string string_of_item sep = function
| [] -> ""
| h::t -> List.fold_left (fun acc elt -> (string_of_item elt) ^ sep ^ acc) (string_of_item h) t
let rec sort_insert elt = function let rec sort_insert elt = function
| [] -> [elt] | [] -> [elt]
| h::t when elt<h -> elt::h::t | h::t when elt<h -> elt::h::t
......
...@@ -111,6 +111,10 @@ module List_: sig ...@@ -111,6 +111,10 @@ module List_: sig
val set: int -> 'a -> 'a list -> 'a list val set: int -> 'a -> 'a list -> 'a list
(** [cut size list] returns a list with the [size] first elements of [list].
If [list] contains less than [size] elements, the input list is returned *)
val cut: int -> 'a list -> 'a list
(** [index elt list] return [Some index] if [index] is the smallest position in the [list] equals to [elt]. (** [index elt list] return [Some index] if [index] is the smallest position in the [list] equals to [elt].
None is returned if [elt] is not in the [list] *) None is returned if [elt] is not in the [list] *)
val index: 'a -> 'a list -> int option val index: 'a -> 'a list -> int option
...@@ -131,6 +135,7 @@ module List_: sig ...@@ -131,6 +135,7 @@ module List_: sig
val sort_disjoint: 'a list -> 'a list -> bool val sort_disjoint: 'a list -> 'a list -> bool
val to_string: ('a -> string) -> string -> 'a list -> string val to_string: ('a -> string) -> string -> 'a list -> string
val rev_to_string: ('a -> string) -> string -> 'a list -> string
val sort_mem: 'a -> 'a list -> bool val sort_mem: 'a -> 'a list -> bool
......
...@@ -81,8 +81,13 @@ module Instance_set = Set.Make (Instance) ...@@ -81,8 +81,13 @@ module Instance_set = Set.Make (Instance)
(* ================================================================================ *) (* ================================================================================ *)
module Rule = struct module Rule = struct
(* the rewriting depth is bounded to stop rewriting when the system is not terminating *) (* the rewriting depth is bounded to stop rewriting when the system is not terminating *)
let max_depth = ref 500 let max_depth_det = ref 100
let max_depth_non_det = ref 2000
let set_max_depth_det value = max_depth_det := value
let set_max_depth_non_det value = max_depth_non_det := value
type const = type const =
| Cst_out of Pid.t * Label_cst.t | Cst_out of Pid.t * Label_cst.t
...@@ -860,15 +865,16 @@ module Rule = struct ...@@ -860,15 +865,16 @@ module Rule = struct
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** [apply_rule instance matching rule] returns a new instance after the application of the rule (** [apply_rule instance matching rule] returns a new instance after the application of the rule
[Command_execution_fail] is raised if some merge unification fails *) [Command_execution_fail] is raised if some merge unification fails *)
let apply_rule domain instance matching rule = let apply_rule domain modul_name max_depth instance matching rule =
(* Timeout check *) (* Timeout check *)
(try Timeout.check () with Timeout.Stop -> Error.run "Time out"); (try Timeout.check () with Timeout.Stop -> Error.run "Time out");
(* limit the rewriting depth to avoid looping rewriting *) (* limit the rewriting depth to avoid looping rewriting *)
begin begin
if List.length instance.Instance.rules >= !max_depth if List.length instance.Instance.rules >= max_depth
then Error.run "Bound reached (when applying rule %s)" rule.name then Error.run "[Module %s] max depth %d reached, last rules applied: …, %s, %s"
modul_name max_depth (List_.rev_to_string (fun x->x) ", " (List_.cut 4 instance.Instance.rules)) rule.name
end; end;
let (new_instance, created_nodes) = let (new_instance, created_nodes) =
...@@ -957,22 +963,22 @@ module Rule = struct ...@@ -957,22 +963,22 @@ module Rule = struct
List.map fst filtered_matching_list List.map fst filtered_matching_list
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** [one_step instance rules] computes the list of one-step reduct with rules *) (** [one_step domain modul_name instance rules] computes the list of one-step reduct with rules *)
let one_step domain instance rules = let one_step domain modul_name instance rules =
List.fold_left List.fold_left
(fun acc rule -> (fun acc rule ->
let matching_list = match_in_graph domain ?param:rule.param rule.pattern instance.Instance.graph in let matching_list = match_in_graph domain ?param:rule.param rule.pattern instance.Instance.graph in
List.fold_left List.fold_left
(fun acc1 matching -> (fun acc1 matching ->
try (apply_rule domain instance matching rule) :: acc1 try (apply_rule domain modul_name !max_depth_non_det instance matching rule) :: acc1
with Command_execution_fail -> acc1 with Command_execution_fail -> acc1
) acc matching_list ) acc matching_list
) [] rules ) [] rules
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** [conf_one_step instance rules] computes one Some (one-step reduct) with rules, None if no rule apply *) (** [conf_one_step domain modul_name instance rules] computes one Some (one-step reduct) with rules, None if no rule apply *)
let rec conf_one_step domain (instance : Instance.t) = function let rec conf_one_step domain modul_name (instance : Instance.t) = function
| [] -> None | [] -> None
| rule::rule_tail -> | rule::rule_tail ->
let (pos,negs) = rule.pattern in let (pos,negs) = rule.pattern in
...@@ -995,8 +1001,8 @@ module Rule = struct ...@@ -995,8 +1001,8 @@ module Rule = struct
fulfill domain (pos.graph,neg.graph) instance.Instance.graph new_partial_matching fulfill domain (pos.graph,neg.graph) instance.Instance.graph new_partial_matching
) negs ) negs
) matching_list in ) matching_list in
Some (apply_rule domain instance first_matching_where_all_witout_are_fulfilled rule) Some (apply_rule domain modul_name !max_depth_det instance first_matching_where_all_witout_are_fulfilled rule)
with Not_found -> (* try another rule *) conf_one_step domain instance rule_tail with Not_found -> (* try another rule *) conf_one_step domain modul_name instance rule_tail
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
...@@ -1021,7 +1027,7 @@ module Rule = struct ...@@ -1021,7 +1027,7 @@ module Rule = struct
let (new_to_do_set,new_nf_set) = let (new_to_do_set,new_nf_set) =
Instance_set.fold Instance_set.fold
(fun v (to_do_set_acc,nf_set_acc) -> (fun v (to_do_set_acc,nf_set_acc) ->
match one_step domain v rules with match one_step domain modul_name v rules with
| [] -> (to_do_set_acc,Instance_set.add (Instance.rev_steps v) nf_set_acc) | [] -> (to_do_set_acc,Instance_set.add (Instance.rev_steps v) nf_set_acc)
| step_of_v -> (List.fold_left (fun acc v1 -> Instance_set.add v1 acc) to_do_set_acc step_of_v, nf_set_acc) | step_of_v -> (List.fold_left (fun acc v1 -> Instance_set.add v1 acc) to_do_set_acc step_of_v, nf_set_acc)
) )
...@@ -1066,16 +1072,16 @@ module Rule = struct ...@@ -1066,16 +1072,16 @@ module Rule = struct
loop filters loop filters
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
let rec conf_normalize domain instance rules = let rec conf_normalize domain modul_name instance rules =
match conf_one_step domain instance rules with match conf_one_step domain modul_name instance rules with
| Some new_instance -> conf_normalize domain new_instance rules | Some new_instance -> conf_normalize domain modul_name new_instance rules
| None -> Instance.rev_steps instance | None -> Instance.rev_steps instance
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
let normalize domain modul_name ?(confluent=false) rules filters instance = let normalize domain modul_name ?(confluent=false) rules filters instance =
if confluent if confluent
then then
let output = conf_normalize domain instance rules in let output = conf_normalize domain modul_name instance rules in
if filter_instance domain filters output if filter_instance domain filters output
then (Instance_set.singleton output, Instance_set.empty) then (Instance_set.singleton output, Instance_set.empty)
else (Instance_set.empty, Instance_set.singleton output) else (Instance_set.empty, Instance_set.singleton output)
......
...@@ -59,6 +59,12 @@ module Instance_set : Set.S with type elt = Instance.t ...@@ -59,6 +59,12 @@ module Instance_set : Set.S with type elt = Instance.t
module Rule : sig module Rule : sig
type t type t
(** [set_max_depth_det value] set the maximum rewriting depth in deterministic application of a module. *)
val set_max_depth_det: int -> unit
(** [set_max_depth_non_det value] set the maximum rewriting depth in non-deterministic application of a module. *)
val set_max_depth_non_det: int -> unit
(** [get_name t] returns the name of the rule [t]. *) (** [get_name t] returns the name of the rule [t]. *)
val get_name: t -> string val get_name: t -> string
......
...@@ -228,6 +228,9 @@ module Rewrite = struct ...@@ -228,6 +228,9 @@ module Rewrite = struct
type display = Libgrew_types.rew_display type display = Libgrew_types.rew_display
type history = Grew_grs.Rewrite_history.t type history = Grew_grs.Rewrite_history.t
let set_max_depth_det value = Grew_rule.Rule.set_max_depth_det value
let set_max_depth_non_det value = Grew_rule.Rule.set_max_depth_non_det value
let display ~gr ~grs ~seq = let display ~gr ~grs ~seq =
handle ~name:"Rewrite.display" (fun () -> Grew_grs.Grs.build_rew_display grs seq gr) () handle ~name:"Rewrite.display" (fun () -> Grew_grs.Grs.build_rew_display grs seq gr) ()
......
...@@ -148,6 +148,9 @@ module Rewrite: sig ...@@ -148,6 +148,9 @@ module Rewrite: sig
type display = Libgrew_types.rew_display type display = Libgrew_types.rew_display
type history type history
val set_max_depth_det: int -> unit
val set_max_depth_non_det: int -> unit
(** [display gr grs seq] builds the [display] (datatype used by the GUI) given by (** [display gr grs seq] builds the [display] (datatype used by the GUI) given by
the rewriting of graph [gr] with the sequence [seq] of [grs]. the rewriting of graph [gr] with the sequence [seq] of [grs].
@param gr the grapth to rewrite @param gr the grapth to rewrite
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment