X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=a6c4fc8adf0fe614be3e204bc1783f096805df67;hb=22d39afadb3027477e4a42c315ec10518cbf47ed;hp=c933aec0b48c3c11115d8d8346302f1144c93892;hpb=e61d023695578ebf09d487480e6e7cac3a2dd2ee;p=helm.git diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index c933aec0b..a6c4fc8ad 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -18,10 +18,10 @@ let elapsed_time = ref 0.;; let maximal_retained_equality = ref None;; (* equality-selection related globals *) -let use_fullred = ref false;; -let weight_age_ratio = ref 0;; (* settable by the user from the command line *) +let use_fullred = ref true;; +let weight_age_ratio = ref 3;; (* settable by the user from the command line *) let weight_age_counter = ref !weight_age_ratio;; -let symbols_ratio = ref 0;; +let symbols_ratio = ref 2;; let symbols_counter = ref 0;; (* statistics... *) @@ -376,7 +376,10 @@ let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with | Negative -> - Indexing.superposition_left env active_table current, [] + let maxm, res = + Indexing.superposition_left !maxmeta env active_table current in + maxmeta := maxm; + res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in @@ -384,7 +387,9 @@ let infer env sign current (active_list, active_table) = let rec infer_positive table = function | [] -> [], [] | (Negative, equality)::tl -> - let res = Indexing.superposition_left env table equality in + let maxm, res = + Indexing.superposition_left !maxmeta env table equality in + maxmeta := maxm; let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> @@ -455,7 +460,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = let demodulate table current = let newmeta, newcurrent = - Indexing.demodulation !maxmeta env table current in + Indexing.demodulation !maxmeta env table sign current in maxmeta := newmeta; if is_identity env newcurrent then if sign = Negative then Some (sign, newcurrent) @@ -542,8 +547,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t2 = Unix.gettimeofday () in fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1); - let demodulate table target = - let newmeta, newtarget = Indexing.demodulation !maxmeta env table target in + let demodulate sign table target = + let newmeta, newtarget = + Indexing.demodulation !maxmeta env table sign target in maxmeta := newmeta; newtarget in @@ -555,13 +561,13 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in let new_neg, new_pos = - let new_neg = List.map (demodulate active_table) new_neg - and new_pos = List.map (demodulate active_table) new_pos in + let new_neg = List.map (demodulate Negative active_table) new_neg + and new_pos = List.map (demodulate Positive active_table) new_pos in match passive_table with | None -> new_neg, new_pos | Some passive_table -> - List.map (demodulate passive_table) new_neg, - List.map (demodulate passive_table) new_pos + List.map (demodulate Negative passive_table) new_neg, + List.map (demodulate Positive passive_table) new_pos in let t2 = Unix.gettimeofday () in @@ -835,7 +841,7 @@ let rec given_clause env passive active = al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in -(* let (_, ns), (_, ps), _ = passive in *) + let (_, ns), (_, ps), _ = passive in (* Printf.printf "passive:\n%s\n" *) (* (String.concat "\n" *) (* ((List.map (fun e -> "Negative " ^ *) @@ -963,6 +969,16 @@ let rec given_clause_fullred env passive active = match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in + let (_, ns), (_, ps), _ = passive in +(* Printf.printf "passive:\n%s\n" *) +(* (String.concat "\n" *) +(* ((List.map (fun e -> "Negative " ^ *) +(* (string_of_equality ~env e)) *) +(* (EqualitySet.elements ns)) @ *) +(* (List.map (fun e -> "Positive " ^ *) +(* (string_of_equality ~env e)) *) +(* (EqualitySet.elements ps)))); *) +(* print_newline (); *) given_clause_fullred env passive active | true, goal -> Success (goal, env) @@ -996,16 +1012,26 @@ let main () = let module PP = CicPp in let term, metasenv, ugraph = get_from_user () in let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in - let proof, goals = - PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in - let goal = List.nth goals 0 in + let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in + let proof, goals = status in + let goal' = List.nth goals 0 in let _, metasenv, meta_proof, _ = proof in - let _, context, goal = CicUtil.lookup_meta goal metasenv in + let _, context, goal = CicUtil.lookup_meta goal' metasenv in let equalities, maxm = find_equalities context proof in - maxmeta := maxm; (* TODO ugly!! *) + maxmeta := maxm+2; (* TODO ugly!! *) + let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in + let new_meta_goal, metasenv, type_of_goal = + let _, context, ty = CicUtil.lookup_meta goal' metasenv in + Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); + print_newline (); + Cic.Meta (maxm+1, irl), + (maxm+1, context, ty)::metasenv, + ty + in +(* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in try - let term_equality = equality_of_term meta_proof goal in + let term_equality = equality_of_term new_meta_goal goal in let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in let active = make_active () in let passive = make_passive [term_equality] equalities in @@ -1033,9 +1059,34 @@ let main () = Printf.printf "NO proof found! :-(\n\n" | Success (Some goal, env) -> Printf.printf "OK, found a proof!\n"; - let proof = Inference.build_term_proof goal in - print_endline (PP.pp proof (names_of_context context)); + let proof = Inference.build_proof_term goal in + (* REMEMBER: we have to instantiate meta_proof, we should use + apply the "apply" tactic to proof and status + *) + let names = names_of_context context in + print_endline (PP.pp proof names); +(* print_endline (PP.ppterm proof); *) + print_endline (string_of_float (finish -. start)); + let newmetasenv = + List.fold_left + (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities + in + let _ = + try + let ty, ug = + CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + in + Printf.printf + "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" + (CicPp.pp type_of_goal names) (CicPp.pp ty names) + (string_of_bool + (fst (CicReduction.are_convertible context type_of_goal ty ug))); + with e -> + Printf.printf "MAXMETA USED: %d\n" !maxmeta; + in + () + | Success (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in @@ -1062,7 +1113,7 @@ let main () = ;; -let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";; +let configuration_file = ref "../../matita/matita.conf.xml";; let _ = let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1) @@ -1070,16 +1121,17 @@ let _ = and set_conf f = configuration_file := f and set_lpo () = Utils.compare_terms := lpo and set_kbo () = Utils.compare_terms := nonrec_kbo - and set_fullred () = use_fullred := true + and set_fullred b = use_fullred := b and set_time_limit v = time_limit := float_of_int v in Arg.parse [ - "-f", Arg.Unit set_fullred, "Use full-reduction strategy"; + "-f", Arg.Bool set_fullred, + "Enable/disable full-reduction strategy (default: enabled)"; - "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)"; + "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 3)"; "-s", Arg.Int set_sel, - "symbols-based selection ratio (relative to the weight ratio)"; + "symbols-based selection ratio (relative to the weight ratio, default: 2)"; "-c", Arg.String set_conf, "Configuration file (for the db connection)";