* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id$ *)
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))
+*)
+ select env g (tl@[hd],pos_set)
| _ -> assert false
in
skip_giant pos_list pos_set)
(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 =
| [] -> 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
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 =
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