From ae47205236492ae4271586cdf75a25597304da1e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 3 Jul 2006 11:48:44 +0000 Subject: [PATCH] - patch to consider the symbols of the goal when computing the weight of an equality. - actives simplified during fwd/back are not appended (but put in front) of the passive list --- .../tactics/paramodulation/saturation.ml | 99 ++++++++++--------- components/tactics/paramodulation/utils.ml | 38 +++++++ components/tactics/paramodulation/utils.mli | 1 + 3 files changed, 93 insertions(+), 45 deletions(-) diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 306f02dcf..4fe509981 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -224,8 +224,8 @@ let rec select env (goals,_) passive = | [] -> min | hd::tl -> my_min_elt (my_min hd min) tl in - (* let current = EqualitySet.min_elt pos_set in *) - let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in +(* let current = EqualitySet.min_elt pos_set in *) + let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in let passive_table = Indexing.remove_index passive_table current in @@ -276,7 +276,7 @@ let make_active () = (* adds to passive a list of equalities new_pos *) -let add_to_passive passive new_pos = +let add_to_passive passive new_pos preferred = let (pos_list, pos_set), table = passive in let ok set equality = not (EqualitySet.mem equality set) in let pos = List.filter (ok pos_set) new_pos in @@ -286,7 +286,12 @@ let add_to_passive passive new_pos = let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities in - (pos_list @ pos, add pos_set pos), + let pos_head, pos_tail = + List.partition + (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred) + pos + in + (pos_head @ pos_list @ pos_tail, add pos_set pos), table ;; @@ -976,24 +981,15 @@ let simplify_goal_set env goals ?passive active = let find (_,_,g) where = List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where in - let simplified = List.fold_left - (fun acc goal -> + (fun (acc_a,acc_p) goal -> match simplify_goal env goal ?passive active with | changed, g -> - if changed then prerr_endline "???????????????cambiato ancora"; - if find g acc then acc else g::acc) - (* active_goals active_goals *) - [] active_goals - in - if List.length active_goals <> List.length simplified then - prerr_endline "SEMPLIFICANDO HO SCARTATO..."; - (simplified,passive_goals) - (* - HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2) - (List.sort (fun (_,_,t1) (_,_,t2) -> compare t1 t1) - ((*goals @*) simplified)) - *) + if changed then + if find g acc_p then acc_a,acc_p else acc_a,g::acc_p + else + if find g acc_a then acc_a,acc_p else g::acc_a,acc_p) + ([],passive_goals) active_goals ;; let check_if_goals_set_is_solved env active goals = @@ -1069,8 +1065,7 @@ let infer_goal_set env active goals = *) let infer_goal_set_with_current env current goals active = - let active_goals, passive_goals = goals in - let active_goals, _ = + let active_goals, passive_goals = simplify_goal_set env goals active in let l,table,_ = build_table [current] in @@ -1096,13 +1091,26 @@ let ids_of_goal_set (ga,gp) = let size_of_goal_set_a (l,_) = List.length l;; let size_of_goal_set_p (_,l) = List.length l;; + +let pp_goals label goals context = + let names = Utils.names_of_context context in + List.iter + (fun _,_,g -> + prerr_endline + (Printf.sprintf "Current goal: %s = %s\n" label (CicPp.pp g names))) + (fst goals); + List.iter + (fun _,_,g -> + prerr_endline + (Printf.sprintf "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) + (snd goals); +;; (** given-clause algorithm with full reduction strategy: NEW implementation *) (* here goals is a set of goals in OR *) let given_clause eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time = - let names = Utils.names_of_context context in let initial_time = Unix.gettimeofday () in let iterations_left iterno = let now = Unix.gettimeofday () in @@ -1171,27 +1179,21 @@ let given_clause Equality.collect active passive goal end; let current, passive = select env goals passive in - let _ = - List.iter - (fun _,_,g -> - prerr_endline (Printf.sprintf "Current goal = %s\n" - (CicPp.pp g names))) - (fst goals); - List.iter - (fun _,_,g -> - prerr_endline (Printf.sprintf "Passive goal = %s\n" - (CicPp.pp g names))) - (snd goals); - prerr_endline (Printf.sprintf "Selected = %s\n" - (Equality.string_of_equality ~env current)) - in (* SIMPLIFICATION OF CURRENT *) + prerr_endline + ("Selected : " ^ + Equality.string_of_equality ~env current); let res = forward_simplify eq_uri env (Utils.Positive, current) active in match res with | None -> step goals theorems passive active (iterno+1) | Some current -> +(* + prerr_endline + ("Selected simpl: " ^ + Equality.string_of_equality ~env current); +*) (* GENERATION OF NEW EQUATIONS *) prerr_endline "infer"; let new' = infer eq_uri env current active in @@ -1214,7 +1216,7 @@ let given_clause in (* FORWARD AND BACKWARD SIMPLIFICATION *) prerr_endline "fwd/back simpl"; - let rec simplify new' active passive = + let rec simplify new' active passive head = let new' = forward_simplify_new eq_uri env new' ~passive active in @@ -1225,12 +1227,15 @@ let given_clause List.fold_left filter_dependent passive pruned in match newa, retained with - | None, None -> active, passive, new' + | None, None -> active, passive, new', head | Some p, None - | None, Some p -> simplify (new' @ p) active passive - | Some p, Some rp -> simplify (new' @ p @ rp) active passive + | None, Some p -> simplify (new' @ p) active passive head + | Some p, Some rp -> + simplify (new' @ p @ rp) active passive (head @ p) + in + let active, passive, new', head = + simplify new' active passive [] in - let active, passive, new' = simplify new' active passive in prerr_endline "simpl goal with new"; let goals = let a,b,_ = build_table new' in @@ -1239,7 +1244,7 @@ let given_clause let _ = <:stop> in rc in - let passive = add_to_passive passive new' in + let passive = add_to_passive passive new' head in step goals theorems passive active (iterno+1) end in @@ -1300,7 +1305,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active = (Equality.string_of_equality ~env e)) new')))) in let new' = List.filter accept_fun new' in - let passive = add_to_passive passive new' in + let passive = add_to_passive passive new' [] in saturate_equations eq_uri env goal accept_fun passive active ;; @@ -1516,11 +1521,12 @@ let saturate let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in + let cleaned_goal = Utils.remove_local_context type_of_goal in + Utils.set_goal_symbols cleaned_goal; let names = Utils.names_of_context context in let eq_indexes, equalities, maxm = Inference.find_equalities context proof in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let cleaned_goal = Utils.remove_local_context type_of_goal in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in let res, time = let t1 = Unix.gettimeofday () in @@ -1575,7 +1581,7 @@ let saturate *) let goals = make_goal_set goal in let max_iterations = 10000 in - let max_time = Unix.gettimeofday () +. 300. (* minutes *) in + let max_time = Unix.gettimeofday () +. 600. (* minutes *) in given_clause eq_uri env goals theorems passive active max_iterations max_time in @@ -1993,6 +1999,9 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql; if demod_table <> "" then begin + let eql = + if eql = [] then [eq_what] else eql + in let demod = let demod = Str.split (Str.regexp "_") demod_table in List.map (fun other -> find_in_ctx 1 other context) demod diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index 542c2dd77..8d0ba901b 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -299,6 +299,29 @@ end module IntSet = Set.Make(OrderedInt) +let goal_symbols = ref TermSet.empty + +let set_of_map m = + TermMap.fold (fun k _ s -> TermSet.add k s) m TermSet.empty +;; + +let set_goal_symbols term = + let m = symbols_of_term term in + goal_symbols := (set_of_map m) +;; + +let symbols_of_eq (ty,left,right,_) = + let sty = set_of_map (symbols_of_term ty) in + let sl = set_of_map (symbols_of_term left) in + let sr = set_of_map (symbols_of_term right) in + TermSet.union sty (TermSet.union sl sr) +;; + +let distance sgoal seq = + let s = TermSet.diff seq sgoal in + TermSet.cardinal s +;; + let compute_equality_weight (ty,left,right,o) = let factor = 2 in match o with @@ -321,6 +344,21 @@ let compute_equality_weight (ty,left,right,o) = w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2)) ;; +let compute_equality_weight e = + let w = compute_equality_weight e in + let d = distance !goal_symbols (symbols_of_eq e) in +(* + prerr_endline (Printf.sprintf "dist %s --- %s === %d" + (String.concat ", " (List.map (CicPp.ppterm) (TermSet.elements + !goal_symbols))) + (String.concat ", " (List.map (CicPp.ppterm) (TermSet.elements + (symbols_of_eq e)))) + d + ); +*) + w + d +;; + (* old let compute_equality_weight (ty,left,right,o) = let metasw = ref 0 in diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index c64eacfd6..d761045b8 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -63,6 +63,7 @@ val names_of_context: Cic.context -> (Cic.name option) list module TermMap: Map.S with type key = Cic.term val symbols_of_term: Cic.term -> int TermMap.t +val set_goal_symbols: Cic.term -> unit val lpo: Cic.term -> Cic.term -> comparison -- 2.39.2