(* 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;;
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
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 =
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 ;;
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
;;
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 =
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
(* 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 =
(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 *)
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
([],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 ->
| 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
;;
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"
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
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 =
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) ->
projects / helm.git / commitdiff