with Backtrack s ->
prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int i);
aux (i+1)
in
aux 1
aux showstoppers xs
with
Dangerous ->
- aux (sort_uniq (h::showstoppers)) ps in
-
- let showstoppers = sort_uniq (aux showstoppers ps) in
- let dangerous_conv =
- List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
+ aux (sort_uniq (h::showstoppers)) ps
+ in
+ let showstoppers = sort_uniq (aux showstoppers ps) in
+ let dangerous_conv =
+ List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
- let showstoppers' = showstoppers @ List.concat dangerous_conv in
- let showstoppers' = sort_uniq (match div with
- | None -> showstoppers'
- | Some div ->
- if List.exists ((=) (hd_of_i_var div)) showstoppers'
- then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+ let showstoppers' = showstoppers @ List.concat dangerous_conv in
+ let showstoppers' = sort_uniq (match div with
+ | None -> showstoppers'
+ | Some div ->
+ if List.exists ((=) (hd_of_i_var div)) showstoppers'
+ then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+ if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
;;
let precompute_edible_data {ps; div} xs =
let showstoppers_eat = List.filter
(fun x -> not (List.mem x showstoppers_step))
showstoppers_eat in
-List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+ List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
+ List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
p, showstoppers_step, showstoppers_eat
;;
| x::_ ->
prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var p.var_names x);
x) in
-(* Strategy that decreases the special_k to 0 first (round robin)
-1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
- let x =
- try
- match
- hd_of (List.find (fun t ->
- compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
- ) (all_terms p))
- with
- | None -> assert false
- | Some x ->
- prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var p.var_names x);
- x
- with
- Not_found ->
- let arity_of_x = max_arity_tms x (all_terms p) in
- assert (Util.option_get arity_of_x > 0);
- x in
-(* Instantiate in decreasing order of compute_special_k
-1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
-let x =
- try
- (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) (all_terms p))))) with
- None -> assert false
- | Some x ->
- prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
- x)
- with
- Not_found -> x
-in*)
let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in
let safe_arity_of_x = safe_arity_of_var p x in
x, min arity_of_x safe_arity_of_x
Backtrack _ -> `Unseparable "backtrack"
;;
+let no_bombs_pacmans p =
+ not (List.exists (eta_subterm `Bottom) (p.ps@p.conv))
+ && not (List.exists (eta_subterm `Pacman) p.ps)
+ && Util.option_map (eta_subterm `Pacman) p.div <> Some true
+;;
+
let check p =
- (* TODO check if there are duplicates in p.ps
- before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *)
- (* FIXME what about initial fragments? *)
if (let rec f = function
| [] -> false
| hd::tl -> List.exists (eta_eq hd) tl || f tl in
- f p.ps)
+ f p.ps) (* FIXME what about initial fragments of numbers? *)
then `CompleteUnseparable "ps contains duplicates"
(* check if div occurs somewhere in ps@conv *)
else if (match p.div with
| None -> true
| Some div -> not (List.exists (eta_subterm div) (p.ps@p.conv))
- ) && false (* TODO no bombs && pacmans *)
+ ) && no_bombs_pacmans p
then `CompleteSeparable "no bombs, pacmans and div"
- else if false (* TODO bombs or div fuori da lambda in ps@conv *)
- then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv"
+ (* il check seguente e' spostato nel parser e lancia un ParsingError *)
+ (* else if false (* TODO bombs or div fuori da lambda in ps@conv *)
+ then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv" *)
else if p.div = None
then `CompleteSeparable "no div"
else `Uncomplete