X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=825d6b8c8b6a586225a349bb52ba5bef20505bb5;hb=e9a76af2c3c2a70f26b0315225b596bcba1a585d;hp=c933aec0b48c3c11115d8d8346302f1144c93892;hpb=e61d023695578ebf09d487480e6e7cac3a2dd2ee;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index c933aec0b..825d6b8c8 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -2,6 +2,10 @@ open Inference;; open Utils;; +(* set to false to disable paramodulation inside auto_tac *) +let connect_to_auto = true;; + + (* profiling statistics... *) let infer_time = ref 0.;; let forward_simpl_time = ref 0.;; @@ -18,12 +22,15 @@ let elapsed_time = ref 0.;; let maximal_retained_equality = ref None;; (* equality-selection related globals *) -let use_fullred = ref false;; -let weight_age_ratio = ref 0;; (* settable by the user from the command line *) +let use_fullred = ref true;; +let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *) let weight_age_counter = ref !weight_age_ratio;; -let symbols_ratio = ref 0;; +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;; @@ -31,12 +38,20 @@ let kept_clauses = ref 0;; (* index of the greatest Cic.Meta created - TODO: find a better way! *) let maxmeta = ref 0;; +(* varbiables controlling the search-space *) +let maxdepth = ref 3;; +let maxwidth = ref 3;; + type result = - | Failure - | Success of Inference.equality option * environment + | ParamodulationFailure + | 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), _, _) = @@ -83,7 +98,7 @@ module OrderedEquality = struct try let res = Pervasives.compare (List.hd a) (List.hd a') in if res <> 0 then res else Pervasives.compare eq1 eq2 - with _ -> Pervasives.compare eq1 eq2 + with Failure "hd" -> Pervasives.compare eq1 eq2 (* match a, a' with *) (* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *) (* let res = Pervasives.compare i j in *) @@ -96,8 +111,12 @@ end module EqualitySet = Set.Make(OrderedEquality);; -let select env passive (active, _) = +let select env goals passive (active, _) = processed_clauses := !processed_clauses + 1; + + let goal = + match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false + in let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = @@ -128,9 +147,13 @@ let select env passive (active, _) = 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 +(* match active with *) +(* | (Negative, e)::_ -> *) +(* let symbols = symbols_of_equality e in *) + let symbols = + let _, _, term = goal in + symbols_of_term term + in let card = cardinality symbols in let foldfun k v (r1, r2) = if TermMap.mem k symbols then @@ -172,19 +195,19 @@ let select env passive (active, _) = (([], neg_set), (remove current pos_list, EqualitySet.remove current pos_set), passive_table) - | _ -> - let current = EqualitySet.min_elt pos_set in - let passive_table = - Indexing.remove_index passive_table current -(* if !use_fullred then Indexing.remove_index passive_table current *) -(* else passive_table *) - in - let passive = - (neg_list, neg_set), - (remove current pos_list, EqualitySet.remove current pos_set), - passive_table - in - (Positive, current), passive +(* | _ -> *) +(* let current = EqualitySet.min_elt pos_set in *) +(* let passive_table = *) +(* Indexing.remove_index passive_table current *) +(* (\* if !use_fullred then Indexing.remove_index passive_table current *\) *) +(* (\* else passive_table *\) *) +(* in *) +(* let passive = *) +(* (neg_list, neg_set), *) +(* (remove current pos_list, EqualitySet.remove current pos_set), *) +(* passive_table *) +(* in *) +(* (Positive, current), passive *) ) | _ -> symbols_counter := !symbols_ratio; @@ -275,9 +298,14 @@ 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 - Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age; + 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 + (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); let symbols, card = match active with | (Negative, e)::_ -> @@ -358,7 +386,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 ()) @@ -376,7 +404,10 @@ let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with | Negative -> - Indexing.superposition_left env active_table current, [] + let maxm, res = + Indexing.superposition_left !maxmeta env active_table current in + maxmeta := maxm; + res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in @@ -384,7 +415,9 @@ let infer env sign current (active_list, active_table) = let rec infer_positive table = function | [] -> [], [] | (Negative, equality)::tl -> - let res = Indexing.superposition_left env table equality in + let maxm, res = + Indexing.superposition_left !maxmeta env table equality in + maxmeta := maxm; let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> @@ -400,11 +433,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 ;; @@ -435,7 +509,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 *) @@ -455,7 +529,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = let demodulate table current = let newmeta, newcurrent = - Indexing.demodulation !maxmeta env table current in + Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) @@ -542,8 +616,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); - let demodulate table target = - let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in + let demodulate sign table target = + let newmeta, newtarget = + Indexing.demodulation_equality !maxmeta env table sign target in maxmeta := newmeta; newtarget in @@ -555,13 +630,13 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in let new_neg, new_pos = - let new_neg = List.map (demodulate active_table) new_neg - and new_pos = List.map (demodulate active_table) new_pos in + let new_neg = List.map (demodulate Negative active_table) new_neg + and new_pos = List.map (demodulate Positive active_table) new_pos in match passive_table with | None -> new_neg, new_pos | Some passive_table -> - List.map (demodulate passive_table) new_neg, - List.map (demodulate passive_table) new_pos + List.map (demodulate Negative passive_table) new_neg, + List.map (demodulate Positive passive_table) new_pos in let t2 = Unix.gettimeofday () in @@ -581,10 +656,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let subs = match passive_table with | None -> - (fun e -> not (Indexing.subsumption env active_table e)) + (fun e -> not (fst (Indexing.subsumption env active_table e))) | Some passive_table -> - (fun e -> not ((Indexing.subsumption env active_table e) || - (Indexing.subsumption env passive_table e))) + (fun e -> not ((fst (Indexing.subsumption env active_table e)) || + (fst (Indexing.subsumption env passive_table e)))) in let t1 = Unix.gettimeofday () in @@ -623,18 +698,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 = @@ -667,17 +746,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 (lazy (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 @@ -692,18 +776,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 ;; @@ -716,8 +803,766 @@ 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 rec given_clause env passive active = +let simplify_goal env goal ?passive (active_list, active_table) = + let pl, passive_table = + match passive with + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + pn @ pp, Some pt + in + let all = if pl = [] then active_list else active_list @ pl in + + let demodulate table goal = + let newmeta, newgoal = + Indexing.demodulation_goal !maxmeta env table goal in + maxmeta := newmeta; + goal != newgoal, newgoal + in + let changed, goal = + match passive_table with + | None -> demodulate active_table goal + | Some passive_table -> + 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 *) + changed, goal +;; + + +let simplify_goals env goals ?passive active = + 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 +;; + + +let simplify_theorems env theorems ?passive (active_list, active_table) = + let pl, passive_table = + match passive with + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + 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; + 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 -> + 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 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 *) +;; + + +let apply_equality_to_goal env equality goal = + let module C = Cic in + let module HL = HelmLibraryObjects in + let module I = Inference in + let metasenv, context, ugraph = env in + let _, proof, (ty, left, right, _), metas, args = equality in + let eqterm = + C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in + let gproof, gmetas, gterm = goal in + try + let subst, metasenv', _ = + let menv = metasenv @ metas @ gmetas in + Inference.unification menv context eqterm gterm ugraph + in + let newproof = + match proof with + | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t) + | I.ProofBlock (s, uri, nt, t, pe, p) -> + I.ProofBlock (subst @ s, uri, nt, t, pe, p) + | _ -> assert false + in + let newgproof = + let rec repl = function + | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp) + | I.NoProof -> newproof + | I.BasicProof p -> newproof + | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p) + | _ -> assert false + in + repl gproof + in + true, subst, newgproof + with CicUnification.UnificationFailure _ -> + false, [], I.NoProof +;; + + +(* +let apply_to_goal env theorems active (depth, goals) = + let _ = + debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals))) + in + let metasenv, context, ugraph = env in + let goal = List.hd goals in + let proof, metas, term = goal in +(* debug_print *) +(* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *) + let newmeta = CicMkImplicit.new_meta metasenv [] in + let metasenv = (newmeta, context, term)::metasenv @ metas in + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let status = + ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) + in + let rec aux = function + | [] -> false, [] (* goals *) (* None *) + | (theorem, thmty, _)::tl -> + try + let subst_in, (newproof, newgoals) = + PrimitiveTactics.apply_tac_verbose ~term:theorem status + in + if newgoals = [] then + let _, _, p, _ = newproof in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof p, gp) + | Inference.NoProof -> Inference.BasicProof p + | Inference.BasicProof _ -> Inference.BasicProof p + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + true, [[newp, metas, term]] (* Some newp *) + else if List.length newgoals = 1 then + let _, menv, p, _ = newproof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let goals = + List.map + (fun i -> + let _, _, ty = CicUtil.lookup_meta i menv in + let proof = + Inference.SubProof + (p, i, Inference.BasicProof (Cic.Meta (i, irl))) + in (proof, menv, ty)) + newgoals + in + let res, others = aux tl in + if res then (true, others) else (false, goals::others) + else + aux tl + with ProofEngineTypes.Fail msg -> + (* debug_print ("FAIL!!:" ^ msg); *) + aux tl + in + let r, l = + if Inference.term_is_equality term then + let rec appleq = function + | [] -> false, [] + | (Positive, equality)::tl -> + let ok, _, newproof = apply_equality_to_goal env equality goal in + if ok then true, [(depth, [newproof, metas, term])] else appleq tl + | _::tl -> appleq tl + in + let al, _ = active in + appleq al + else + false, [] + in + if r = true then r, l else + let r, l = aux theorems in + if r = true then + r, List.map (fun l -> (depth+1, l)) l + else + r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l) +;; +*) + + +let new_meta () = + incr maxmeta; !maxmeta +;; + + +let apply_to_goal env theorems active goal = + let metasenv, context, ugraph = env in + let proof, metas, term = goal in + debug_print + (lazy + (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 + let proof', newmeta = + let rec get_meta = function + | SubProof (t, i, _) -> t, i + | ProofGoalBlock (_, p) -> get_meta p + | _ -> + let n = new_meta () in (* CicMkImplicit.new_meta metasenv [] in *) + Cic.Meta (n, irl), n + in + get_meta proof + in +(* let newmeta = CicMkImplicit.new_meta metasenv [] in *) + let metasenv = (newmeta, context, term)::metasenv @ metas in + ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) +(* ((None, metasenv, proof', term), newmeta) *) + in + let rec aux = function + | [] -> `No (* , [], [] *) + | (theorem, thmty, _)::tl -> + try + let subst, (newproof, newgoals) = + PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status + in + if newgoals = [] then + let _, _, p, _ = newproof in + let newp = + let rec repl = function + | Inference.ProofGoalBlock (_, gp) -> + Inference.ProofGoalBlock (Inference.BasicProof p, gp) + | Inference.NoProof -> Inference.BasicProof p + | Inference.BasicProof _ -> Inference.BasicProof p + | Inference.SubProof (t, i, p2) -> + Inference.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + let _, m = status in + let subst = List.filter (fun (i, _) -> i = m) subst in +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "m = %d\nsubst = %s\n" *) +(* m (print_subst subst))); *) + `Ok (subst, [newp, metas, term]) + else + let _, menv, p, _ = newproof in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let goals = + List.map + (fun i -> + let _, _, ty = CicUtil.lookup_meta i menv in + let p' = + let rec gp = function + | SubProof (t, i, p) -> + SubProof (t, i, gp p) + | ProofGoalBlock (sp1, sp2) -> +(* SubProof (p, i, sp) *) + ProofGoalBlock (sp1, gp sp2) +(* gp sp *) + | BasicProof _ + | NoProof -> + SubProof (p, i, BasicProof (Cic.Meta (i, irl))) + | ProofSymBlock (s, sp) -> + ProofSymBlock (s, gp sp) + | ProofBlock (s, u, nt, t, pe, sp) -> + ProofBlock (s, u, nt, t, pe, gp sp) +(* | _ -> assert false *) + in gp proof + in + debug_print + (lazy + (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))); *) + let best = aux tl in + match best with + | `Ok (_, _) -> best + | `No -> `GoOn ([subst, goals]) + | `GoOn sl(* , subst', goals' *) -> +(* if (List.length goals') < (List.length goals) then best *) +(* else `GoOn, subst, goals *) + `GoOn ((subst, goals)::sl) + with ProofEngineTypes.Fail msg -> + aux tl + in + let r, s, l = + if Inference.term_is_equality term then + let rec appleq = function + | [] -> false, [], [] + | (Positive, equality)::tl -> + let ok, s, newproof = apply_equality_to_goal env equality goal in + if ok then true, s, [newproof, metas, term] else appleq tl + | _::tl -> appleq tl + in + let al, _ = active in + appleq al + else + false, [], [] + in + if r = true then `Ok (s, l) else aux theorems +;; + + +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))); *) + let rec repl = function + | NoProof -> NoProof + | BasicProof t -> + BasicProof (CicMetaSubst.apply_subst subst t) + | ProofGoalBlock (p, pb) -> +(* 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'))); *) + let p = repl p in + SubProof (t', i, p) + | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) + | ProofBlock (s, u, nty, t, pe, p) -> + ProofBlock (subst @ s, u, nty, t, pe, p) + in (repl proof, metas, term) + in + let r = apply_to_goal env theorems active goal in ( + match r with + | `No -> `No (depth, goals) + | `GoOn sl (* (subst, gl) *) -> +(* let tl = List.map (propagate_subst subst) tl in *) +(* 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)))); *) + `GoOn l (* (depth+1, gl @ tl) *) + | `Ok (subst, gl) -> + if tl = [] then +(* let _ = *) +(* let p, _, t = List.hd gl in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "OK: %s, %s\n" *) +(* (string_of_proof p) (CicPp.ppterm t))) *) +(* in *) + `Ok (depth, gl) + else + let p, _, _ = List.hd gl in + let subproof = + let rec repl = function + | SubProof (_, _, p) -> repl p + | ProofGoalBlock (p1, p2) -> + ProofGoalBlock (repl p1, repl p2) + | p -> p + in + build_proof_term (repl p) + in + let i = + let rec get_meta = function + | SubProof (_, i, p) -> max i (get_meta p) + | ProofGoalBlock (_, p) -> get_meta p + | _ -> -1 (* assert false *) + in + get_meta p + in + let subst = + let _, (context, _, _) = List.hd subst in + [i, (context, subproof, Cic.Implicit None)] + in + let tl = List.map (propagate_subst subst) tl in + `GoOn ([depth+1, tl]) + ) + | _ -> assert false + in + debug_print + (lazy + (Printf.sprintf "apply_to_goal_conj (%d, [%s])" + depth + (String.concat "; " + (List.map (fun (_, _, t) -> CicPp.ppterm t) goals)))); + if depth > !maxdepth || (List.length goals) > !maxwidth then ( + debug_print + (lazy (Printf.sprintf "Pruning because depth = %d, width = %d" + depth (List.length goals))); + `No (depth, goals) + ) else + aux goals +;; + + +module OrderedGoals = struct + type t = int * (Inference.proof * Cic.metasenv * Cic.term) list + + let compare g1 g2 = + let d1, l1 = g1 + and d2, l2 = g2 in + 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 +(* let res = Pervasives.compare g1 g2 in *) +(* let _ = *) +(* let print_goals (d, gl) = *) +(* let gl' = List.map (fun (_, _, t) -> CicPp.ppterm t) gl in *) +(* Printf.sprintf "%d, [%s]" d (String.concat "; " gl') *) +(* in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "comparing g1:%s and g2:%s, res: %d\n" *) +(* (print_goals g1) (print_goals g2) res)) *) +(* in *) +(* res *) +end + +module GoalsSet = Set.Make(OrderedGoals);; + + +exception SearchSpaceOver;; + + +let apply_to_goals env is_passive_empty theorems active goals = + debug_print (lazy "\n\n\tapply_to_goals\n\n"); + let add_to set goals = + List.fold_left (fun s g -> GoalsSet.add g s) set goals + in + let rec aux set = function + | [] -> + debug_print (lazy "HERE!!!"); + if is_passive_empty then raise SearchSpaceOver else false, set + | goals::tl -> + let res = apply_to_goal_conj env theorems active goals in + match res with + | `Ok newgoals -> + let _ = + let d, p, t = + match newgoals with + | (d, (p, _, t)::_) -> d, p, t + | _ -> assert false + in + debug_print + (lazy + (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n" + d (string_of_proof p) (CicPp.ppterm t))) + 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 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 +(* print_set set "SET AFTER"; *) +(* let m = GoalsSet.cardinal set in *) +(* if n < m then *) + false, set' +(* else *) +(* let _ = print_set set "SET didn't change" in *) +(* aux set tl *) + | `No newgoals -> + aux set tl +(* let set = add_to set (newgoals::goals::tl) in *) +(* let res, set = aux set tl in *) +(* res, set *) + in + let n = List.length goals in + let res, goals = aux (add_to GoalsSet.empty goals) goals in + let goals = GoalsSet.elements goals in + debug_print (lazy "\n\tapply_to_goals end\n"); + let m = List.length goals in + if m = n && is_passive_empty then + raise SearchSpaceOver + else + res, goals +;; + + +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 @@ -726,12 +1571,14 @@ let rec given_clause env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print + (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate)); prune_passive selection_estimate active passive ) else passive @@ -742,43 +1589,65 @@ let rec given_clause env passive active = kept_clauses := (size_of_passive passive) + (size_of_active 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 -> Failure + | true -> (* ParamodulationFailure *) + given_clause dbd env goals theorems passive active | false -> - let (sign, current), passive = select env passive active in + 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 env passive active + given_clause dbd env goals theorems passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - Success (Some current, env) + 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 ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + 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 + let res, goal' = contains_empty env new' in if res then - Success (goal, env) + 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' (* ~passive *) active 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) + forward_simpl_new_time := + !forward_simpl_new_time +. (t2 -. t1) in let active = match sign with @@ -789,7 +1658,8 @@ let rec given_clause env passive active = backward_simplify env ([], [current]) active in let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); + backward_simpl_time := + !backward_simpl_time +. (t2 -. t1); match newa with | None -> active | Some (n, p) -> @@ -835,7 +1705,7 @@ let rec given_clause env passive active = al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in -(* let (_, ns), (_, ps), _ = passive in *) + let (_, ns), (_, ps), _ = passive in (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) @@ -845,14 +1715,71 @@ let rec given_clause env passive active = (* (string_of_equality ~env e)) *) (* (EqualitySet.elements ps)))); *) (* print_newline (); *) - given_clause env passive active + given_clause dbd env goals theorems passive active | true, goal -> - Success (goal, env) + 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 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 @@ -861,12 +1788,14 @@ let rec given_clause_fullred env passive active = if !time_limit = 0. || !processed_clauses = 0 then passive else if !elapsed_time > !time_limit then ( - Printf.printf "Time limit (%.2f) reached: %.2f\n" - !time_limit !elapsed_time; + debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n" + !time_limit !elapsed_time)); make_passive [] [] ) else if kept > selection_estimate then ( - Printf.printf ("Too many passive equalities: pruning... (kept: %d, " ^^ - "selection_estimate: %d)\n") kept selection_estimate; + debug_print + (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^ + "(kept: %d, selection_estimate: %d)\n") + kept selection_estimate)); prune_passive selection_estimate active passive ) else passive @@ -877,28 +1806,57 @@ let rec given_clause_fullred env passive active = kept_clauses := (size_of_passive passive) + (size_of_active active); +(* 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 -> Failure + | true -> (* ParamodulationFailure *) + given_clause_fullred dbd env goals theorems passive active | false -> - let (sign, current), passive = select env passive active in + 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 env passive active + given_clause_fullred dbd env goals theorems passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( - Printf.printf "OK!!! %s %s" (string_of_sign sign) - (string_of_equality ~env current); - print_newline (); - Success (Some current, env) + 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 ( - print_endline "\n================================================"; - Printf.printf "selected: %s %s" - (string_of_sign sign) (string_of_equality ~env current); - print_newline (); + 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 @@ -911,13 +1869,15 @@ let rec given_clause_fullred env passive active = let al, tbl = active in match sign with | Negative -> (sign, current)::al, tbl - | Positive -> al @ [(sign, current)], Indexing.index tbl current + | 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); + 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 @@ -939,156 +1899,488 @@ let rec given_clause_fullred env passive active = if k < (kept - 1) then processed_clauses := !processed_clauses + (kept - 1 - k); -(* let _ = *) -(* Printf.printf "active:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *) -(* (string_of_equality ~env e)) (fst 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 *) + 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 "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 - given_clause_fullred env passive active +(* 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_fullred dbd env goals theorems passive active | true, goal -> - Success (goal, env) + let proof = + match goal with + | Some goal -> let _, proof, _, _, _ = goal in Some proof + | None -> None + in + ParamodulationSuccess (proof (* goal *), env) ) +(* with SearchSpaceOver -> *) +(* ParamodulationFailure *) ;; -let get_from_user () = - let dbd = Mysql.quick_connect - ~host:"localhost" ~user:"helm" ~database:"mowgli" () in - let rec get () = - match read_line () with - | "" -> [] - | t -> t::(get ()) - in - let term_string = String.concat "\n" (get ()) in - let env, metasenv, term, ugraph = - List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0 - in - term, metasenv, ugraph -;; - +(* let given_clause_ref = ref given_clause;; *) -let given_clause_ref = ref given_clause;; - - -let main () = +let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in let module PET = ProofEngineTypes in let module PP = CicPp in - let term, metasenv, ugraph = get_from_user () in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in - let proof, goals = - PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in - let goal = List.nth goals 0 in + let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let proof, goals = status in + let goal' = List.nth goals 0 in let _, metasenv, meta_proof, _ = proof in - let _, context, goal = CicUtil.lookup_meta goal metasenv in - let equalities, maxm = find_equalities context proof in - maxmeta := maxm; (* TODO ugly!! *) + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, equalities, maxm = find_equalities context proof in + let lib_eq_uris, 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 = + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); + print_newline (); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in +(* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) 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 + (Printf.sprintf + "Theorems:\n-------------------------------------\n%s\n" + (String.concat "\n" + (List.map + (fun (_, t, ty, _) -> + Printf.sprintf + "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) + (snd theorems))))) + in try - let term_equality = equality_of_term meta_proof 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 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 - | Failure -> - Printf.printf "NO proof found! :-(\n\n" - | Success (Some goal, env) -> - Printf.printf "OK, found a proof!\n"; - let proof = Inference.build_term_proof goal in - print_endline (PP.pp proof (names_of_context context)); - print_endline (string_of_float (finish -. start)); - | Success (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; + let goal = Inference.BasicProof new_meta_goal, [], goal in +(* let term_equality = equality_of_term new_meta_goal goal in *) +(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *) +(* 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 + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "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 + (lazy + (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" + (let _, _, g = goal in CicPp.ppterm g); +(* (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 [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) + dbd env goals theorems passive active + in + let finish = Unix.gettimeofday () in + let _ = + match res with + | ParamodulationFailure -> + Printf.printf "NO proof found! :-(\n\n" + | ParamodulationSuccess (Some proof (* goal *), env) -> +(* let proof = Inference.build_proof_term goal in *) + let proof = Inference.build_proof_term proof 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); + let newmetasenv = + List.fold_left + (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); *) + 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 ;; -let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; +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 _ = - 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 - and set_fullred () = use_fullred := true - and set_time_limit v = time_limit := float_of_int v +let saturate + dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = + let module C = Cic in + reset_refs (); + Indexing.init_index (); + maxdepth := depth; + maxwidth := width; + let proof, goal = status in + let goal' = goal in + let uri, metasenv, meta_proof, term_to_prove = proof in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in + let eq_indexes, equalities, maxm = find_equalities context proof in + let new_meta_goal, metasenv, type_of_goal = + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + debug_print + (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty))); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty in - Arg.parse [ - "-f", Arg.Unit set_fullred, "Use full-reduction strategy"; - - "-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)"; + let ugraph = CicUniv.empty_ugraph in + let env = (metasenv, context, ugraph) in + let goal = Inference.BasicProof new_meta_goal, [], goal in + let res, time = + let lib_eq_uris, 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 + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "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 + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); + res + in + let theorems = + if full then +(* 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) + 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 + (Printf.sprintf + "Theorems:\n-------------------------------------\n%s\n" + (String.concat "\n" + (List.map + (fun (_, t, ty, _) -> + Printf.sprintf + "Term: %s, type: %s" + (CicPp.ppterm t) (CicPp.ppterm ty)) + (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 = + 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 + match res with + | ParamodulationSuccess (Some proof (* goal *), env) -> + debug_print (lazy "OK, found a proof!"); +(* let proof = Inference.build_proof_term goal in *) + let proof = Inference.build_proof_term proof in + let names = names_of_context context in + let newmetasenv = + let i1 = + match new_meta_goal with + | C.Meta (i, _) -> i | _ -> 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 (lazy (CicPp.pp proof [](* names *))); + debug_print + (lazy + (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 + (lazy + (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 (lazy "THE PROOF DOESN'T TYPECHECK!!!"); + debug_print (lazy (CicPp.pp proof names)); + raise (ProofEngineTypes.Fail + "Found a proof, but it doesn't typecheck") + in + debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); + newstatus + | _ -> + raise (ProofEngineTypes.Fail "NO proof found") +;; - "-c", Arg.String set_conf, "Configuration file (for the db connection)"; +(* dummy function called within matita to trigger linkage *) +let init () = ();; - "-lpo", Arg.Unit set_lpo, "Use lpo term ordering"; - "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)"; +(* UGLY SIDE EFFECT... *) +if connect_to_auto then ( + AutoTactic.paramodulation_tactic := saturate; + AutoTactic.term_is_equality := Inference.term_is_equality; +);; - "-l", Arg.Int set_time_limit, "Time limit (in seconds)"; - ] (fun a -> ()) "Usage:" -in -Helm_registry.load_from !configuration_file; -main ()