(* 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 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
bag, p
in
bag, Some (goalproof, p, id, subst, cicmenv)
- | None -> bag, None)
+ | None ->
+ bag, None)
| _ -> bag, None
;;
(fun (subst, equality, swapped) (bag,acc) ->
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
- Indexing.check_for_duplicates cicmenv "from subsumption";
+ if Utils.debug_metas then
+ Indexing.check_for_duplicates cicmenv "from subsumption";
let bag, p =
if swapped then
Equality.symmetric bag eq_ty l id uri m
([],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))])
-(* 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 =
| [] -> bag, (active_goals, [])
| hd::tl ->
let changed, selected = simplify_goal bag env hd active in
- let (_,_,t1) = selected in
+ let (_,m1,t1) = selected in
let already_in =
List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
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 =
| 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
;;
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) ->
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
projects / helm.git / blobdiff