From: Alberto Griggio Date: Mon, 10 Oct 2005 16:16:04 +0000 (+0000) Subject: fixed a bug (status not reset properly between calls), tried some other X-Git-Tag: V_0_7_2_3~225 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9a76af2c3c2a70f26b0315225b596bcba1a585d;p=helm.git fixed a bug (status not reset properly between calls), tried some other euristics (not very satisfactory... :-( ) --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index a7b2c3039..497c42636 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -150,6 +150,10 @@ let get_candidates mode trie term = (* DISCRIMINATION TREES *) +let init_index () = + Hashtbl.clear Discrimination_tree.arities; +;; + let empty_table () = Discrimination_tree.DiscriminationTree.empty ;; @@ -990,6 +994,16 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = (* | _, _, (_, left, right, _), _, _ -> *) (* not (fst (CR.are_convertible context left right ugraph)) *) (* in *) + let _ = + let env = metasenv, context, ugraph in + debug_print + (lazy + (Printf.sprintf "end of superposition_right:\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Positive " ^ + (Inference.string_of_equality ~env e)) (new1 @ new2)))))) + in let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index ac9934000..0556c442d 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1256,7 +1256,8 @@ let find_library_theorems dbd env status equalities_uris = in List.fold_left (fun s u -> UriManager.UriSet.add u s) - s [sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); eq_ind_r_URI ()] + s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); + eq_ind_r_URI ()] in let metasenv, context, ugraph = env in let candidates = @@ -1266,10 +1267,16 @@ let find_library_theorems dbd env status equalities_uris = else let t = CicUtil.term_of_uri uri in let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in - (t, ty, [])::l) + (uri, t, ty, [])::l) [] (MetadataQuery.signature_of_goal ~dbd status) in - candidates + let refl_equal = + let u = eq_XURI () in + let t = CicUtil.term_of_uri u in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + (u, t, ty, []) + in + refl_equal::candidates ;; @@ -1370,7 +1377,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = else let _, context, ty = CicUtil.lookup_meta i menv in (i, (context, Cic.Meta (j, l), ty))::s - with Not_found -> + with Not_found | CicUtil.Meta_not_found _ -> (* debug_print ("Not_found meta ?" ^ (string_of_int i)); *) s ) diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 560af55da..1d76aba7a 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -112,7 +112,7 @@ val find_library_equalities: val find_library_theorems: HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t -> - (Cic.term * Cic.term * Cic.metasenv) list + (UriManager.uri * Cic.term * Cic.term * Cic.metasenv) list val find_context_hypotheses: environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index ab39ff3de..af0861b60 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -15,6 +15,8 @@ let get_from_user ~(dbd:HMysql.dbd) = term, metasenv, ugraph ;; +let full = ref false;; + let _ = let module S = Saturation in let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v @@ -30,8 +32,10 @@ let _ = and set_time_limit v = S.time_limit := float_of_int v and set_width w = S.maxwidth := w and set_depth d = S.maxdepth := d + and set_full () = full := true in Arg.parse [ + "-full", Arg.Unit set_full, "Enable full mode"; "-f", Arg.Bool set_fullred, "Enable/disable full-reduction strategy (default: enabled)"; @@ -67,4 +71,4 @@ let dbd = HMysql.quick_connect () in let term, metasenv, ugraph = get_from_user ~dbd in -Saturation.main dbd term metasenv ugraph;; +Saturation.main dbd !full term metasenv ugraph;; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 4cf14ae18..825d6b8c8 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -48,6 +48,10 @@ type result = | ParamodulationSuccess of Inference.proof option * environment ;; +type goal = proof * Cic.metasenv * Cic.term;; + +type theorem = Cic.term * Cic.term * Cic.metasenv;; + (* let symbols_of_equality (_, (_, left, right), _, _) = @@ -799,6 +803,35 @@ let get_selection_estimate () = ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.))) ;; + +let make_goals goal = + let active = [] + and passive = [0, [goal]] in + active, passive +;; + + +let make_theorems theorems = + theorems, [] +(* let active = [] *) +(* and passive = theorems in *) +(* active, passive *) +;; + + +let activate_goal (active, passive) = + match passive with + | goal_conj::tl -> true, (goal_conj::active, tl) + | [] -> false, (active, passive) +;; + + +let activate_theorem (active, passive) = + match passive with + | theorem::tl -> true, (theorem::active, tl) + | [] -> false, (active, passive) +;; + let simplify_goal env goal ?passive (active_list, active_table) = let pl, passive_table = @@ -815,32 +848,50 @@ let simplify_goal env goal ?passive (active_list, active_table) = let newmeta, newgoal = Indexing.demodulation_goal !maxmeta env table goal in maxmeta := newmeta; - newgoal + goal != newgoal, newgoal in - let goal = + let changed, goal = match passive_table with | None -> demodulate active_table goal | Some passive_table -> - let goal = demodulate active_table goal in - demodulate passive_table goal + let changed, goal = demodulate active_table goal in + let changed', goal = demodulate passive_table goal in + (changed || changed'), goal in - let _ = - let p, _, t = goal in - debug_print - (lazy - (Printf.sprintf "Goal after demodulation: %s, %s" - (string_of_proof p) (CicPp.ppterm t))) - in - goal +(* let _ = *) +(* let p, _, t = goal in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "Goal after demodulation: %s, %s" *) +(* (string_of_proof p) (CicPp.ppterm t))) *) +(* in *) + changed, goal ;; let simplify_goals env goals ?passive active = - List.map - (fun (d, gl) -> - let gl = List.map (fun g -> simplify_goal env g ?passive active) gl in - d, gl) - goals + let a_goals, p_goals = goals in + let p_goals = + List.map + (fun (d, gl) -> + let gl = + List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in + d, gl) + p_goals + in + let goals = + List.fold_left + (fun (a, p) (d, gl) -> + let changed = ref false in + let gl = + List.map + (fun g -> + let c, g = simplify_goal env g ?passive active in + changed := !changed || c; g) gl in + if !changed then (a, (d, gl)::p) else ((d, gl)::a, p)) + ([], p_goals) a_goals + in + goals ;; @@ -854,18 +905,31 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = pn @ pp, Some pt in let all = if pl = [] then active_list else active_list @ pl in - + let a_theorems, p_theorems = theorems in let demodulate table theorem = let newmeta, newthm = Indexing.demodulation_theorem !maxmeta env table theorem in maxmeta := newmeta; - newthm + theorem != newthm, newthm in + let foldfun table (a, p) theorem = + let changed, theorem = demodulate table theorem in + if changed then (a, theorem::p) else (theorem::a, p) + in + let mapfun table theorem = snd (demodulate table theorem) in match passive_table with - | None -> List.map (demodulate active_table) theorems + | None -> + let p_theorems = List.map (mapfun active_table) p_theorems in + List.fold_left (foldfun active_table) ([], p_theorems) a_theorems +(* List.map (demodulate active_table) theorems *) | Some passive_table -> - let theorems = List.map (demodulate active_table) theorems in - List.map (demodulate passive_table) theorems + let p_theorems = List.map (mapfun active_table) p_theorems in + let p_theorems, a_theorems = + List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in + let p_theorems = List.map (mapfun passive_table) p_theorems in + List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems +(* let theorems = List.map (demodulate active_table) theorems in *) +(* List.map (demodulate passive_table) theorems *) ;; @@ -1001,8 +1065,8 @@ let apply_to_goal env theorems active goal = let proof, metas, term = goal in debug_print (lazy - (Printf.sprintf "apply_to_goal with goal: %s, %s" - (string_of_proof proof) (CicPp.ppterm term))); + (Printf.sprintf "apply_to_goal with goal: %s" + (* (string_of_proof proof) *)(CicPp.ppterm term))); let status = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in @@ -1078,11 +1142,21 @@ let apply_to_goal env theorems active goal = in debug_print (lazy - (Printf.sprintf "new sub goal: %s, %s" - (string_of_proof p') (CicPp.ppterm ty))); + (Printf.sprintf "new sub goal: %s" + (* (string_of_proof p') *)(CicPp.ppterm ty))); (p', menv, ty)) newgoals in + let goals = + let weight t = + let w, m = weight_of_term t in + w + 2 * (List.length m) + in + List.sort + (fun (_, _, t1) (_, _, t2) -> + Pervasives.compare (weight t1) (weight t2)) + goals + in (* debug_print *) (* (lazy *) (* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *) @@ -1119,27 +1193,27 @@ let apply_to_goal_conj env theorems active (depth, goals) = let rec aux = function | goal::tl -> let propagate_subst subst (proof, metas, term) = - debug_print - (lazy - (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" - (print_subst subst) (string_of_proof proof) - (CicPp.ppterm term))); +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" *) +(* (print_subst subst) (string_of_proof proof) *) +(* (CicPp.ppterm term))); *) let rec repl = function | NoProof -> NoProof | BasicProof t -> BasicProof (CicMetaSubst.apply_subst subst t) | ProofGoalBlock (p, pb) -> - debug_print (lazy "HERE"); +(* debug_print (lazy "HERE"); *) let pb' = repl pb in ProofGoalBlock (p, pb') | SubProof (t, i, p) -> let t' = CicMetaSubst.apply_subst subst t in - debug_print - (lazy - (Printf.sprintf - "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" - i (CicPp.ppterm t) (print_subst subst) - (CicPp.ppterm t'))); +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf *) +(* "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" *) +(* i (CicPp.ppterm t) (print_subst subst) *) +(* (CicPp.ppterm t'))); *) let p = repl p in SubProof (t', i, p) | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) @@ -1152,25 +1226,25 @@ let apply_to_goal_conj env theorems active (depth, goals) = | `No -> `No (depth, goals) | `GoOn sl (* (subst, gl) *) -> (* let tl = List.map (propagate_subst subst) tl in *) - debug_print (lazy "GO ON!!!"); +(* debug_print (lazy "GO ON!!!"); *) let l = List.map (fun (s, gl) -> (depth+1, gl @ (List.map (propagate_subst s) tl))) sl in - debug_print - (lazy - (Printf.sprintf "%s\n" - (String.concat "; " - (List.map - (fun (s, gl) -> - (Printf.sprintf "[%s]" - (String.concat "; " - (List.map - (fun (p, _, g) -> - (Printf.sprintf "<%s, %s>" - (string_of_proof p) - (CicPp.ppterm g))) gl)))) l)))); +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "%s\n" *) +(* (String.concat "; " *) +(* (List.map *) +(* (fun (s, gl) -> *) +(* (Printf.sprintf "[%s]" *) +(* (String.concat "; " *) +(* (List.map *) +(* (fun (p, _, g) -> *) +(* (Printf.sprintf "<%s, %s>" *) +(* (string_of_proof p) *) +(* (CicPp.ppterm g))) gl)))) l)))); *) `GoOn l (* (depth+1, gl @ tl) *) | `Ok (subst, gl) -> if tl = [] then @@ -1294,30 +1368,38 @@ let apply_to_goals env is_passive_empty theorems active goals = in true, GoalsSet.singleton newgoals | `GoOn newgoals -> - let print_set set msg = - debug_print - (lazy - (Printf.sprintf "%s:\n%s" msg - (String.concat "\n" - (GoalsSet.fold - (fun (d, gl) l -> - let gl' = - List.map (fun (_, _, t) -> CicPp.ppterm t) gl - in - let s = - Printf.sprintf "%d, [%s]" d - (String.concat "; " gl') - in - s::l) set [])))) - in - let set = add_to set (goals::tl) in +(* let print_set set msg = *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "%s:\n%s" msg *) +(* (String.concat "\n" *) +(* (GoalsSet.fold *) +(* (fun (d, gl) l -> *) +(* let gl' = *) +(* List.map (fun (_, _, t) -> CicPp.ppterm t) gl *) +(* in *) +(* let s = *) +(* Printf.sprintf "%d, [%s]" d *) +(* (String.concat "; " gl') *) +(* in *) +(* s::l) set [])))) *) +(* in *) + +(* let r, s = *) +(* try aux set tl with SearchSpaceOver -> false, GoalsSet.empty *) +(* in *) +(* if r then *) +(* r, s *) +(* else *) + + let set' = add_to set (goals::tl) in (* print_set set "SET BEFORE"; *) - let n = GoalsSet.cardinal set in - let set = add_to set newgoals in +(* let n = GoalsSet.cardinal set in *) + let set' = add_to set' newgoals in (* print_set set "SET AFTER"; *) - let m = GoalsSet.cardinal set in +(* let m = GoalsSet.cardinal set in *) (* if n < m then *) - false, set + false, set' (* else *) (* let _ = print_set set "SET didn't change" in *) (* aux set tl *) @@ -1339,7 +1421,148 @@ let apply_to_goals env is_passive_empty theorems active goals = ;; -let rec given_clause env goals theorems passive active = +let apply_goal_to_theorems dbd env theorems active goals = +(* let theorems, _ = theorems in *) + let context_hyp, library_thms = theorems in + let thm_uris = + List.fold_left + (fun s (u, _, _, _) -> UriManager.UriSet.add u s) + UriManager.UriSet.empty library_thms + in + let a_goals, p_goals = goals in + let goal = List.hd a_goals in + let rec aux = function + | [] -> false, (a_goals, p_goals) + | theorem::tl -> + let res = apply_to_goal_conj env [theorem] active goal in + match res with + | `Ok newgoals -> + true, ([newgoals], []) + | `No _ -> + aux tl +(* false, (a_goals, p_goals) *) + | `GoOn newgoals -> + let res, (ag, pg) = aux tl in + if res then + res, (ag, pg) + else + let newgoals = + List.filter + (fun (d, gl) -> + (d <= !maxdepth) && (List.length gl) <= !maxwidth) + newgoals in + let p_goals = newgoals @ pg in + let p_goals = + List.stable_sort + (fun (d1, l1) (d2, l2) -> (List.length l1) - (List.length l2)) + p_goals + in + res, (ag, p_goals) + in + let theorems = +(* let ty = *) +(* match goal with *) +(* | (_, (_, _, t)::_) -> t *) +(* | _ -> assert false *) +(* in *) +(* if CicUtil.is_meta_closed ty then *) +(* let _ = *) +(* debug_print (lazy (Printf.sprintf "META CLOSED: %s" (CicPp.ppterm ty))) *) +(* in *) +(* let metasenv, context, ugraph = env in *) +(* let uris = *) +(* MetadataConstraints.sigmatch ~dbd (MetadataConstraints.signature_of ty) *) +(* in *) +(* let uris = List.sort (fun (i, _) (j, _) -> Pervasives.compare i j) uris in *) +(* let uris = *) +(* List.filter *) +(* (fun u -> UriManager.UriSet.mem u thm_uris) (List.map snd uris) *) +(* in *) +(* List.map *) +(* (fun u -> *) +(* let t = CicUtil.term_of_uri u in *) +(* let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in *) +(* (t, ty, [])) *) +(* uris *) +(* else *) + List.map (fun (_, t, ty, m) -> (t, ty, m)) library_thms + in + aux (context_hyp @ theorems) +;; + + +let apply_theorem_to_goals env theorems active goals = + let a_goals, p_goals = goals in + let theorem = List.hd (fst theorems) in + let theorems = [theorem] in + let rec aux p = function + | [] -> false, ([], p) + | goal::tl -> + let res = apply_to_goal_conj env theorems active goal in + match res with + | `Ok newgoals -> true, ([newgoals], []) + | `No _ -> aux p tl + | `GoOn newgoals -> aux (newgoals @ p) tl + in + let ok, (a, p) = aux p_goals a_goals in + if ok then + ok, (a, p) + else + let p_goals = + List.stable_sort + (fun (d1, l1) (d2, l2) -> + let r = d2 - d1 in + if r <> 0 then r + else let r = (List.length l1) - (List.length l2) in + if r <> 0 then r + else + let res = ref 0 in + let _ = + List.exists2 + (fun (_, _, t1) (_, _, t2) -> + let r = Pervasives.compare t1 t2 in + if r <> 0 then (res := r; true) else false) l1 l2 + in !res) + p + in + ok, (a_goals, p_goals) +;; + + +let rec given_clause dbd env goals theorems passive active = + let goals = simplify_goals env goals active in + let ok, goals = activate_goal goals in +(* let theorems = simplify_theorems env theorems active in *) + if ok then + let ok, goals = apply_goal_to_theorems dbd env theorems active goals in + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_aux dbd env goals theorems passive active + else +(* let ok', theorems = activate_theorem theorems in *) + let ok', theorems = false, theorems in + if ok' then + let ok, goals = apply_theorem_to_goals env theorems active goals in + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_aux dbd env goals theorems passive active + else + if (passive_is_empty passive) then ParamodulationFailure + else given_clause_aux dbd env goals theorems passive active + +and given_clause_aux dbd env goals theorems passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in @@ -1366,95 +1589,91 @@ let rec given_clause env goals theorems passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); -(* let refl_equal = *) -(* CicUtil.term_of_uri *) -(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *) -(* in *) - let goals = simplify_goals env goals active in - let theorems = simplify_theorems env theorems active in - let is_passive_empty = passive_is_empty passive in - try - let ok, goals = apply_to_goals env is_passive_empty theorems active goals in - if ok then - let proof = - match goals with - | (_, [proof, _, _])::_ -> Some proof - | _ -> assert false - in - ParamodulationSuccess (proof, env) - else - match is_passive_empty (* passive_is_empty passive *) with - | true -> (* ParamodulationFailure *) - given_clause env goals theorems passive active - | false -> - let (sign, current), passive = select env goals passive active in - let time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in - let time2 = Unix.gettimeofday () in - forward_simpl_time := !forward_simpl_time +. (time2 -. time1); - match res with - | None -> - given_clause env goals theorems passive active - | Some (sign, current) -> - if (sign = Negative) && (is_identity env current) then ( - debug_print - (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current))); - let _, proof, _, _, _ = current in - ParamodulationSuccess (Some proof (* current *), env) - ) else ( - debug_print - (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) - (string_of_equality ~env current))); - - let t1 = Unix.gettimeofday () in - let new' = infer env sign current active in - let t2 = Unix.gettimeofday () in - infer_time := !infer_time +. (t2 -. t1); - - let res, goal' = contains_empty env new' in - if res then - let proof = - match goal' with - | Some goal -> let _, proof, _, _, _ = goal in Some proof - | None -> None - in - ParamodulationSuccess (proof (* goal *), env) - else - let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' active in - let t2 = Unix.gettimeofday () in - let _ = - forward_simpl_new_time := - !forward_simpl_new_time +. (t2 -. t1) - in - let active = - match sign with - | Negative -> active - | Positive -> - let t1 = Unix.gettimeofday () in - let active, _, newa, _ = - backward_simplify env ([], [current]) active +(* (\* let goals = simplify_goals env goals active in *\) *) +(* (\* let theorems = simplify_theorems env theorems active in *\) *) +(* let is_passive_empty = passive_is_empty passive in *) +(* try *) +(* let ok, goals = false, [] in (\* apply_to_goals env is_passive_empty theorems active goals in *\) *) +(* if ok then *) +(* let proof = *) +(* match goals with *) +(* | (_, [proof, _, _])::_ -> Some proof *) +(* | _ -> assert false *) +(* in *) +(* ParamodulationSuccess (proof, env) *) +(* else *) + match passive_is_empty passive with + | true -> (* ParamodulationFailure *) + given_clause dbd env goals theorems passive active + | false -> + let (sign, current), passive = select env (fst goals) passive active in + let time1 = Unix.gettimeofday () in + let res = forward_simplify env (sign, current) ~passive active in + let time2 = Unix.gettimeofday () in + forward_simpl_time := !forward_simpl_time +. (time2 -. time1); + match res with + | None -> + given_clause dbd env goals theorems passive active + | Some (sign, current) -> + if (sign = Negative) && (is_identity env current) then ( + debug_print + (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current))); + let _, proof, _, _, _ = current in + ParamodulationSuccess (Some proof (* current *), env) + ) else ( + debug_print + (lazy "\n================================================"); + debug_print (lazy (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current))); + + let t1 = Unix.gettimeofday () in + let new' = infer env sign current active in + let t2 = Unix.gettimeofday () in + infer_time := !infer_time +. (t2 -. t1); + + let res, goal' = contains_empty env new' in + if res then + let proof = + match goal' with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) + else + let t1 = Unix.gettimeofday () in + let new' = forward_simplify_new env new' active in + let t2 = Unix.gettimeofday () in + let _ = + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1) + in + let active = + match sign with + | Negative -> active + | Positive -> + let t1 = Unix.gettimeofday () in + let active, _, newa, _ = + backward_simplify env ([], [current]) active + in + let t2 = Unix.gettimeofday () in + backward_simpl_time := + !backward_simpl_time +. (t2 -. t1); + match newa with + | None -> active + | Some (n, p) -> + let al, tbl = active in + let nn = List.map (fun e -> Negative, e) n in + let pp, tbl = + List.fold_right + (fun e (l, t) -> + (Positive, e)::l, + Indexing.index tbl e) + p ([], tbl) in - let t2 = Unix.gettimeofday () in - backward_simpl_time := - !backward_simpl_time +. (t2 -. t1); - match newa with - | None -> active - | Some (n, p) -> - let al, tbl = active in - let nn = List.map (fun e -> Negative, e) n in - let pp, tbl = - List.fold_right - (fun e (l, t) -> - (Positive, e)::l, - Indexing.index tbl e) - p ([], tbl) - in - nn @ al @ pp, tbl - in + nn @ al @ pp, tbl + in (* let _ = *) (* Printf.printf "active:\n%s\n" *) (* (String.concat "\n" *) @@ -1476,17 +1695,17 @@ let rec given_clause env goals theorems passive active = (* (string_of_equality ~env e)) pos))); *) (* print_newline (); *) (* in *) - match contains_empty env new' with - | false, _ -> - let active = - let al, tbl = active in - match sign with - | Negative -> (sign, current)::al, tbl - | Positive -> - al @ [(sign, current)], Indexing.index tbl current - in - let passive = add_to_passive passive new' in - let (_, ns), (_, ps), _ = passive in + match contains_empty env new' with + | false, _ -> + let active = + let al, tbl = active in + match sign with + | Negative -> (sign, current)::al, tbl + | Positive -> + al @ [(sign, current)], Indexing.index tbl 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 " ^ *) @@ -1496,22 +1715,71 @@ let rec given_clause env goals theorems passive active = (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) - given_clause env goals theorems passive active - | true, goal -> - let proof = - match goal with - | Some goal -> - let _, proof, _, _, _ = goal in Some proof - | None -> None - in - ParamodulationSuccess (proof (* goal *), env) - ) - with SearchSpaceOver -> - ParamodulationFailure + given_clause dbd env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> + let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) + ) +(* with SearchSpaceOver -> *) +(* ParamodulationFailure *) ;; -let rec given_clause_fullred env goals theorems passive active = +let rec given_clause_fullred dbd env goals theorems passive active = + let goals = simplify_goals env goals ~passive active in + let ok, goals = activate_goal goals in +(* let theorems = simplify_theorems env theorems ~passive active in *) + if ok then + let _ = + let print_goals goals = + (String.concat "\n" + (List.map + (fun (d, gl) -> + let gl' = + List.map + (fun (p, _, t) -> + (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl + in + Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) + in + debug_print + (lazy + (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" + (print_goals (fst goals)) (print_goals (snd goals)))) + in + let ok, goals = apply_goal_to_theorems dbd env theorems active goals in + if ok then + let proof = + match (fst goals) with + | (_, [proof, _, _])::_ -> Some proof + | _ -> assert false + in + ParamodulationSuccess (proof, env) + else + given_clause_fullred_aux dbd env goals theorems passive active + else +(* let ok', theorems = activate_theorem theorems in *) +(* if ok' then *) +(* let ok, goals = apply_theorem_to_goals env theorems active goals in *) +(* if ok then *) +(* let proof = *) +(* match (fst goals) with *) +(* | (_, [proof, _, _])::_ -> Some proof *) +(* | _ -> assert false *) +(* in *) +(* ParamodulationSuccess (proof, env) *) +(* else *) +(* given_clause_fullred_aux env goals theorems passive active *) +(* else *) + if (passive_is_empty passive) then ParamodulationFailure + else given_clause_fullred_aux dbd env goals theorems passive active + +and given_clause_fullred_aux dbd env goals theorems passive active = let time1 = Unix.gettimeofday () in let selection_estimate = get_selection_estimate () in @@ -1538,133 +1806,126 @@ let rec given_clause_fullred env goals theorems passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); -(* let refl_equal = *) -(* CicUtil.term_of_uri *) -(* (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *) -(* in *) - let goals = simplify_goals env goals ~passive active in - let theorems = simplify_theorems env theorems ~passive active in - let is_passive_empty = passive_is_empty passive in - try - let ok, goals = apply_to_goals env is_passive_empty theorems active goals in - if ok then - let proof = - match goals with - | (_, [proof, _, _])::_ -> Some proof - | _ -> assert false - in - ParamodulationSuccess (proof, env) - else - let _ = - debug_print - (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); - debug_print - (lazy - (String.concat "\n" - (List.map - (fun (d, gl) -> - let gl' = - List.map - (fun (p, _, t) -> - (string_of_proof p) ^ ", " ^ (CicPp.ppterm t)) gl - in - Printf.sprintf "%d: %s" d (String.concat "; " gl')) - goals))); - in - match is_passive_empty (* passive_is_empty passive *) with - | true -> (* ParamodulationFailure *) - given_clause_fullred env goals theorems passive active - | false -> - let (sign, current), passive = select env goals passive active in - let time1 = Unix.gettimeofday () in - let res = forward_simplify env (sign, current) ~passive active in - let time2 = Unix.gettimeofday () in - forward_simpl_time := !forward_simpl_time +. (time2 -. time1); - match res with - | None -> - given_clause_fullred env goals theorems passive active - | Some (sign, current) -> - if (sign = Negative) && (is_identity env current) then ( - debug_print - (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current))); - let _, proof, _, _, _ = current in - ParamodulationSuccess (Some proof (* current *), env) - ) else ( - debug_print - (lazy "\n================================================"); - debug_print (lazy (Printf.sprintf "selected: %s %s" - (string_of_sign sign) - (string_of_equality ~env current))); - - let t1 = Unix.gettimeofday () in - let new' = infer env sign current active in - let t2 = Unix.gettimeofday () in - infer_time := !infer_time +. (t2 -. t1); - - let active = - if is_identity env current then active - else - let al, tbl = active in - match sign with - | Negative -> (sign, current)::al, tbl - | Positive -> - al @ [(sign, current)], Indexing.index tbl current - in - let rec simplify new' active passive = - let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' ~passive active in - let t2 = Unix.gettimeofday () in - forward_simpl_new_time := - !forward_simpl_new_time +. (t2 -. t1); - let t1 = Unix.gettimeofday () in - let active, passive, newa, retained = - backward_simplify env new' ~passive active in - let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); - match newa, retained with - | None, None -> active, passive, new' - | Some (n, p), None - | None, Some (n, p) -> - let nn, np = new' in - simplify (nn @ n, np @ p) active passive - | Some (n, p), Some (rn, rp) -> - let nn, np = new' in - simplify (nn @ n @ rn, np @ p @ rp) active passive - in - let active, passive, new' = simplify new' active passive in +(* try *) +(* let ok, goals = apply_to_goals env is_passive_empty theorems active goals in *) +(* if ok then *) +(* let proof = *) +(* match goals with *) +(* | (_, [proof, _, _])::_ -> Some proof *) +(* | _ -> assert false *) +(* in *) +(* ParamodulationSuccess (proof, env) *) +(* else *) +(* let _ = *) +(* debug_print *) +(* (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); *) +(* debug_print *) +(* (lazy *) +(* (String.concat "\n" *) +(* (List.map *) +(* (fun (d, gl) -> *) +(* let gl' = *) +(* List.map *) +(* (fun (p, _, t) -> *) +(* (\* (string_of_proof p) ^ ", " ^ *\) (CicPp.ppterm t)) gl *) +(* in *) +(* Printf.sprintf "%d: %s" d (String.concat "; " gl')) *) +(* goals))); *) +(* in *) + match passive_is_empty passive with + | true -> (* ParamodulationFailure *) + given_clause_fullred dbd env goals theorems passive active + | false -> + let (sign, current), passive = select env (fst goals) passive active in + let time1 = Unix.gettimeofday () in + let res = forward_simplify env (sign, current) ~passive active in + let time2 = Unix.gettimeofday () in + forward_simpl_time := !forward_simpl_time +. (time2 -. time1); + match res with + | None -> + given_clause_fullred dbd env goals theorems passive active + | Some (sign, current) -> + if (sign = Negative) && (is_identity env current) then ( + debug_print + (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) + (string_of_equality ~env current))); + let _, proof, _, _, _ = current in + ParamodulationSuccess (Some proof (* current *), env) + ) else ( + debug_print + (lazy "\n================================================"); + debug_print (lazy (Printf.sprintf "selected: %s %s" + (string_of_sign sign) + (string_of_equality ~env current))); + + let t1 = Unix.gettimeofday () in + let new' = infer env sign current active in + let t2 = Unix.gettimeofday () in + infer_time := !infer_time +. (t2 -. t1); + + let active = + if is_identity env current then active + else + let al, tbl = active in + match sign with + | Negative -> (sign, current)::al, tbl + | Positive -> + al @ [(sign, current)], Indexing.index tbl current + in + let rec simplify new' active passive = + let t1 = Unix.gettimeofday () in + let new' = forward_simplify_new env new' ~passive active in + let t2 = Unix.gettimeofday () in + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1); + let t1 = Unix.gettimeofday () in + let active, passive, newa, retained = + backward_simplify env new' ~passive active in + let t2 = Unix.gettimeofday () in + backward_simpl_time := !backward_simpl_time +. (t2 -. t1); + match newa, retained with + | None, None -> active, passive, new' + | Some (n, p), None + | None, Some (n, p) -> + let nn, np = new' in + simplify (nn @ n, np @ p) active passive + | Some (n, p), Some (rn, rp) -> + let nn, np = new' in + simplify (nn @ n @ rn, np @ p @ rp) active passive + in + let active, passive, new' = simplify new' active passive in - let k = size_of_passive passive in - if k < (kept - 1) then - processed_clauses := !processed_clauses + (kept - 1 - k); - - let _ = + let k = size_of_passive passive in + if k < (kept - 1) then + processed_clauses := !processed_clauses + (kept - 1 - k); + + let _ = + debug_print + (lazy + (Printf.sprintf "active:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + (fst active)))))) + in + let _ = + match new' with + | neg, pos -> debug_print (lazy - (Printf.sprintf "active:\n%s\n" + (Printf.sprintf "new':\n%s\n" (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) - (fst active)))))) - in - let _ = - match new' with - | neg, pos -> - debug_print - (lazy - (Printf.sprintf "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))))) - in - match contains_empty env new' with - | false, _ -> - let passive = add_to_passive passive new' in + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))))) + in + match contains_empty env new' with + | false, _ -> + let passive = add_to_passive passive new' in (* let (_, ns), (_, ps), _ = passive in *) (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) @@ -1675,23 +1936,23 @@ let rec given_clause_fullred env goals theorems passive active = (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) - given_clause_fullred env goals theorems passive active - | true, goal -> - let proof = - match goal with - | Some goal -> let _, proof, _, _, _ = goal in Some proof - | None -> None - in - ParamodulationSuccess (proof (* goal *), env) - ) - with SearchSpaceOver -> - ParamodulationFailure + given_clause_fullred dbd env goals theorems passive active + | true, goal -> + let proof = + match goal with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) + ) +(* with SearchSpaceOver -> *) +(* ParamodulationFailure *) ;; (* let given_clause_ref = ref given_clause;; *) -let main dbd term metasenv ugraph = +let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in @@ -1718,9 +1979,20 @@ let main dbd term metasenv ugraph = in (* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in - let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in - let context_hyp = find_context_hypotheses env eq_indexes in - let theorems = context_hyp @ theorems in + let theorems = + if full then + let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let context_hyp = find_context_hypotheses env eq_indexes in + context_hyp, theorems + else + let refl_equal = + let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") + in + let t = CicUtil.term_of_uri refl_equal in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + [], [(refl_equal, t, ty, [])] + in let _ = debug_print (lazy @@ -1728,10 +2000,10 @@ let main dbd term metasenv ugraph = "Theorems:\n-------------------------------------\n%s\n" (String.concat "\n" (List.map - (fun (t, ty, _) -> + (fun (_, t, ty, _) -> Printf.sprintf "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - theorems)))) + (snd theorems))))) in try let goal = Inference.BasicProof new_meta_goal, [], goal in @@ -1808,9 +2080,15 @@ let main dbd term metasenv ugraph = 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 [0, [goal]] theorems passive active *) +(* in *) let res = + let goals = make_goals goal in +(* and theorems = make_theorems theorems in *) (if !use_fullred then given_clause_fullred else given_clause) - env [0, [goal]] theorems passive active + dbd env goals theorems passive active in let finish = Unix.gettimeofday () in let _ = @@ -1831,12 +2109,12 @@ let main dbd term metasenv ugraph = (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities in let _ = - 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); +(* 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); *) try let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph @@ -1892,10 +2170,28 @@ let main dbd term metasenv ugraph = let default_depth = !maxdepth and default_width = !maxwidth;; +let reset_refs () = + maxmeta := 0; + symbols_counter := 0; + weight_age_counter := !weight_age_ratio; + processed_clauses := 0; + start_time := 0.; + elapsed_time := 0.; + maximal_retained_equality := None; + infer_time := 0.; + forward_simpl_time := 0.; + forward_simpl_new_time := 0.; + backward_simpl_time := 0.; + passive_maintainance_time := 0.; + derived_clauses := 0; + kept_clauses := 0; +;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in - maxmeta := 0; + reset_refs (); + Indexing.init_index (); maxdepth := depth; maxwidth := width; let proof, goal = status in @@ -1965,9 +2261,26 @@ let saturate in let theorems = if full then - let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in +(* let refl_eq = *) +(* let u = eq_XURI () in *) +(* let t = CicUtil.term_of_uri u in *) +(* let ty, _ = *) +(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *) +(* (t, ty, []) *) +(* in *) +(* let le_S = *) +(* let u = UriManager.uri_of_string *) +(* "cic:/matita/nat/orders/le.ind#xpointer(1/1/2)" in *) +(* let t = CicUtil.term_of_uri u in *) +(* let ty, _ = *) +(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *) +(* (t, ty, []) *) +(* in *) +(* let thms = refl_eq::le_S::[] in *) + let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in let context_hyp = find_context_hypotheses env eq_indexes in - context_hyp @ thms +(* context_hyp @ thms *) + (context_hyp, thms) else let refl_equal = let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in @@ -1975,7 +2288,7 @@ let saturate in let t = CicUtil.term_of_uri refl_equal in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - [(t, ty, [])] + [], [(refl_equal, t, ty, [])] in let _ = debug_print @@ -1984,16 +2297,21 @@ let saturate "Theorems:\n-------------------------------------\n%s\n" (String.concat "\n" (List.map - (fun (t, ty, _) -> + (fun (_, t, ty, _) -> Printf.sprintf "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - theorems)))) + (snd theorems))))) 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 [0, [goal]] theorems passive active in +(* let res = given_clause_fullred env [0, [goal]] theorems passive active in *) + let res = + let goals = make_goals goal in +(* and theorems = make_theorems theorems in *) + given_clause_fullred dbd env goals theorems passive active + in let finish = Unix.gettimeofday () in (res, finish -. start) in