X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=c5f3132e9aa5e5e1cb56849862f78e09175f0aed;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=7ee7d6b162d5f439b5fad8a45917bf57c9e3f75a;hpb=b8934a9598d747662139c74c751b8223bcc19d03;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 7ee7d6b16..c5f3132e9 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -29,6 +29,9 @@ (* set to false to disable paramodulation inside auto_tac *) +let fst3 a,_,_ = a;; +let last _,_,a = a;; + let connect_to_auto = true;; let debug_print = Utils.debug_print;; @@ -106,7 +109,7 @@ end module EqualitySet = Set.Make(OrderedEquality);; -type passive_table = Equality.equality list * EqualitySet.t +type passive_table = Equality.equality list * EqualitySet.t * Indexing.Index.t type active_table = Equality.equality list * Indexing.Index.t type new_proof = Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv @@ -117,8 +120,8 @@ type result = new_proof * active_table * passive_table * Equality.equality_bag ;; -let list_of_passive (l,s) = l ;; -let list_of_active (l,s) = l ;; +let list_of_passive (l,_,_) = l ;; +let list_of_active (l,_) = l ;; let make_passive eq_list = let set = @@ -126,7 +129,8 @@ let make_passive eq_list = in (* we have the invariant that the list and the set have the same * cardinality *) - EqualitySet.elements set, set + EqualitySet.elements set, set, + List.fold_left Indexing.index Indexing.empty eq_list ;; let make_empty_active () = [], Indexing.empty ;; @@ -134,12 +138,12 @@ let make_active eq_list = eq_list, List.fold_left Indexing.index Indexing.empty eq_list ;; -let size_of_passive (passive_list, _) = List.length passive_list;; +let size_of_passive (passive_list, _,_) = List.length passive_list;; let size_of_active (active_list, _) = List.length active_list;; let passive_is_empty = function - | [], s when EqualitySet.is_empty s -> true - | [], s -> assert false (* the set and the list should be in sync *) + | [], s , _ when EqualitySet.is_empty s -> true + | [], s ,_ -> assert false (* the set and the list should be in sync *) | _ -> false ;; @@ -162,28 +166,29 @@ let rec select env g passive = match (List.rev goals) with goal::_ -> goal | _ -> assert false in *) - let pos_list, pos_set = passive in + let pos_list, pos_set, pos_table = passive in let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with | 0 -> ( weight_age_counter := !weight_age_ratio; - let skip_giant pos_list pos_set = + let skip_giant pos_list pos_set pos_table = match pos_list with | (hd:EqualitySet.elt)::tl -> let w,_,_,_,_ = Equality.open_equality hd in if w < 30 then - hd, (tl, EqualitySet.remove hd pos_set) + hd, (tl, EqualitySet.remove hd pos_set, + Indexing.remove_index pos_table hd) else (* (prerr_endline ("+++ skipping giant of size "^string_of_int w^" +++"); *) - select env g (tl@[hd],pos_set) + select env g (tl@[hd],pos_set,pos_table) | _ -> assert false in - skip_giant pos_list pos_set) + skip_giant pos_list pos_set pos_table) (* let rec skip_giant pos_list pos_set = @@ -254,20 +259,22 @@ let rec select env g passive = in (* let current = EqualitySet.min_elt pos_set in *) let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in - current,(remove current pos_list, EqualitySet.remove current pos_set) + current,(remove current pos_list, EqualitySet.remove current pos_set, + Indexing.remove_index pos_table current) ;; let filter_dependent bag passive id = - let pos_list, pos_set = passive in + let pos_list, pos_set, pos_table = passive in let passive,no_pruned = List.fold_right - (fun eq ((list,set),no) -> + (fun eq ((list,set,table),no) -> if Equality.depend bag eq id then - (list, EqualitySet.remove eq set), no + 1 + (list, EqualitySet.remove eq set,Indexing.remove_index table eq), + no + 1 else - (eq::list, set), no) - pos_list (([],pos_set),0) + (eq::list,set,table), no) + pos_list (([],pos_set,pos_table),0) in (* if no_pruned > 0 then @@ -279,7 +286,7 @@ let filter_dependent bag passive id = (* adds to passive a list of equalities new_pos *) let add_to_passive passive new_pos preferred = - let pos_list, pos_set = passive in + let pos_list, pos_set , pos_table = passive in let ok set equality = not (EqualitySet.mem equality set) in let pos = List.filter (ok pos_set) new_pos in let add set equalities = @@ -290,7 +297,8 @@ let add_to_passive passive new_pos preferred = (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred) pos in - pos_head @ pos_list @ pos_tail, add pos_set pos + pos_head @ pos_list @ pos_tail, add pos_set pos, + List.fold_left Indexing.index pos_table pos ;; (* TODO *) @@ -784,8 +792,8 @@ let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) = Equality.mk_equality bag (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) in - match Indexing.subsumption env table goal_equation with - (* match Indexing.unification env table goal_equation with *) + (* match Indexing.subsumption env table goal_equation with *) + match Indexing.unification env table goal_equation with | Some (subst, equality, swapped ) -> (* prerr_endline @@ -882,7 +890,7 @@ let simplify_goal_set bag env goals active = ([],passive_goals) active_goals ;; -let check_if_goals_set_is_solved bag env active goals = +let check_if_goals_set_is_solved bag env active passive goals = let active_goals, passive_goals = goals in List.fold_left (fun (bag, proof) goal -> @@ -891,9 +899,10 @@ let check_if_goals_set_is_solved bag env active goals = | None -> check bag goal [ (fun b x -> b, check_if_goal_is_identity env x); - (fun bag -> check_if_goal_is_subsumed bag env (snd active))]) -(* provare active and passive?*) - (bag,None) active_goals + (fun bag -> check_if_goal_is_subsumed bag env (snd active)); + (fun bag -> check_if_goal_is_subsumed bag env (last passive)) + ]) + (bag,None) (active_goals @ passive_goals) ;; let infer_goal_set bag env active goals = @@ -1051,7 +1060,7 @@ let given_clause else bag, goals in - match check_if_goals_set_is_solved bag env active goals with + match check_if_goals_set_is_solved bag env active passive goals with | bag, Some p -> debug_print (lazy (Printf.sprintf "\nFound a proof in: %f\n" @@ -1073,14 +1082,15 @@ let given_clause if max g_iterno s_iterno mod 40 = 0 then (print_status (max g_iterno s_iterno) goals active passive; let active = List.map Equality.id_of (fst active) in - let passive = List.map Equality.id_of (fst passive) in + let passive = List.map Equality.id_of (fst3 passive) in let goal = ids_of_goal_set goals in Equality.collect bag active passive goal) else bag in if s_iterno > saturation_steps then - ParamodulationFailure ("max saturation steps",active,passive,bag) + step bag goals passive active (g_iterno+1) (s_iterno+1) + (* ParamodulationFailure ("max saturation steps",active,passive,bag) *) else let current, passive = select env goals passive in match add_to_active_aux bag active passive env eq_uri current with @@ -1100,7 +1110,7 @@ let given_clause step bag goals passive active (g_iterno+1) (s_iterno+1) end in - step bag goals passive active 1 1 + step bag goals passive active 0 0 ;; let rec saturate_equations bag eq_uri env goal accept_fun passive active = @@ -1185,9 +1195,15 @@ let add_to_active bag active passive env ty term newmetas = | Some eq_uri -> try let bag, current = Equality.equality_of_term bag term ty newmetas in - let bag, current = Equality.fix_metas bag current in - match add_to_active_aux bag active passive env eq_uri current with - | _,a,p,b -> a,p,b + let w,_,_,_,_ = Equality.open_equality current in + if w > 100 then + (HLog.debug + ("skipping giant " ^ CicPp.ppterm term ^ " of weight " ^ + string_of_int w); active, passive, bag) + else + let bag, current = Equality.fix_metas bag current in + match add_to_active_aux bag active passive env eq_uri current with + | _,a,p,b -> a,p,b with | Equality.TermIsNotAnEquality -> active, passive, bag ;; @@ -1629,7 +1645,8 @@ let given_clause given_clause bag eq_uri env goals passive active goal_steps saturation_steps max_time with - | ParamodulationFailure (_,a,p,b) -> + | ParamodulationFailure (msg,a,p,b) -> + if Utils.debug then prerr_endline msg; None, a, p, b | ParamodulationSuccess ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p,b) -> @@ -1642,6 +1659,77 @@ let given_clause Some (subst, proof,gl),a,p, b ;; +let solve_narrowing bag status active passive goal_steps = + let proof, goalno = status in + let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in + let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in + let cleaned_goal = Utils.remove_local_context type_of_goal in + let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in + let canonical_menv,other_menv = + List.partition (fun (_,c,_) -> c = context) metasenv in + let canonical_menv = + List.map + (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv + in + let metasenv' = + List.filter + (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal) + canonical_menv + in + let goal = [], metasenv', cleaned_goal in + let env = metasenv,context,CicUniv.empty_ugraph in + let goals = + let table = List.fold_left Indexing.index (last passive) (fst active) in + goal :: Indexing.demodulation_all_goal bag env table goal 4 + in + let rec aux newactives newpassives bag = function + | [] -> bag, (newactives, newpassives) + | hd::tl -> + let selected = hd in + let (_,m1,t1) = selected in + let already_in = + List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) + newactives + in + if already_in then + aux newactives newpassives bag tl + else + let bag, newpassives = + if Utils.metas_of_term t1 = [] then + bag, newpassives + else + let bag, new' = + Indexing.superposition_left bag env (snd active) selected + in + let new' = + List.map + (fun x -> let b, x = simplify_goal bag env x active in x) + new' + in + bag, newpassives @ new' + in + aux (selected::newactives) newpassives bag tl + in + let rec do_n bag ag pg = function + | 0 -> None, active, passive, bag + | n -> + let bag, (ag, pg) = aux [] [] bag (ag @ pg) in + match check_if_goals_set_is_solved bag env active passive (ag,pg) with + | bag, None -> do_n bag ag pg (n-1) + | bag, Some (gproof,newproof,subsumption_id,subsumption_subst,pmenv)-> + let subst, proof, gl = + build_proof bag + status gproof newproof subsumption_id subsumption_subst pmenv + in + let uri,metasenv,subst,meta_proof,term_to_prove,attrs = proof in + let proof = + uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs + in + Some (subst, proof,gl),active,passive, bag + in + do_n bag [] goals goal_steps +;; + let add_to_passive eql passives = add_to_passive passives eql eql