open Printf
-let debug = ref false
+let debug = ref true
let debug_print ?(depth=0) s =
if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
let debug_do f = if !debug then f () else ()
status pos cache
and attack pos cache and_item =
- show pos; (* uncomment to show the tree *)
+ (* show pos; uncomment to show the tree *)
match and_item with
| _, S _ -> assert false (* next would close the proof or give a D *)
| _, L _ -> assert false (* L is a final solution *)
up_to depth depth
;;
+let rec rm_assoc n = function
+ | [] -> assert false
+ | (x,i)::tl when n=x -> i,tl
+ | p::tl -> let i,tl = rm_assoc n tl in i,p::tl
+;;
+
+let merge canonicals elements n m =
+ let cn,canonicals = rm_assoc n canonicals in
+ let cm,canonicals = rm_assoc m canonicals in
+ let ln,elements = rm_assoc cn elements in
+ let lm,elements = rm_assoc cm elements in
+ let canonicals =
+ (n,cm)::(m,cm)::List.map
+ (fun (x,xc) as p ->
+ if xc = cn then (x,cm) else p) canonicals
+ in
+ let elements = (cn,ln@lm)::elements
+ in
+ canonicals,elements
+;;
+
+let clusters f l =
+ let canonicals = List.map (fun x -> (x,x)) l in
+ let elements = List.map (fun x -> (x,[x])) l in
+ List.fold_left
+ (fun (canonicals,elements) x ->
+ let dep = f x in
+ List.fold_left
+ (fun (canonicals,elements) d ->
+ merge canonicals elements d x)
+ (canonicals,elements) dep)
+ (canonicals,elements) l
+;;
+
let group_by_tac ~eq_predicate ~action:tactic status =
let goals = head_goals status#stack in
if List.length goals < 2 then tactic status
(* ========================= dispatching of auto/auto_paramod ============ *)
let auto_tac ~params:(_,flags as params) =
if List.mem_assoc "paramodulation" flags then
- auto_paramod_tac ~params
+ auto_paramod_tac ~params
+ else if List.mem_assoc "fast_paramod" flags then
+ NnAuto.fast_eq_check_tac ~params
+ else if List.mem_assoc "slir" flags then
+ NnAuto.auto_tac ~params
else
auto_tac ~params
;;