From da3031c3a830df0aaab4f57b63689a1b20d7ab89 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 30 Apr 2009 13:03:25 +0000 Subject: [PATCH] Added a passive table --- .../tactics/paramodulation/saturation.ml | 70 +++++++++++-------- 1 file changed, 41 insertions(+), 29 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 7ee7d6b16..fb6017839 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 new_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,7 +899,9 @@ 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))]) + (fun bag -> check_if_goal_is_subsumed bag env (snd active)); + (fun bag -> check_if_goal_is_subsumed bag env (last passive)) + ]) (* provare active and passive?*) (bag,None) active_goals ;; @@ -1051,7 +1061,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 +1083,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 +1111,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 = @@ -1629,7 +1640,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) -> -- 2.39.2