* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id$ *)
of weight, age and goal-similarity
*)
-let rec select env (goals,_) passive =
+let rec select env g passive =
processed_clauses := !processed_clauses + 1;
+(*
let goal =
match (List.rev goals) with goal::_ -> goal | _ -> assert false
in
+*)
let pos_list, pos_set = passive in
let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
if !weight_age_ratio > 0 then
match !weight_age_counter with
| 0 -> (
weight_age_counter := !weight_age_ratio;
+ let skip_giant pos_list pos_set =
+ 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)
+ else
+(*
+ (prerr_endline
+ ("+++ skipping giant of size "^string_of_int w^" +++");
+*)
+ select env g (tl@[hd],pos_set)
+ | _ -> assert false
+ in
+ skip_giant pos_list pos_set)
+
+(*
let rec skip_giant pos_list pos_set =
match pos_list with
| (hd:EqualitySet.elt)::tl ->
let w,_,_,_,_ = Equality.open_equality hd in
let pos_set = EqualitySet.remove hd pos_set in
- if w < 500 then
+ if w < 30 then
hd, (tl, pos_set)
else
(prerr_endline
("+++ skipping giant of size "^string_of_int w^" +++");
skip_giant tl pos_set)
| _ -> assert false
- in
- skip_giant pos_list pos_set)
+ in
+ skip_giant pos_list pos_set)
+
+*)
+(*
| _ when (!symbols_counter > 0) ->
(symbols_counter := !symbols_counter - 1;
let cardinality map =
let _, current = EqualitySet.fold f pos_set initial in
current,
(remove current pos_list, EqualitySet.remove current pos_set))
+*)
| _ ->
symbols_counter := !symbols_ratio;
let my_min e1 e2 =
(eq::list, set), no)
pos_list (([],pos_set),0)
in
+(*
if no_pruned > 0 then
prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++");
+*)
passive
;;
let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
maxmeta := maxm;
let active_table = Indexing.index active_table copy_of_current in
- let _ = <:start<current contro active>> in
+(* let _ = <:start<current contro active>> in *)
let maxm, res =
Indexing.superposition_right eq_uri !maxmeta env active_table current
in
- let _ = <:stop<current contro active>> in
+(* let _ = <:stop<current contro active>> in *)
if Utils.debug_metas then
ignore(List.map
(function current ->
maxmeta := maxm;
*)
let curr_table = Indexing.index Indexing.empty current in
- let _ = <:start<active contro current>> in
+(* let _ = <:start<active contro current>> in *)
let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
- let _ = <:stop<active contro current>> in
+(* let _ = <:stop<active contro current>> in *)
if Utils.debug_metas then
ignore(List.map
(function current ->
(* match Indexing.subsumption env table goal_equation with*)
match Indexing.unification env table goal_equation with
| Some (subst, equality, swapped ) ->
+(*
prerr_endline
- ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+ ("GOAL SUBSUMED IS: "^Equality.string_of_equality goal_equation ~env);
prerr_endline
- ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
- prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
+ ("GOAL IS SUBSUMED BY: "^Equality.string_of_equality equality ~env);
+ prerr_endline ("SUBST:"^Subst.ppsubst ~names subst);
+*)
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =
let find (_,_,g) where =
List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
in
+ (* prova:tengo le passive semplificate
+ let passive_goals =
+ List.map (fun g -> snd (simplify_goal env g active)) passive_goals
+ in *)
List.fold_left
(fun (acc_a,acc_p) goal ->
match simplify_goal env goal active with
check goal [
check_if_goal_is_identity env;
check_if_goal_is_subsumed env (snd active)])
+(* provare active and passive?*)
None active_goals
;;
| [] -> active_goals, []
| hd::tl ->
let changed,selected = simplify_goal env hd active in
+(*
if changed then
prerr_endline ("--------------- goal semplificato");
+*)
let (_,_,t1) = selected in
let already_in =
List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
(snd goals);
;;
+let print_status iterno goals active passive =
+ print_endline
+ (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
+ iterno (size_of_active active) (size_of_passive passive)
+ (size_of_goal_set_a goals) (size_of_goal_set_p goals))
+;;
+
(** given-clause algorithm with full reduction strategy: NEW implementation *)
(* here goals is a set of goals in OR *)
let given_clause
int_of_float iterations_left
in
let rec step goals theorems passive active iterno =
- pp_goals "xxx" goals context;
if iterno > max_iterations then
(ParamodulationFailure "No more iterations to spend")
else if Unix.gettimeofday () > max_time then
(ParamodulationFailure "No more time to spend")
else
-(*
- let _ = prerr_endline "simpl goal with active" in
- let _ = <:start<simplify goal set active>> in
- let goals = simplify_goal_set env goals passive active in
- let _ = <:stop<simplify goal set active>> in
-*)
let _ =
- prerr_endline
- (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n"
- iterno (size_of_active active) (size_of_passive passive)
- (size_of_goal_set_a goals) (size_of_goal_set_p goals))
+(* print_status iterno goals active passive *)
+ Printf.printf ".%!";
in
(* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
let passive =
passive
in
kept_clauses := (size_of_passive passive) + (size_of_active active);
- let goals = infer_goal_set env active goals in
+ let goals = infer_goal_set env active goals
+ in
match check_if_goals_set_is_solved env active goals with
| Some p ->
- prerr_endline
- (Printf.sprintf "Found a proof in: %f\n"
+ print_endline
+ (Printf.sprintf "\nFound a proof in: %f\n"
(Unix.gettimeofday() -. initial_time));
ParamodulationSuccess p
| None ->
(* COLLECTION OF GARBAGED EQUALITIES *)
if iterno mod 40 = 0 then
begin
+ print_status 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 goal = ids_of_goal_set goals in
end;
let current, passive = select env goals passive in
(* SIMPLIFICATION OF CURRENT *)
+(*
prerr_endline
("Selected : " ^
Equality.string_of_equality ~env current);
+*)
let res =
forward_simplify eq_uri env 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";
+(* prerr_endline "infer"; *)
let new' = infer eq_uri env current active in
- prerr_endline "infer goal";
+(* prerr_endline "infer goal"; *)
(*
match check_if_goals_set_is_solved env active goals with
| Some p ->
infer_goal_set_with_current env current goals active
in
(* FORWARD AND BACKWARD SIMPLIFICATION *)
- prerr_endline "fwd/back simpl";
+(* prerr_endline "fwd/back simpl"; *)
let rec simplify new' active passive head =
let new' =
forward_simplify_new eq_uri env new' active
let active, passive, new', head =
simplify new' active passive []
in
- prerr_endline "simpl goal with new";
+(* prerr_endline "simpl goal with new"; *)
let goals =
let a,b,_ = build_table new' in
- let _ = <:start<simplify_goal_set new>> in
+(* let _ = <:start<simplify_goal_set new>> in *)
let rc = simplify_goal_set env goals (a,b) in
- let _ = <:stop<simplify_goal_set new>> in
+(* let _ = <:stop<simplify_goal_set new>> in *)
rc
in
let passive = add_to_passive passive new' head in
raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
| ParamodulationSuccess
(goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
- prerr_endline "OK, found a proof!";
- prerr_endline
+ print_endline "Proof:";
+ print_endline
(Equality.pp_proof names goalproof newproof subsumption_subst
subsumption_id type_of_goal);
- prerr_endline "ENDOFPROOFS";
+(* prerr_endline "ENDOFPROOFS"; *)
+(*
+ prerr_endline ("max weight: " ^
+ (string_of_int (Equality.max_weight goalproof newproof)));
+*)
(* generation of the CIC proof *)
let side_effects =
List.filter (fun i -> i <> goalno)
eq_uri goalproof initial type_of_goal side_effects
context proof_menv
in
- prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
+(* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
(*prerr_endline (CicPp.pp goal_proof names);*)
List.map (Subst.apply_subst subsumption_subst) side_effects_t
in
(* replacing fake mets with real ones *)
- prerr_endline "replacing metas...";
+(* prerr_endline "replacing metas..."; *)
let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
let goal_proof_menv, what, with_what,free_meta =
List.fold_left
(ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
in
-prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) );
+(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int
+ * free_metas) ); *)
(* check/refine/... build the new proof *)
let replaced_goal =
ProofEngineReduction.replace
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
-prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
+(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *)
let _ =
try
CicTypeChecker.type_of_aux' real_menv context goal_proof
let open_goals =
match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
in
+(*
Printf.eprintf
"GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n"
(String.concat ", " (List.map string_of_int open_goals))
(CicMetaSubst.ppmetasenv [] metasenv)
(CicMetaSubst.ppmetasenv [] real_metasenv);
- prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+*)
+ print_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
proof, open_goals
;;
proof,[goalno]
;;
-let get_stats () =
+let get_stats () = ""
+(*
<:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
Equality.get_stats ()
;;
+*)
projects / helm.git / blobdiff