X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=6d5ecee159a8ba72f0d39b4351af16a044d837eb;hb=1bcae23ef41ad2110426eebd97671d27d09213a3;hp=5d5273d51746eb0517e281b719a1cc19a046c7be;hpb=758dbd74dccfb2491b59e4267600caf1d485e77a;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 5d5273d51..6d5ecee15 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -23,11 +23,14 @@ let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; -let weight_age_ratio = ref 3;; (* settable by the user from the command line *) +let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio;; -let symbols_ratio = ref 2;; +let symbols_ratio = ref (* 0 *) 3;; let symbols_counter = ref 0;; +(* non-recursive Knuth-Bendix term ordering by default *) +Utils.compare_terms := Utils.nonrec_kbo;; + (* statistics... *) let derived_clauses = ref 0;; let kept_clauses = ref 0;; @@ -279,8 +282,12 @@ let prune_passive howmany (active, _) passive = let (nl, ns), (pl, ps), tbl = passive in let howmany = float_of_int howmany and ratio = float_of_int !weight_age_ratio in - let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.)) - and in_age = int_of_float (howmany /. (ratio +. 1.)) in + let round v = + let t = ceil v in + int_of_float (if t -. v < 0.5 then t else v) + in + let in_weight = round (howmany *. ratio /. (ratio +. 1.)) + and in_age = round (howmany /. (ratio +. 1.)) in debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age); let symbols, card = match active with @@ -362,7 +369,7 @@ let prune_passive howmany (active, _) passive = let _, ps, pl = picka in_age ps pl in if not (EqualitySet.is_empty ps) then (* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *) - maximal_retained_equality := Some (EqualitySet.max_elt ps); + maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) @@ -409,11 +416,52 @@ let infer env sign current (active_list, active_table) = in derived_clauses := !derived_clauses + (List.length new_neg) + (List.length new_pos); - match (* !maximal_weight *)!maximal_retained_equality with + match !maximal_retained_equality with | None -> new_neg, new_pos - | Some (* w *) eq -> - let new_pos = - List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in + | Some eq -> + (* if we have a maximal_retained_equality, we can discard all equalities + "greater" than it, as they will never be reached... An equality is + greater than maximal_retained_equality if it is bigger + wrt. OrderedEquality.compare and it is less similar than + maximal_retained_equality to the current goal *) + let symbols, card = + match active_list with + | (Negative, e)::_ -> + let symbols = symbols_of_equality e in + let card = TermMap.fold (fun k v res -> res + v) symbols 0 in + Some symbols, card + | _ -> None, 0 + in + let new_pos = + match symbols with + | None -> + List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos + | Some symbols -> + let filterfun e = + if OrderedEquality.compare e eq <= 0 then + true + else + let foldfun 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 + in + let initial = + let common, others = + TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in + others + (abs (common - card)) + in + let common, others = + TermMap.fold foldfun (symbols_of_equality e) (0, 0) in + let c = others + (abs (common - card)) in + if c < initial then true else false + in + List.filter filterfun new_pos + in new_neg, new_pos ;; @@ -444,7 +492,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = in let all = if pl = [] then active_list else active_list @ pl in -(* let rec find_duplicate sign current = function *) + (* let rec find_duplicate sign current = function *) (* | [] -> false *) (* | (s, eq)::tl when s = sign -> *) (* if meta_convertibility_eq current eq then true *) @@ -633,18 +681,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = ;; -let backward_simplify_active env new_pos new_table active = +let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in let active_list, newa = List.fold_right (fun (s, equality) (res, newn) -> - match forward_simplify env (s, equality) (new_pos, new_table) with - | None -> res, newn - | Some (s, e) -> - if equality = e then - (s, e)::res, newn - else - res, (s, e)::newn) + let ew, _, _, _, _ = equality in + if ew < min_weight then + (s, equality)::res, newn + else + match forward_simplify env (s, equality) (new_pos, new_table) with + | None -> res, newn + | Some (s, e) -> + if equality = e then + (s, e)::res, newn + else + res, (s, e)::newn) active_list ([], []) in let find eq1 where = @@ -677,17 +729,22 @@ let backward_simplify_active env new_pos new_table active = ;; -let backward_simplify_passive env new_pos new_table passive = +let backward_simplify_passive env new_pos new_table min_weight passive = let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - match forward_simplify env (sign, equality) (new_pos, new_table) 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 + let ew, _, _, _, _ = equality in + if ew < min_weight then +(* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *) + equality::resl, ress, newn + else + match forward_simplify env (sign, equality) (new_pos, new_table) 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 @@ -702,18 +759,21 @@ let backward_simplify_passive env new_pos new_table passive = let backward_simplify env new' ?passive active = - let new_pos, new_table = + let new_pos, new_table, min_weight = List.fold_left - (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) - ([], Indexing.empty_table ()) (snd new') - in - let active, newa = backward_simplify_active env new_pos new_table active in + (fun (l, t, w) e -> + let ew, _, _, _, _ = e in + (Positive, e)::l, Indexing.index t e, min ew w) + ([], Indexing.empty_table (), 1000000) (snd new') + in + let active, newa = + backward_simplify_active env new_pos new_table min_weight active in match passive with | None -> active, (make_passive [] []), newa, None | Some passive -> let passive, newp = - backward_simplify_passive env new_pos new_table passive in + backward_simplify_passive env new_pos new_table min_weight passive in active, passive, newa, newp ;; @@ -1036,10 +1096,48 @@ let main dbd term metasenv ugraph = in () else - let active = make_active () in - let passive = - make_passive [term_equality] (equalities @ library_equalities) + let equalities = + let equalities = equalities @ library_equalities in + debug_print ( + Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities))); + debug_print "SIMPLYFYING EQUALITIES..."; + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) + in + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) + in + debug_print ( + Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res))); + res in + let active = make_active () in + let passive = make_passive [term_equality] equalities in Printf.printf "\ncurrent goal: %s\n" (string_of_equality ~env term_equality); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); @@ -1048,7 +1146,7 @@ let main dbd term metasenv ugraph = (String.concat "\n" (List.map (string_of_equality ~env) - equalities)); + (equalities @ library_equalities))); print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; @@ -1091,6 +1189,7 @@ let main dbd term metasenv ugraph = with e -> Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); Printf.printf "MAXMETA USED: %d\n" !maxmeta; + print_endline (string_of_float (finish -. start)); in () @@ -1140,7 +1239,7 @@ let saturate dbd (proof, goal) = let env = (metasenv, context, ugraph) in (* try *) let term_equality = equality_of_term new_meta_goal goal in - let res = + let res, time = if is_identity env term_equality then let w, _, (eq_ty, left, right, o), m, a = term_equality in let proof = @@ -1148,21 +1247,60 @@ let saturate dbd (proof, goal) = (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); eq_ty; left] in - ParamodulationSuccess - (Some (0, Inference.BasicProof proof, - (eq_ty, left, right, o), m, a), env) + (ParamodulationSuccess + (Some (0, Inference.BasicProof proof, + (eq_ty, left, right, o), m, a), env), 0.) else let library_equalities, maxm = find_library_equalities ~dbd context (proof, goal') (maxm+2) in maxmeta := maxm+2; - + let equalities = + let equalities = equalities @ library_equalities in + debug_print ( + Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities))); + debug_print "SIMPLYFYING EQUALITIES..."; + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active + in + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) + in + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) + in + debug_print ( + Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res))); + res + in let active = make_active () in - let passive = - make_passive [term_equality] (equalities @ library_equalities) - in + let passive = make_passive [term_equality] equalities in + let start = Unix.gettimeofday () in let res = given_clause_fullred env passive active in - res + let finish = Unix.gettimeofday () in + (res, finish -. start) in match res with | ParamodulationSuccess (Some goal, env) -> @@ -1223,6 +1361,7 @@ let saturate dbd (proof, goal) = raise (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck") in + debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time); newstatus | _ -> raise (ProofEngineTypes.Fail "NO proof found")