X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=dbc85261b87385771cc457f5407ed14a1ccf6984;hb=975da98810a335a759a3b5e5f96b1beb96c932d2;hp=a0148fb358398b9cd89cc8fff49827bf84ae399c;hpb=87955f4aa47c0f5f416f24bae4848eccb1cc23d5;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index a0148fb35..dbc85261b 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -15,6 +15,32 @@ let string_of_sign = function ;; +(* +let symbols_of_equality (_, (_, left, right), _, _) = + TermSet.union (symbols_of_term left) (symbols_of_term right) +;; +*) + +let symbols_of_equality ((_, (_, left, right), _, _) as equality) = + let m1 = symbols_of_term left in + let m = + TermMap.fold + (fun k v res -> + try + let c = TermMap.find k res in + TermMap.add k (c+v) res + with Not_found -> + TermMap.add k v res) + (symbols_of_term right) m1 + in +(* Printf.printf "symbols_of_equality %s:\n" *) +(* (string_of_equality equality); *) +(* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *) +(* print_newline (); *) + m +;; + + module OrderedEquality = struct type t = Inference.equality @@ -39,10 +65,15 @@ module EqualitySet = Set.Make(OrderedEquality);; let weight_age_ratio = ref 0;; (* settable by the user from the command line *) let weight_age_counter = ref !weight_age_ratio;; -let set_selection = ref (fun set -> EqualitySet.min_elt set);; +let symbols_ratio = ref 0;; +let symbols_counter = ref 0;; + -let select env passive = +let select env passive active = let (neg_list, neg_set), (pos_list, pos_set) = passive in + let remove eq l = + List.filter (fun e -> not (e = eq)) l + in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with @@ -55,19 +86,76 @@ let select env passive = (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set)) | _, _ -> assert false ) - | _ -> - let remove eq l = - List.filter (fun e -> not (e = eq)) l + | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> ( + symbols_counter := !symbols_counter - 1; + let cardinality map = + TermMap.fold (fun k v res -> res + v) map 0 in + match active with + | (Negative, e)::_ -> + let symbols = symbols_of_equality e in + let card = cardinality symbols in + let f equality (i, e) = + let common, others = + TermMap.fold + (fun k v (r1, r2) -> + if TermMap.mem k symbols then + let c = TermMap.find k symbols in + let c1 = abs (c - v) in + let c2 = v - c1 in + r1 + c2, r2 + c1 + else + r1, r2 + v) + (symbols_of_equality equality) (0, 0) + in +(* Printf.printf "equality: %s, common: %d, others: %d\n" *) +(* (string_of_equality ~env equality) common others; *) + let c = others + (abs (common - card)) in + if c < i then (c, equality) + else (i, e) + in + let e1 = EqualitySet.min_elt pos_set in + let initial = + let common, others = + TermMap.fold + (fun k v (r1, r2) -> + if TermMap.mem k symbols then + let c = TermMap.find k symbols in + let c1 = abs (c - v) in + let c2 = v - (abs (c - v)) in + r1 + c1, r2 + c2 + else + r1, r2 + v) + (symbols_of_equality e1) (0, 0) + in + (others + (abs (common - card))), e1 + in + let _, current = EqualitySet.fold f pos_set initial in + Printf.printf "\nsymbols-based selection: %s\n\n" + (string_of_equality ~env current); + (Positive, current), + (([], neg_set), + (remove current pos_list, EqualitySet.remove current pos_set)) + | _ -> + let current = EqualitySet.min_elt pos_set in + let passive = + (neg_list, neg_set), + (remove current pos_list, EqualitySet.remove current pos_set) + in + (Positive, current), passive + ) + | _ -> + symbols_counter := !symbols_ratio; + let set_selection set = EqualitySet.min_elt set in if EqualitySet.is_empty neg_set then - let current = !set_selection pos_set in + let current = set_selection pos_set in let passive = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set) in (Positive, current), passive else - let current = !set_selection neg_set in + let current = set_selection neg_set in let passive = (remove current neg_list, EqualitySet.remove current neg_set), (pos_list, pos_set) @@ -156,8 +244,16 @@ let contains_empty env (negative, positive) = ;; -let forward_simplify env (sign, current) active = +let forward_simplify env ?(active=[]) ?passive (sign, current) = (* first step, remove already present equalities *) + let pn, pp = + match passive with + | None -> [], [] + | Some ((pn, _), (pp, _)) -> + (List.map (fun e -> Negative, e) pn), + (List.map (fun e -> Positive, e) pp) + in + let all = active @ pn @ pp in let duplicate = let rec aux = function | [] -> false @@ -166,7 +262,7 @@ let forward_simplify env (sign, current) active = else aux tl | _::tl -> aux tl in - aux active + aux all in if duplicate then None @@ -175,40 +271,61 @@ let forward_simplify env (sign, current) active = | [] -> Some (sign, current) | (Negative, _)::tl -> aux env (sign, current) tl | (Positive, equality)::tl -> - let newmeta, current = + let newmeta, newcurrent = demodulation !maxmeta env current equality in maxmeta := newmeta; - if is_identity env current then + if is_identity env newcurrent then None + else if newcurrent <> current then + aux env (sign, newcurrent) active else - aux env (sign, current) tl + aux env (sign, newcurrent) tl in - aux env (sign, current) active + aux env (sign, current) all ;; -let forward_simplify_new env (new_neg, new_pos) active = +let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) = + let pn, pp = + match passive with + | None -> [], [] + | Some ((pn, _), (pp, _)) -> + (List.map (fun e -> Negative, e) pn), + (List.map (fun e -> Positive, e) pp) + in + let all = active @ pn @ pp in let remove_identities equalities = let ok eq = not (is_identity env eq) in List.filter ok equalities in - let rec simpl active target = - match active with + let rec simpl all' target = + match all' with | [] -> target | (Negative, _)::tl -> simpl tl target | (Positive, source)::tl -> - let newmeta, target = demodulation !maxmeta env target source in + let newmeta, newtarget = demodulation !maxmeta env target source in maxmeta := newmeta; - if is_identity env target then target - else simpl tl target + if is_identity env newtarget then newtarget + else if newtarget <> target then ( +(* Printf.printf "OK:\n%s\n%s\n" *) +(* (string_of_equality ~env target) *) +(* (string_of_equality ~env newtarget); *) +(* print_newline (); *) + simpl all newtarget + ) + else simpl tl newtarget + in + let new_neg = List.map (simpl all) new_neg + and new_pos = remove_identities (List.map (simpl all) new_pos) in + let new_pos_set = + List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos in - let new_neg = List.map (simpl active) new_neg - and new_pos = List.map (simpl active) new_pos in - new_neg, remove_identities new_pos + new_neg, EqualitySet.elements new_pos_set ;; -let backward_simplify env (sign, current) active = +(* +let backward_simplify_active env (sign, current) active = match sign with | Negative -> active | Positive -> @@ -234,17 +351,75 @@ let backward_simplify env (sign, current) active = (fun (s, eq) res -> if find eq res then res else (s, eq)::res) active [] ;; +*) + + +let backward_simplify_active env (new_neg, new_pos) active = + let new_pos = List.map (fun e -> Positive, e) new_pos in + let active = + List.fold_right + (fun (s, equality) res -> + match forward_simplify env ~active:new_pos (s, equality) with + | None -> res + | Some e -> e::res) + active [] + in + let find eq1 where = + List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where + in + List.fold_right + (fun (s, eq) res -> + if (is_identity env eq) || (find eq res) then + res + else + (s, eq)::res) + active [] +;; + + +let backward_simplify_passive env (new_neg, new_pos) passive = + let new_pos = List.map (fun e -> Positive, e) new_pos in + let (nl, ns), (pl, ps) = passive in + let f sign equality (resl, ress, newn) = + match forward_simplify env ~active:new_pos (sign, equality) with + | None -> resl, EqualitySet.remove equality ress, newn + | Some (s, e) -> + if equality = e then + equality::resl, ress, newn + else + let ress = EqualitySet.remove equality ress in + resl, ress, e::newn + in + let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, []) + and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in + match newn, newp with + | [], [] -> ((nl, ns), (pl, ps)), None + | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp) +;; + + +let backward_simplify env ?(active=[]) ?passive new' = + let active = backward_simplify_active env new' active in + match passive with + | None -> + active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None + | Some passive -> + let passive, new' = + backward_simplify_passive env new' passive in + active, passive, new' +;; + let rec given_clause env passive active = match passive_is_empty passive with | true -> Failure | false -> (* Printf.printf "before select\n"; *) - let (sign, current), passive = select env passive in + let (sign, current), passive = select env passive active in (* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) (* (string_of_sign sign) (string_of_equality ~env current); *) - match forward_simplify env (sign, current) active with + match forward_simplify env (sign, current) ~active ~passive with | None when sign = Negative -> Printf.printf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current); @@ -257,56 +432,148 @@ let rec given_clause env passive active = (* print_newline (); *) given_clause env passive active | Some (sign, current) -> -(* Printf.printf "selected: %s %s" *) -(* (string_of_sign sign) (string_of_equality ~env current); *) -(* print_newline (); *) + print_endline "\n================================================"; + Printf.printf "selected: %s %s" + (string_of_sign sign) (string_of_equality ~env current); + print_newline (); let new' = infer env sign current active in - let new' = forward_simplify_new env new' active in - - let active = - backward_simplify env (sign, current) active -(* match new' with *) -(* | [], [] -> backward_simplify env (sign, current) active *) -(* | _ -> active *) - in + let res, proof = contains_empty env new' in + if res then + Success (proof, env) + else + let new' = forward_simplify_new env new' ~active in + + (* let active, passive, retained = *) + (* backward_simplify env [(sign, current)] ~active ~passive *) + (* in *) + let active = + match sign with + | Negative -> active + | Positive -> + let active, _, _ = + backward_simplify env ([], [current]) ~active + in + active + in + let _ = + Printf.printf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) active))); + print_newline (); + in + let _ = + match new' with + | neg, pos -> + Printf.printf "new':\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))); + print_newline (); + in + match contains_empty env new' with + | false, _ -> + let active = + match sign with + | Negative -> (sign, current)::active + | Positive -> active @ [(sign, current)] + in + let passive = add_to_passive passive new' in + let (_, ns), (_, ps) = passive in + Printf.printf "passive:\n%s\n" + (String.concat "\n" + ((List.map (fun e -> "Negative " ^ + (string_of_equality ~env e)) + (EqualitySet.elements ns)) @ + (List.map (fun e -> "Positive " ^ + (string_of_equality ~env e)) + (EqualitySet.elements ps)))); + print_newline (); + given_clause env passive active + | true, proof -> + Success (proof, env) +;; - print_endline "\n================================================"; - let _ = - Printf.printf "active:\n%s\n" + +(* +let rec given_clause env passive active = + match passive_is_empty passive with + | true -> Failure + | false -> +(* Printf.printf "before select\n"; *) + let (sign, current), passive = select env passive active in +(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) +(* (string_of_sign sign) (string_of_equality ~env current); *) + print_endline "\n================================================"; + Printf.printf "selected: %s %s" + (string_of_sign sign) (string_of_equality ~env current); + print_newline (); + + let new' = infer env sign current active in + + let rec simplify new' active passive = + let new' = forward_simplify_new env new' ~active ~passive in + let active, passive, retained = + backward_simplify env new' ~active ~passive + in + match retained with + | None -> active, passive, new' + | Some (rn, rp) -> + let nn, np = new' in + simplify (nn @ rn, np @ rp) active passive + in + let active, passive, new' = simplify new' active passive in + let _ = + Printf.printf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) active))); + print_newline (); + in + let _ = + match new' with + | neg, pos -> + Printf.printf "new':\n%s\n" (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) active))); + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))); print_newline (); + in + match contains_empty env new' with + | false, _ -> + let active = + match sign with + | Negative -> (sign, current)::active + | Positive -> active @ [(sign, current)] in - -(* let _ = *) -(* match new' with *) -(* | neg, pos -> *) -(* Printf.printf "new':\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) neg) @ *) -(* (List.map *) -(* (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) pos))); *) -(* print_newline (); *) -(* in *) - match contains_empty env new' with - | false, _ -> - let active = - match sign with - | Negative -> (sign, current)::active - | Positive -> active @ [(sign, current)] - in - let passive = add_to_passive passive new' in - given_clause env passive active - | true, proof -> - Success (proof, env) + let passive = add_to_passive passive new' in + let (_, ns), (_, ps) = passive in + Printf.printf "passive:\n%s\n" + (String.concat "\n" + ((List.map (fun e -> "Negative " ^ + (string_of_equality ~env e)) + (EqualitySet.elements ns)) @ + (List.map (fun e -> "Positive " ^ + (string_of_equality ~env e)) + (EqualitySet.elements ps)))); + print_newline (); + given_clause env passive active + | true, proof -> + Success (proof, env) ;; +*) let get_from_user () = @@ -354,17 +621,17 @@ let main () = (function (_, (ty, t1, t2), _, _) -> let w1 = weight_of_term t1 in let w2 = weight_of_term t2 in - let res = nonrec_kbo t1 t2 in + let res = !compare_terms t1 t2 in Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty) (PP.ppterm t1) (string_of_weight w1) (string_of_comparison res) (PP.ppterm t2) (string_of_weight w2)) equalities; print_endline "--------------------------------------------------"; - let start = Sys.time () in + let start = Unix.gettimeofday () in print_endline "GO!"; let res = given_clause env passive active in - let finish = Sys.time () in + let finish = Unix.gettimeofday () in match res with | Failure -> Printf.printf "NO proof found! :-(\n\n" @@ -381,17 +648,23 @@ let main () = let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; let _ = - let set_ratio v = weight_age_ratio := v; weight_age_counter := v - and set_sel () = set_selection := (fun s -> EqualitySet.max_elt s) + let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) + and set_sel v = symbols_ratio := v; symbols_counter := v; and set_conf f = configuration_file := f + and set_lpo () = Utils.compare_terms := lpo + and set_kbo () = Utils.compare_terms := nonrec_kbo in Arg.parse [ - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio"; + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)"; - "-i", Arg.Unit set_sel, - "Inverse selection (select heaviest equalities before)"; + "-s", Arg.Int set_sel, + "symbols-based selection ratio (relative to the weight ratio)"; "-c", Arg.String set_conf, "Configuration file (for the db connection)"; + + "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; + + "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; ] (fun a -> ()) "Usage:" in Helm_registry.load_from !configuration_file;