X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=6d5ecee159a8ba72f0d39b4351af16a044d837eb;hb=162a34842afbb574f89e3a358a79a310e7ec8b16;hp=413c7b15ea7bd760ed301b64f46d025336c3a646;hpb=a822b6e6080d6030257037bdf1f475bfa1eeb75a;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 413c7b15e..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 ;; @@ -1005,9 +1065,9 @@ let main dbd term metasenv ugraph = let _, metasenv, meta_proof, _ = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in -(* let library_equalities, maxm = *) -(* find_library_equalities ~dbd context (proof, goal') (maxm+1) *) -(* in *) + let library_equalities, maxm = + find_library_equalities ~dbd context (proof, goal') (maxm+2) + in maxmeta := maxm+2; (* TODO ugly!! *) let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = @@ -1023,84 +1083,136 @@ let main dbd term metasenv ugraph = try let term_equality = equality_of_term new_meta_goal goal in let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in - let active = make_active () in - let passive = - make_passive [term_equality] (equalities (* @ library_equalities *)) - in - Printf.printf "\ncurrent goal: %s\n" - (string_of_equality ~env term_equality); - Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); - Printf.printf "\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (string_of_equality ~env) - equalities)); - print_endline "--------------------------------------------------"; - let start = Unix.gettimeofday () in - print_endline "GO!"; - start_time := Unix.gettimeofday (); - let res = - (if !use_fullred then given_clause_fullred else given_clause) - env passive active - in - let finish = Unix.gettimeofday () in - let _ = - match res with - | ParamodulationFailure -> - Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some goal, env) -> - let proof = Inference.build_proof_term goal in - let newmetasenv = + if is_identity env term_equality then + let proof = + Cic.Appl [Cic.MutConstruct (* reflexivity *) + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + eq_ty; left] + in + let _ = + Printf.printf "OK, found a proof!\n"; + let names = names_of_context context in + print_endline (PP.pp proof names) + in + () + else + 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 m (_, _, _, menv, _) -> m @ menv) metasenv equalities + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active in - let _ = - try - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + 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 - Printf.printf "OK, found a proof!\n"; - (* REMEMBER: we have to instantiate meta_proof, we should use - apply the "apply" tactic to proof and status - *) - let names = names_of_context context in - print_endline (PP.pp proof names); - (* print_endline (PP.ppterm proof); *) - - print_endline (string_of_float (finish -. start)); - Printf.printf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug))); - with e -> - Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e); - Printf.printf "MAXMETA USED: %d\n" !maxmeta; - in - () - - | ParamodulationSuccess (None, env) -> - Printf.printf "Success, but no proof?!?\n\n" - in - Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ - "forward_simpl_new_time: %.9f\n" ^^ - "backward_simpl_time: %.9f\n") - !infer_time !forward_simpl_time !forward_simpl_new_time - !backward_simpl_time; - Printf.printf "passive_maintainance_time: %.9f\n" - !passive_maintainance_time; - Printf.printf " successful unification/matching time: %.9f\n" - !Indexing.match_unif_time_ok; - Printf.printf " failed unification/matching time: %.9f\n" - !Indexing.match_unif_time_no; - Printf.printf " indexing retrieval time: %.9f\n" - !Indexing.indexing_retrieval_time; - Printf.printf " demodulate_term.build_newtarget_time: %.9f\n" - !Indexing.build_newtarget_time; - Printf.printf "derived %d clauses, kept %d clauses.\n" - !derived_clauses !kept_clauses; + 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); + Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) + (equalities @ library_equalities))); + print_endline "--------------------------------------------------"; + let start = Unix.gettimeofday () in + print_endline "GO!"; + start_time := Unix.gettimeofday (); + let res = + (if !use_fullred then given_clause_fullred else given_clause) + env passive active + in + let finish = Unix.gettimeofday () in + let _ = + match res with + | ParamodulationFailure -> + Printf.printf "NO proof found! :-(\n\n" + | ParamodulationSuccess (Some goal, env) -> + let proof = Inference.build_proof_term goal in + let newmetasenv = + List.fold_left + (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities + in + let _ = + try + let ty, ug = + CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + in + Printf.printf "OK, found a proof!\n"; + (* REMEMBER: we have to instantiate meta_proof, we should use + apply the "apply" tactic to proof and status + *) + let names = names_of_context context in + print_endline (PP.pp proof names); + (* print_endline (PP.ppterm proof); *) + + print_endline (string_of_float (finish -. start)); + Printf.printf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible + context type_of_goal ty ug))); + 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 + () + + | ParamodulationSuccess (None, env) -> + Printf.printf "Success, but no proof?!?\n\n" + in + Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ + "forward_simpl_new_time: %.9f\n" ^^ + "backward_simpl_time: %.9f\n") + !infer_time !forward_simpl_time !forward_simpl_new_time + !backward_simpl_time; + Printf.printf "passive_maintainance_time: %.9f\n" + !passive_maintainance_time; + Printf.printf " successful unification/matching time: %.9f\n" + !Indexing.match_unif_time_ok; + Printf.printf " failed unification/matching time: %.9f\n" + !Indexing.match_unif_time_no; + Printf.printf " indexing retrieval time: %.9f\n" + !Indexing.indexing_retrieval_time; + Printf.printf " demodulate_term.build_newtarget_time: %.9f\n" + !Indexing.build_newtarget_time; + Printf.printf "derived %d clauses, kept %d clauses.\n" + !derived_clauses !kept_clauses; with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); raise exc @@ -1114,10 +1226,6 @@ let saturate dbd (proof, goal) = let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in - let library_equalities, maxm = - find_library_equalities ~dbd context (proof, goal') (maxm+2) - in - maxmeta := maxm+2; let new_meta_goal, metasenv, type_of_goal = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -1130,22 +1238,80 @@ let saturate dbd (proof, goal) = let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in (* try *) - let term_equality = equality_of_term new_meta_goal goal in - let active = make_active () in - let passive = - make_passive [term_equality] (equalities @ library_equalities) - in - let res = given_clause_fullred env passive active in - match res with - | ParamodulationSuccess (Some goal, env) -> - debug_print "OK, found a proof!"; - let proof = Inference.build_proof_term goal in - let names = names_of_context context in - let newmetasenv = - let i1 = - match new_meta_goal with - | C.Meta (i, _) -> i | _ -> assert false + let term_equality = equality_of_term new_meta_goal goal in + let res, time = + if is_identity env term_equality then + let w, _, (eq_ty, left, right, o), m, a = term_equality in + let proof = + Cic.Appl [Cic.MutConstruct (* reflexivity *) + (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + eq_ty; left] + in + (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 in + let start = Unix.gettimeofday () in + let res = given_clause_fullred env passive active in + let finish = Unix.gettimeofday () in + (res, finish -. start) + in + match res with + | ParamodulationSuccess (Some goal, env) -> + debug_print "OK, found a proof!"; + let proof = Inference.build_proof_term goal in + let names = names_of_context context in + let newmetasenv = + let i1 = + match new_meta_goal with + | C.Meta (i, _) -> i | _ -> assert false + in (* let i2 = *) (* match meta_proof with *) (* | C.Meta (i, _) -> i *) @@ -1155,49 +1321,50 @@ let saturate dbd (proof, goal) = (* print_newline (); *) (* assert false *) (* in *) - List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv - in - let newstatus = - try - let ty, ug = - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph - in - debug_print (CicPp.pp proof [](* names *)); - debug_print - (Printf.sprintf - "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" - (CicPp.pp type_of_goal names) (CicPp.pp ty names) - (string_of_bool - (fst (CicReduction.are_convertible - context type_of_goal ty ug)))); - let equality_for_replace i t1 = - match t1 with - | C.Meta (n, _) -> n = i - | _ -> false - in - let real_proof = - ProofEngineReduction.replace - ~equality:equality_for_replace - ~what:[goal'] ~with_what:[proof] - ~where:meta_proof - in - debug_print ( - Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" - (match uri with Some uri -> UriManager.string_of_uri uri - | None -> "") - (print_metasenv newmetasenv) - (CicPp.pp real_proof [](* names *)) - (CicPp.pp term_to_prove names)); - ((uri, newmetasenv, real_proof, term_to_prove), []) - with CicTypeChecker.TypeCheckerFailure _ -> - debug_print "THE PROOF DOESN'T TYPECHECK!!!"; - debug_print (CicPp.pp proof names); - raise - (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck") - in - newstatus - | _ -> - raise (ProofEngineTypes.Fail "NO proof found") + List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv + in + let newstatus = + try + let ty, ug = + CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + in + debug_print (CicPp.pp proof [](* names *)); + debug_print + (Printf.sprintf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible + context type_of_goal ty ug)))); + let equality_for_replace i t1 = + match t1 with + | C.Meta (n, _) -> n = i + | _ -> false + in + let real_proof = + ProofEngineReduction.replace + ~equality:equality_for_replace + ~what:[goal'] ~with_what:[proof] + ~where:meta_proof + in + debug_print ( + Printf.sprintf "status:\n%s\n%s\n%s\n%s\n" + (match uri with Some uri -> UriManager.string_of_uri uri + | None -> "") + (print_metasenv newmetasenv) + (CicPp.pp real_proof [](* names *)) + (CicPp.pp term_to_prove names)); + ((uri, newmetasenv, real_proof, term_to_prove), []) + with CicTypeChecker.TypeCheckerFailure _ -> + debug_print "THE PROOF DOESN'T TYPECHECK!!!"; + debug_print (CicPp.pp proof names); + 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") (* with e -> *) (* raise (Failure "saturation failed") *) ;;