X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=dbc85261b87385771cc457f5407ed14a1ccf6984;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=405ba15a632307b773a22a1b68d20a1615344450;hpb=03cff55eef08d25984bc92080e4cac93889f3ba7;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 405ba15a6..dbc85261b 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -15,21 +15,29 @@ let string_of_sign = function ;; -let string_of_equality ?env = - match env with - | None -> ( - function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) - (CicPp.ppterm left) (CicPp.ppterm right) - ) - | Some (_, context, _) -> ( - let names = names_of_context context in - function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) - (CicPp.pp left names) (CicPp.pp right names) - ) +(* +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 ;; @@ -40,32 +48,146 @@ struct let compare eq1 eq2 = match meta_convertibility_eq eq1 eq2 with | true -> 0 - | false -> Pervasives.compare eq1 eq2 + | false -> + let _, (ty, left, right), _, _ = eq1 + and _, (ty', left', right'), _, _ = eq2 in + let weight_of t = fst (weight_of_term ~consider_metas:false t) in + let w1 = (weight_of ty) + (weight_of left) + (weight_of right) + and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in + match Pervasives.compare w1 w2 with + | 0 -> Pervasives.compare eq1 eq2 + | res -> res end module EqualitySet = Set.Make(OrderedEquality);; - -let select env passive = - match passive with - | hd::tl, pos -> (Negative, hd), (tl, pos) - | [], hd::tl -> (Positive, hd), ([], tl) - | _, _ -> assert false +let weight_age_ratio = ref 0;; (* settable by the user from the command line *) +let weight_age_counter = ref !weight_age_ratio;; + +let symbols_ratio = ref 0;; +let symbols_counter = ref 0;; + + +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 + | 0 -> ( + weight_age_counter := !weight_age_ratio; + match neg_list, pos_list with + | hd::tl, pos -> + (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set)) + | [], hd::tl -> + (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set)) + | _, _ -> assert false + ) + | _ 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 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 passive = + (remove current neg_list, EqualitySet.remove current neg_set), + (pos_list, pos_set) + in + (Negative, current), passive ;; -(* -let select env passive = - match passive with - | neg, pos when EqualitySet.is_empty neg -> - let elem = EqualitySet.min_elt pos in - (Positive, elem), (neg, EqualitySet.remove elem pos) - | neg, pos -> - let elem = EqualitySet.min_elt neg in - (Negative, elem), (EqualitySet.remove elem neg, pos) +let make_passive neg pos = + let set_of equalities = + List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities + in + (neg, set_of neg), (pos, set_of pos) +;; + + +let add_to_passive passive (new_neg, new_pos) = + let (neg_list, neg_set), (pos_list, pos_set) = passive in + let ok set equality = not (EqualitySet.mem equality set) in + let neg = List.filter (ok neg_set) new_neg + and pos = List.filter (ok pos_set) new_pos in + let add set equalities = + List.fold_left (fun s e -> EqualitySet.add e s) set equalities + in + (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos) +;; + + +let passive_is_empty = function + | ([], _), ([], _) -> true + | _ -> false ;; -*) (* TODO: find a better way! *) @@ -122,81 +244,88 @@ let contains_empty env (negative, positive) = ;; -let add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) = - let find sign eq1 eq2 = - if meta_convertibility_eq eq1 eq2 then ( -(* Printf.printf "Trovato equazione duplicata di segno %s\n%s\n\n" *) -(* (string_of_sign sign) (string_of_equality eq1); *) - true - ) else - false +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 ok sign equalities equality = - not (List.exists (find sign equality) equalities) + let all = active @ pn @ pp in + let duplicate = + let rec aux = function + | [] -> false + | (s, eq)::tl when s = sign -> + if meta_convertibility_eq current eq then true + else aux tl + | _::tl -> aux tl + in + aux all in - let neg = List.filter (ok Negative passive_neg) new_neg in - let pos = List.filter (ok Positive passive_pos) new_pos in -(* let neg, pos = new_neg, new_pos in *) - (neg @ passive_neg, passive_pos @ pos) -;; - - -let is_identity ((_, context, ugraph) as env) = function - | ((_, (ty, left, right), _, _) as equality) -> - let res = - (left = right || - (fst (CicReduction.are_convertible context left right ugraph))) - in -(* if res then ( *) -(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *) -(* print_newline (); *) -(* ); *) - res -;; - - -let forward_simplify env (sign, current) active = -(* if sign = Negative then *) -(* Some (sign, current) *) -(* else *) - let rec aux env (sign, current) = - function - | [] -> Some (sign, current) - | (Negative, _)::tl -> aux env (sign, current) tl - | (Positive, equality)::tl -> - let newmeta, current = demodulation !maxmeta env current equality in - maxmeta := newmeta; - if is_identity env current then - None - else - aux env (sign, current) tl + if duplicate then + None + else + let rec aux env (sign, current) = function + | [] -> Some (sign, current) + | (Negative, _)::tl -> aux env (sign, current) tl + | (Positive, equality)::tl -> + let newmeta, newcurrent = + demodulation !maxmeta env current equality in + maxmeta := newmeta; + if is_identity env newcurrent then + None + else if newcurrent <> current then + aux env (sign, newcurrent) active + else + 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 -> @@ -222,27 +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 add_to_passive (passive_neg, passive_pos) (new_neg, new_pos) = - let add_all = List.fold_left (fun res eq -> EqualitySet.add eq res) in - add_all passive_neg new_neg, add_all passive_pos new_pos + +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 rec given_clause env passive active = +let backward_simplify env ?(active=[]) ?passive new' = + let active = backward_simplify_active env new' active in match passive with -(* | s1, s2 when (EqualitySet.is_empty s1) && (EqualitySet.is_empty s2) -> *) -(* Failure *) - | [], [] -> Failure - | passive -> + | 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); @@ -250,60 +427,153 @@ let rec given_clause env passive active = let proof, _, _, _ = current in Success (Some proof, env) | None -> - Printf.printf "avanti... %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); +(* Printf.printf "avanti... %s %s" (string_of_sign sign) *) +(* (string_of_equality ~env current); *) +(* print_newline (); *) given_clause env passive active | Some (sign, current) -> -(* Printf.printf "sign: %s\ncurrent: %s\n" *) -(* (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 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) +;; - let new' = forward_simplify_new env new' active in - - 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 () = @@ -341,12 +611,7 @@ let main () = let term_equality = equality_of_term meta_proof goal in let meta_proof, (eq_ty, left, right), _, _ = term_equality in let active = [] in -(* let passive = *) -(* (EqualitySet.singleton term_equality, *) -(* List.fold_left *) -(* (fun res eq -> EqualitySet.add eq res) EqualitySet.empty equalities) *) -(* in *) - let passive = [term_equality], equalities in + let passive = make_passive [term_equality] equalities in Printf.printf "\ncurrent goal: %s ={%s} %s\n" (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -356,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" @@ -380,8 +645,27 @@ let main () = ;; +let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; + let _ = - let configuration_file = "../../gTopLevel/gTopLevel.conf.xml" in - Helm_registry.load_from configuration_file + 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 (default: 0)"; + + "-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; main ()