| Terms.Predicate _ -> assert false;
;;
+ let goal_pos t goal =
+ let rec aux path = function
+ | Terms.Var _ -> []
+ | Terms.Leaf x ->
+ if B.eq t x then path else []
+ | Terms.Node l ->
+ match
+ HExtlib.list_findopt
+ (fun x i ->
+ let p = aux (i::path) x in
+ if p = [] then None else Some p)
+ l
+ with
+ | None -> []
+ | Some p -> p
+ in
+ aux []
+ (match goal with
+ | _,Terms.Equation (l,r,ty,_),_,_ -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
+ | _,Terms.Predicate p,_,_ -> p)
+ ;;
+
let parse_symbols l goal =
let res = parse_symbols (parse_symbols SymbMap.empty [goal]) l in
SymbMap.fold (fun t (occ,ar) acc ->
- (t,occ,ar,goal_occ_nbr t goal)::acc) res []
+ (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
+ ;;
+
+ let rec leaf_count = function
+ | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
+ | Terms.Leaf _ -> 1
+ | _ -> 0
;;
let rec dependencies op clauses acc =
match clauses with
- | [] -> []
+ | [] -> acc
| (_,lit,_,_)::tl ->
match lit with
| Terms.Predicate _ -> assert false
else
dependencies op tl acc
else dependencies op tl acc
- | _ -> acc
+ | ((Terms.Node (Terms.Leaf op1::t) as x),y)
+ | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+ let rec term_leaves = function
+ | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
+ | Terms.Leaf x -> [x]
+ | _ -> []
+ in
+ if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then
+ dependencies op tl (op1::acc)
+ else
+ dependencies op tl acc
+ | _ -> dependencies op tl acc
;;
- let dependencies op clauses = dependencies op clauses [];;
+ let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
(* let max_weight_hyp = *)