X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=07c6c601291ce9660e7d86ee5a9f9ec63b52399b;hb=b1ec882fae6023000ff6076e0a45f9809a6210e4;hp=bf9f8ba57dde43b7bcbbdf6b9fa0cb73a2940fc6;hpb=fd65a0a393bfb43d88ff936f40f045511e900e26;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index bf9f8ba57..07c6c6012 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -28,26 +28,10 @@ open Inference;; open Utils;; +let check_table t l = + List.fold_left + (fun b (_,eq) -> b && (Indexing.in_index t eq)) true l -(* -for debugging -let check_equation env equation msg = - let w, proof, (eq_ty, left, right, order), metas = equation in - let metasenv, context, ugraph = env in - let metasenv' = metasenv @ metas in - try - CicTypeChecker.type_of_aux' metasenv' context left ugraph; - CicTypeChecker.type_of_aux' metasenv' context right ugraph; - () - with - CicUtil.Meta_not_found _ as exn -> - begin - prerr_endline msg; - prerr_endline (CicPp.ppterm left); - prerr_endline (CicPp.ppterm right); - raise exn - end -*) (* set to false to disable paramodulation inside auto_tac *) let connect_to_auto = true;; @@ -91,6 +75,15 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; +let test eq = false +(* + let (_,(_,_,(ty,left,right,_),m1)) = eq in + let actual = + (Inference.metas_of_term left)@(Inference.metas_of_term right) + in + let m = List.filter (fun (i, _, _) -> List.mem i actual) m1 in + m <> m1 +;; *) type result = | ParamodulationFailure @@ -128,7 +121,7 @@ module OrderedEquality = struct and w2, _, (ty', left', right', _), m2 = eq2 in match Pervasives.compare w1 w2 with | 0 -> - let res = (List.length m1) - (List.length m2) in + let res = (List.length m1) - (List.length m2) in if res <> 0 then res else Pervasives.compare eq1 eq2 | res -> res end @@ -140,30 +133,30 @@ module OrderedEquality = struct let minor eq = let w, _, (ty, left, right, o), _ = eq in match o with - | Lt -> Some left - | Le -> assert false - | Gt -> Some right - | Ge -> assert false - | Eq - | Incomparable -> None - + | Lt -> Some left + | Le -> assert false + | Gt -> Some right + | Ge -> assert false + | Eq + | Incomparable -> None + let compare eq1 eq2 = let w1, _, (ty, left, right, o1), m1 = eq1 and w2, _, (ty', left', right', o2), m2 = eq2 in match Pervasives.compare w1 w2 with | 0 -> - (match minor eq1, minor eq2 with - | Some t1, Some t2 -> - fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2) - | Some _, None -> -1 - | None, Some _ -> 1 - | _,_ -> - (List.length m2) - (List.length m1) ) - | res -> res + (match minor eq1, minor eq2 with + | Some t1, Some t2 -> + fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2) + | Some _, None -> -1 + | None, Some _ -> 1 + | _,_ -> + (List.length m2) - (List.length m1) ) + | res -> res let compare eq1 eq2 = match compare eq1 eq2 with - 0 -> Pervasives.compare eq1 eq2 + 0 -> Pervasives.compare eq1 eq2 | res -> res end *) @@ -194,15 +187,15 @@ let min_elt weight l = (match l with [] -> raise Empty_list | a::tl -> - let wa = float_of_int (weight a) in - let x = ref 0. in - List.fold_left - (fun (current,w) arg -> - x:=!x +. 1.; + let wa = float_of_int (weight a) in + let x = ref 0. in + List.fold_left + (fun (current,w) arg -> + x:=!x +. 1.; let w1 = weight arg in let wa = (float_of_int w1) +. !x *. age_factor in - if wa < w then (arg,wa) else (current,w)) - (a,wa) tl) + if wa < w then (arg,wa) else (current,w)) + (a,wa) tl) ;; (* @@ -239,9 +232,8 @@ let rec select env goals passive (active, _) = (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], (hd:EqualitySet.elt)::tl -> - let w,_,_,_ = hd in let passive_table = - Indexing.remove_index passive_table hd + Indexing.remove_index passive_table hd in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) | _, _ -> assert false @@ -338,8 +330,8 @@ let add_to_passive passive (new_neg, new_pos) = let ok set equality = not (EqualitySet.mem equality set) in let neg = List.filter (ok neg_set) new_neg and pos = List.filter (ok pos_set) new_pos in - let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) table pos + let table = + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities @@ -462,18 +454,18 @@ let infer env sign current (active_list, active_table) = let maxm, res = Indexing.superposition_left !maxmeta env active_table current in if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup-1") res); + ignore(List.map + (function current -> + Indexing.check_target c current "sup-1") res); maxmeta := maxm; res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup0") res); + ignore(List.map + (function current -> + Indexing.check_target c current "sup0") res); maxmeta := maxm; let rec infer_positive table = function | [] -> [], [] @@ -481,21 +473,21 @@ let infer env sign current (active_list, active_table) = let maxm, res = Indexing.superposition_left !maxmeta env table equality in maxmeta := maxm; - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "supl") res); + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "supl") res); let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> let maxm, res = Indexing.superposition_right !maxmeta env table equality in maxmeta := maxm; - if Utils.debug_metas then - ignore - (List.map - (function current -> - Indexing.check_target c current "sup2") res); + if Utils.debug_metas then + ignore + (List.map + (function current -> + Indexing.check_target c current "sup2") res); let neg, pos = infer_positive table tl in neg, res @ pos in @@ -503,12 +495,12 @@ let infer env sign current (active_list, active_table) = maxmeta := maxm; let curr_table = Indexing.index Indexing.empty current in let neg, pos = - infer_positive curr_table ((sign,copy_of_current)::active_list) - in - if Utils.debug_metas then - ignore(List.map - (function current -> - Indexing.check_target c current "sup3") pos); + infer_positive curr_table ((sign,copy_of_current)::active_list) + in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup3") pos); neg, res @ pos in derived_clauses := !derived_clauses + (List.length new_neg) + @@ -516,12 +508,12 @@ let infer env sign current (active_list, active_table) = match !maximal_retained_equality with | None -> if Utils.debug_metas then - (ignore(List.map - (function current -> - Indexing.check_target c current "sup4") new_pos); - ignore(List.map - (function current -> - Indexing.check_target c current "sup5") new_neg)); + (ignore(List.map + (function current -> + Indexing.check_target c current "sup4") new_pos); + ignore(List.map + (function current -> + Indexing.check_target c current "sup5") new_neg)); new_neg, new_pos | Some eq -> ignore(assert false); @@ -568,7 +560,7 @@ let infer env sign current (active_list, active_table) = in List.filter filterfun new_pos in - new_neg, new_pos + new_neg, new_pos ;; @@ -607,35 +599,42 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) else ( -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) -(* (string_of_equality current) *) -(* (string_of_equality newcurrent))); *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "active is: %s" *) -(* (String.concat "\n" *) -(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) - None +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) +(* (string_of_equality current) *) +(* (string_of_equality newcurrent))); *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "active is: %s" *) +(* (String.concat "\n" *) +(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *) + None ) else Some (sign, newcurrent) in - let res = + let rec demod current = if Utils.debug_metas then ignore (Indexing.check_target context current "demod0"); let res = demodulate active_table current in if Utils.debug_metas then - ignore ((function None -> () | Some (_,x) -> - Indexing.check_target context x "demod1";()) res); + ignore ((function None -> () | Some (_,x) -> + ignore (Indexing.check_target context x "demod1");()) res); match res with | None -> None | Some (sign, newcurrent) -> match passive_table with | None -> res - | Some passive_table -> demodulate passive_table newcurrent - in + | Some passive_table -> + match demodulate passive_table newcurrent with + | None -> None + | Some (sign,newnewcurrent) -> + if newcurrent <> newnewcurrent then + demod newnewcurrent + else Some (sign,newnewcurrent) + in + let res = demod current in match res with | None -> None | Some (Negative, c) -> @@ -651,17 +650,17 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = else match passive_table with | None -> - if fst (Indexing.subsumption env active_table c) then - None - else - res + if fst (Indexing.subsumption env active_table c) then + None + else + res | Some passive_table -> if Indexing.in_index passive_table c then None else - let r1, _ = Indexing.subsumption env active_table c in - if r1 then None else - let r2, _ = Indexing.subsumption env passive_table c in - if r2 then None else res + let r1, _ = Indexing.subsumption env active_table c in + if r1 then None else + let r2, _ = Indexing.subsumption env passive_table c in + if r2 then None else res ;; type fs_time_info_t = { @@ -678,11 +677,11 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = if Utils.debug_metas then begin let m,c,u = env in - ignore(List.map - (fun current -> - Indexing.check_target c current "forward new neg") new_neg); - ignore(List.map - (fun current -> Indexing.check_target c current "forward new pos") + ignore(List.map + (fun current -> + Indexing.check_target c current "forward new neg") new_neg); + ignore(List.map + (fun current -> Indexing.check_target c current "forward new pos") new_pos;) end; let t1 = Unix.gettimeofday () in @@ -758,6 +757,62 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = ;; +(** simplifies a goal with equalities in active and passive *) +let rec 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 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 + changed, if not changed then goal + else snd (simplify_goal env goal ?passive (active_list, active_table)) +;; + + +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 +;; + + (** simplifies active usign new *) let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in @@ -868,16 +923,16 @@ let close env new' given = List.fold_left (fun (n,p) (s,c) -> let neg,pos = infer env s c (new_pos,new_table) in - neg@n,pos@p) + neg@n,pos@p) ([],[]) given ;; let is_commutative_law eq = let w, proof, (eq_ty, left, right, order), metas = snd eq in match left,right with - Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], - Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> - f1 = f2 && a1 = b2 && a2 = b1 + Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], + Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> + f1 = f2 && a1 = b2 && a2 = b1 | _ -> false ;; @@ -934,60 +989,6 @@ let activate_theorem (active, passive) = ;; -(** simplifies a goal with equalities in active and passive *) -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 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 - 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 = @@ -1066,6 +1067,7 @@ let simplify_equalities env equalities = res ;; +(* (* applies equality to goal to see if the goal can be closed *) let apply_equality_to_goal env equality goal = let module C = Cic in @@ -1082,12 +1084,11 @@ let apply_equality_to_goal env equality goal = (* (string_of_equality equality) (CicPp.ppterm gterm))); *) try let subst, metasenv', _ = - let menv = metasenv @ metas @ gmetas in Inference.unification metas gmetas context eqterm gterm ugraph in let newproof = match proof with - | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t) + | I.BasicProof (subst',t) -> I.BasicProof (subst@subst',t) | I.ProofBlock (s, uri, nt, t, pe, p) -> I.ProofBlock (subst @ s, uri, nt, t, pe, p) | _ -> assert false @@ -1096,13 +1097,15 @@ let apply_equality_to_goal env equality goal = 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) + | I.BasicProof _ -> newproof + | I.SubProof (t, i, p) -> + prerr_endline "SUBPROOF!"; + I.SubProof (t, i, repl p) | _ -> assert false in repl gproof in - true, subst, newgproof + true, (subst:Inference.substitution), newgproof with CicUnification.UnificationFailure _ -> false, [], I.NoProof ;; @@ -1161,9 +1164,9 @@ let apply_to_goal env theorems ?passive active goal = 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.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 @@ -1190,10 +1193,11 @@ let apply_to_goal env theorems ?passive active goal = ProofGoalBlock (sp1, gp sp2) | BasicProof _ | NoProof -> - SubProof (p, i, BasicProof (Cic.Meta (i, irl))) + SubProof (p, i, BasicProof ([],Cic.Meta (i, irl))) | ProofSymBlock (s, sp) -> ProofSymBlock (s, gp sp) | ProofBlock (s, u, nt, t, pe, sp) -> + prerr_endline "apply_to_goal!"; ProofBlock (s, u, nt, t, pe, gp sp) in gp proof in @@ -1241,7 +1245,7 @@ let apply_to_goal env theorems ?passive active goal = else false, [], [] in - if r = true then `Ok (s, l) else aux theorems + if r = true then `Ok ((s:Cic.substitution),l) else aux theorems ;; @@ -1290,13 +1294,13 @@ let rec apply_to_goal_conj env theorems ?passive active (depth, goals) = let propagate_subst subst (proof, metas, term) = let rec repl = function | NoProof -> NoProof - | BasicProof t -> - BasicProof (CicMetaSubst.apply_subst subst t) + | BasicProof (subst',t) -> + BasicProof (subst@subst',t) | ProofGoalBlock (p, pb) -> let pb' = repl pb in ProofGoalBlock (p, pb') | SubProof (t, i, p) -> - let t' = CicMetaSubst.apply_subst subst t in + let t' = Inference.apply_subst subst t in let p = repl p in SubProof (t', i, p) | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) @@ -1578,10 +1582,8 @@ let apply_theorem_to_goals env theorems active goals = ok, (a_goals, p_goals) ;; - (* given-clause algorithm with lazy reduction strategy *) let rec given_clause dbd env goals theorems passive active = - let _,context,_ = env in let goals = simplify_goals env goals active in let ok, goals = activate_goal goals in (* let theorems = simplify_theorems env theorems active in *) @@ -1648,7 +1650,7 @@ and given_clause_aux dbd env goals theorems passive active = let (sign, current), passive = select env (fst goals) passive active in let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in prerr_endline ("Selected = " ^ - (CicPp.pp (Inference.term_of_equality current) names)); + (CicPp.pp (Inference.term_of_equality current) names)); let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in @@ -1737,10 +1739,16 @@ and given_clause_aux dbd env goals theorems passive active = ParamodulationSuccess (proof, env) ) ;; +*) +let counter = ref 0 (** given-clause algorithm with full reduction strategy *) let rec given_clause_fullred dbd env goals theorems passive active = +(* + let table,list = active in + assert (check_table list table); +*) let goals = simplify_goals env goals ~passive active in let _,context,_ = env in let ok, goals = activate_goal goals in @@ -1761,30 +1769,81 @@ let rec given_clause_fullred dbd env goals theorems passive active = (* (Printf.sprintf "goal activated:\n%s\n%s\n" *) (* (CicPp.ppterm t) (string_of_proof p))); *) (* in *) - let ok, goals = - apply_goal_to_theorems dbd env theorems ~passive active goals - in + let ok, proof = + (* apply_goal_to_theorems dbd env theorems ~passive active goals in *) + let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in + match (fst goals) with + | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ + when left = right && iseq uri -> + let p = + Cic.Appl [Cic.MutConstruct (* reflexivity *) + (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left] + 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, Some newp + | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_-> + (* here we check if the goal is subsumed by an active *) + let ok, subst = + (* the first m is unused *) + Indexing.subsumption (m,context,CicUniv.empty_ugraph) + (snd active) + (0,proof,(eq_ty,left,right,Eq),m) + in + if ok then + begin + prerr_endline "The goal is subsumed by an active"; + false, None + end + else + ok, None + | _ -> false, None + in if ok then - let proof = - match (fst goals) with - | (_, [proof, _, _])::_ -> Some proof - | _ -> assert false - in ( prerr_endline "esco qui"; + let active = + List.filter test (fst active) in + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + active))) + in prerr_endline s; + let passive = + List.filter + (fun x -> test (1,x)) + (let x,y,_ = passive in (fst x)@(fst y)) in + let p = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> + (string_of_equality ~env e)) + passive))) + in prerr_endline p; (* - let s = Printf.sprintf "actives:\n%s\n" - (String.concat "\n" + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" ((List.map - (fun (s, e) -> (string_of_sign s) ^ " " ^ + (fun (s, e) -> (string_of_sign s) ^ " " ^ (string_of_equality ~env e)) - (fst active)))) in - let sp = Printf.sprintf "passives:\n%s\n" - (String.concat "\n" + (fst active)))) in + let sp = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" (List.map - (string_of_equality ~env) - (let x,y,_ = passive in (fst x)@(fst y)))) in - prerr_endline s; - prerr_endline sp; *) + (string_of_equality ~env) + (let x,y,_ = passive in (fst x)@(fst y)))) in + prerr_endline s; + prerr_endline sp; *) ParamodulationSuccess (proof, env)) else given_clause_fullred_aux dbd env goals theorems passive active @@ -1806,10 +1865,29 @@ let rec given_clause_fullred dbd env goals theorems passive active = else given_clause_fullred_aux dbd env goals theorems passive active and given_clause_fullred_aux dbd env goals theorems passive active = - prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^ + prerr_endline (string_of_int !counter ^ + " MAXMETA: " ^ string_of_int !maxmeta ^ " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ - " #ACTIVES: " ^ string_of_int (size_of_active active) ^ + " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); + incr counter; +(* if !counter mod 10 = 0 then + begin + let size = HExtlib.estimate_size (passive,active) in + let sizep = HExtlib.estimate_size (passive) in + let sizea = HExtlib.estimate_size (active) in + let (l1,s1),(l2,s2), t = passive in + let sizetbl = HExtlib.estimate_size t in + let sizel = HExtlib.estimate_size (l1,l2) in + let sizes = HExtlib.estimate_size (s1,s2) in + + prerr_endline ("SIZE: " ^ string_of_int size); + prerr_endline ("SIZE P: " ^ string_of_int sizep); + prerr_endline ("SIZE A: " ^ string_of_int sizea); + prerr_endline ("SIZE TBL: " ^ string_of_int sizetbl ^ + " SIZE L: " ^ string_of_int sizel ^ + " SIZE S:" ^ string_of_int sizes); + end;*) (* if (size_of_active active) mod 50 = 0 then (let s = Printf.sprintf "actives:\n%s\n" @@ -1855,10 +1933,20 @@ and given_clause_fullred_aux dbd env goals theorems passive active = given_clause_fullred dbd env goals theorems passive active | false -> let (sign, current), passive = select env (fst goals) passive active in - let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in - prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^ - string_of_equality ~env current); - (* (CicPp.pp (Inference.term_of_equality current) names));*) + prerr_endline + ("Selected = " ^ (string_of_sign sign) ^ " " ^ + string_of_equality ~env current); +(* ^ + (let w,p,(t,l,r,o),m = current in + " size w: " ^ string_of_int (HExtlib.estimate_size w)^ + " size p: " ^ string_of_int (HExtlib.estimate_size p)^ + " size t: " ^ string_of_int (HExtlib.estimate_size t)^ + " size l: " ^ string_of_int (HExtlib.estimate_size l)^ + " size r: " ^ string_of_int (HExtlib.estimate_size r)^ + " size o: " ^ string_of_int (HExtlib.estimate_size o)^ + " size m: " ^ string_of_int (HExtlib.estimate_size m)^ + " size m-c: " ^ string_of_int + (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *) let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in @@ -1868,11 +1956,24 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (* weight_age_counter := !weight_age_counter + 1; *) given_clause_fullred dbd env goals theorems passive active | Some (sign, current) -> + if test (sign, current) then + (prerr_endline + ("Simplified = " ^ (string_of_sign sign) ^ " " ^ + string_of_equality ~env current); + let active = fst active in + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + active))) + in prerr_endline s; + assert false); 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 + let _, proof, _, m = current in ParamodulationSuccess (Some proof, env) ) else ( debug_print @@ -1883,7 +1984,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = let t1 = Unix.gettimeofday () in let new' = infer env sign current active in - let _ = + let _ = match new' with | neg, pos -> debug_print @@ -1910,13 +2011,14 @@ and given_clause_fullred_aux dbd env goals theorems passive active = in let rec simplify new' active passive = let t1 = Unix.gettimeofday () in - let new' = forward_simplify_new env new' ~passive active 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 + backward_simplify env new' ~passive active in + let t2 = Unix.gettimeofday () in backward_simpl_time := !backward_simpl_time +. (t2 -. t1); match newa, retained with @@ -1924,18 +2026,23 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | Some (n, p), None | None, Some (n, p) -> let nn, np = new' in - if Utils.debug_metas then - ignore ( - List.map (fun x -> Indexing.check_target context x "simplify1")n; - List.map (fun x -> Indexing.check_target context x "simplify2")p); - simplify (nn @ n, np @ p) active passive + if Utils.debug_metas then + begin + List.iter + (fun x->Indexing.check_target context x "simplify1") + n; + List.iter + (fun x->Indexing.check_target context x "simplify2") + p + end; + 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 active, _, new' = simplify new' active passive in (* pessima prova - let new1 = prova env new' active in + let new1 = prova env new' active in let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in let _ = match new1 with @@ -1992,8 +2099,15 @@ end prova *) in ParamodulationSuccess (proof, env) ) + ;; +let profiler0 = HExtlib.profile "P/Saturation.given_clause_fullred" + +let given_clause_fullred dbd env goals theorems passive active = + profiler0.HExtlib.profile + (given_clause_fullred dbd env goals theorems passive) active + let rec saturate_equations env goal accept_fun passive active = elapsed_time := Unix.gettimeofday () -. !start_time; @@ -2127,7 +2241,7 @@ let main dbd full term metasenv ugraph = (fst theorems))))) in (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in + let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in @@ -2147,7 +2261,7 @@ let main dbd full term metasenv ugraph = start_time := Unix.gettimeofday (); let res = let goals = make_goals goal in - (if !use_fullred then given_clause_fullred else given_clause) + (if !use_fullred then given_clause_fullred else given_clause_fullred) dbd env goals theorems passive active in let finish = Unix.gettimeofday () in @@ -2189,29 +2303,29 @@ let main dbd full term metasenv ugraph = | ParamodulationSuccess (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in - if Utils.time then - begin - prerr_endline - ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ + if Utils.time then + begin + prerr_endline + ((Printf.sprintf ("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.sprintf "beta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "passive_maintainance_time: %.9f\n" - !passive_maintainance_time) ^ - (Printf.sprintf " successful unification/matching time: %.9f\n" - !Indexing.match_unif_time_ok) ^ - (Printf.sprintf " failed unification/matching time: %.9f\n" - !Indexing.match_unif_time_no) ^ - (Printf.sprintf " indexing retrieval time: %.9f\n" - !Indexing.indexing_retrieval_time) ^ - (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" - !Indexing.build_newtarget_time) ^ - (Printf.sprintf "derived %d clauses, kept %d clauses.\n" - !derived_clauses !kept_clauses)) - end + (Printf.sprintf "beta_expand_time: %.9f\n" + !Indexing.beta_expand_time) ^ + (Printf.sprintf "passive_maintainance_time: %.9f\n" + !passive_maintainance_time) ^ + (Printf.sprintf " successful unification/matching time: %.9f\n" + !Indexing.match_unif_time_ok) ^ + (Printf.sprintf " failed unification/matching time: %.9f\n" + !Indexing.match_unif_time_no) ^ + (Printf.sprintf " indexing retrieval time: %.9f\n" + !Indexing.indexing_retrieval_time) ^ + (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" + !Indexing.build_newtarget_time) ^ + (Printf.sprintf "derived %d clauses, kept %d clauses.\n" + !derived_clauses !kept_clauses)) + end (* with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); @@ -2243,17 +2357,19 @@ let reset_refs () = Inference.metas_of_proof_time := 0.; ;; -let saturate +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; +(* CicUnification.unif_ty := false;*) 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 + prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context)); let eq_indexes, equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = @@ -2266,8 +2382,8 @@ let saturate ty in let ugraph = CicUniv.empty_ugraph in - let env = (metasenv, context, ugraph) in - let goal = Inference.BasicProof new_meta_goal, [], goal in + let env = (metasenv, context, ugraph) in + let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -2323,9 +2439,10 @@ let saturate (res, finish -. start) in match res with - | ParamodulationSuccess (Some proof, env) -> + | ParamodulationSuccess (Some proof, _) -> debug_print (lazy "OK, found a proof!"); let proof = Inference.build_proof_term proof in + (* prerr_endline (CicPp.ppterm proof); *) let names = names_of_context context in let newmetasenv = let i1 = @@ -2378,24 +2495,24 @@ let saturate let tdemodulate = fs_time_info.demodulate in let tsubsumption = fs_time_info.subsumption in if Utils.time then - begin - prerr_endline ( - (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ - (Printf.sprintf "\ntall: %.9f" tall) ^ - (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ - (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ - (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ - (Printf.sprintf "\nbeta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "\nmetas_of_proof: %.9f\n" - !Inference.metas_of_proof_time) ^ - (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ - (Printf.sprintf "\nforward_simpl_new_times: %.9f" - !forward_simpl_new_time) ^ - (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ - (Printf.sprintf "\npassive_maintainance_time: %.9f" - !passive_maintainance_time)) - end; + begin + prerr_endline ( + (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ + (Printf.sprintf "\ntall: %.9f" tall) ^ + (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ + (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ + (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ + (Printf.sprintf "\nbeta_expand_time: %.9f\n" + !Indexing.beta_expand_time) ^ + (Printf.sprintf "\nmetas_of_proof: %.9f\n" + !Inference.metas_of_proof_time) ^ + (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ + (Printf.sprintf "\nforward_simpl_new_times: %.9f" + !forward_simpl_new_time) ^ + (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ + (Printf.sprintf "\npassive_maintainance_time: %.9f" + !passive_maintainance_time)) + end; newstatus | _ -> raise (ProofEngineTypes.Fail (lazy "NO proof found")) @@ -2438,14 +2555,14 @@ let retrieve_and_print dbd term metasenv ugraph = debug_print (lazy (Printf.sprintf "\n\nequalities:\n%s\n" - (String.concat "\n" + (String.concat "\n" (List.map - (fun (u, e) -> -(* Printf.sprintf "%s: %s" *) - (UriManager.string_of_uri u) -(* (string_of_equality e) *) - ) - equalities)))); + (fun (u, e) -> +(* Printf.sprintf "%s: %s" *) + (UriManager.string_of_uri u) +(* (string_of_equality e) *) + ) + equalities)))); debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let (u, e) = e in @@ -2459,36 +2576,36 @@ let retrieve_and_print dbd term metasenv ugraph = let res = forward_simplify env (Positive, e) (active, tbl) in match others with | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl ((u, (snd e))::others_simpl) - ) + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl ((u, (snd e))::others_simpl) + ) | [] -> ( - match res with - | None -> others_simpl - | Some e -> (u, (snd e))::others_simpl - ) + match res with + | None -> others_simpl + | Some e -> (u, (snd e))::others_simpl + ) in let _equalities = match equalities with | [] -> [] | hd::tl -> - let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) - let res = - List.rev (simpl (*(Positive,*) hd others []) - in - debug_print - (lazy - (Printf.sprintf "\nequalities AFTER:\n%s\n" - (String.concat "\n" - (List.map - (fun (u, e) -> - Printf.sprintf "%s: %s" - (UriManager.string_of_uri u) - (string_of_equality e) - ) - res)))); - res in + let others = tl in (* List.map (fun e -> (Positive, e)) tl in *) + let res = + List.rev (simpl (*(Positive,*) hd others []) + in + debug_print + (lazy + (Printf.sprintf "\nequalities AFTER:\n%s\n" + (String.concat "\n" + (List.map + (fun (u, e) -> + Printf.sprintf "%s: %s" + (UriManager.string_of_uri u) + (string_of_equality e) + ) + res)))); + res in debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))) @@ -2525,7 +2642,7 @@ let main_demod_equalities dbd term metasenv ugraph = in let env = (metasenv, context, ugraph) in (*try*) - let goal = Inference.BasicProof new_meta_goal, [], goal in + let goal = Inference.BasicProof ([],new_meta_goal), [], goal in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in let passive = make_passive [] equalities in @@ -2585,7 +2702,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in let goalterm = Cic.Meta (metano,irl) in - let initgoal = Inference.BasicProof goalterm, [], ty in + let initgoal = Inference.BasicProof ([],goalterm), [], ty in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = simplify_equalities env (equalities@library_equalities) in let table = @@ -2600,15 +2717,15 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = begin let opengoal = Cic.Meta(maxm,irl) in let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in + Inference.build_proof_term ~noproof:opengoal newproof in let extended_metasenv = (maxm,context,newty)::metasenv in - let extended_status = - (curi,extended_metasenv,pbo,pty),goal in - let (status,newgoals) = - ProofEngineTypes.apply_tactic - (PrimitiveTactics.apply_tac ~term:proofterm) - extended_status in - (status,maxm::newgoals) + let extended_status = + (curi,extended_metasenv,pbo,pty),goal in + let (status,newgoals) = + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:proofterm) + extended_status in + (status,maxm::newgoals) end else if newty = ty then raise (ProofEngineTypes.Fail (lazy "no progress"))