(* equality-selection related globals *)
let use_fullred = ref true;;
-let weight_age_ratio = ref 3;; (* settable by the user from the command line *)
+let weight_age_ratio = ref (* 5 *) 3;; (* settable by the user *)
let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref 2;;
+let symbols_ratio = ref (* 0 *) 2;;
let symbols_counter = ref 0;;
+(* non-recursive Knuth-Bendix term ordering by default *)
+Utils.compare_terms := Utils.nonrec_kbo;;
+
(* statistics... *)
let derived_clauses = ref 0;;
let kept_clauses = ref 0;;
;;
-let backward_simplify_active env new_pos new_table active =
+let backward_simplify_active env new_pos new_table min_weight active =
let active_list, active_table = active in
let active_list, newa =
List.fold_right
(fun (s, equality) (res, newn) ->
- match forward_simplify env (s, equality) (new_pos, new_table) with
- | None -> res, newn
- | Some (s, e) ->
- if equality = e then
- (s, e)::res, newn
- else
- res, (s, e)::newn)
+ let ew, _, _, _, _ = equality in
+ if ew < min_weight then
+ (s, equality)::res, newn
+ else
+ match forward_simplify env (s, equality) (new_pos, new_table) with
+ | None -> res, newn
+ | Some (s, e) ->
+ if equality = e then
+ (s, e)::res, newn
+ else
+ res, (s, e)::newn)
active_list ([], [])
in
let find eq1 where =
;;
-let backward_simplify_passive env new_pos new_table passive =
+let backward_simplify_passive env new_pos new_table min_weight passive =
let (nl, ns), (pl, ps), passive_table = passive in
let f sign equality (resl, ress, newn) =
- match forward_simplify env (sign, equality) (new_pos, new_table) with
- | None -> resl, EqualitySet.remove equality ress, newn
- | Some (s, e) ->
- if equality = e then
- equality::resl, ress, newn
- else
- let ress = EqualitySet.remove equality ress in
- resl, ress, e::newn
+ let ew, _, _, _, _ = equality in
+ if ew < min_weight then
+(* let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *)
+ equality::resl, ress, newn
+ else
+ match forward_simplify env (sign, equality) (new_pos, new_table) with
+ | None -> resl, EqualitySet.remove equality ress, newn
+ | Some (s, e) ->
+ if equality = e then
+ equality::resl, ress, newn
+ else
+ let ress = EqualitySet.remove equality ress in
+ resl, ress, e::newn
in
let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
let backward_simplify env new' ?passive active =
- let new_pos, new_table =
+ let new_pos, new_table, min_weight =
List.fold_left
- (fun (l, t) e -> (Positive, e)::l, Indexing.index t e)
- ([], Indexing.empty_table ()) (snd new')
- in
- let active, newa = backward_simplify_active env new_pos new_table active in
+ (fun (l, t, w) e ->
+ let ew, _, _, _, _ = e in
+ (Positive, e)::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty_table (), 1000000) (snd new')
+ in
+ let active, newa =
+ backward_simplify_active env new_pos new_table min_weight active in
match passive with
| None ->
active, (make_passive [] []), newa, None
| Some passive ->
let passive, newp =
- backward_simplify_passive env new_pos new_table passive in
+ backward_simplify_passive env new_pos new_table min_weight passive in
active, passive, newa, newp
;;
in
()
else
- let active = make_active () in
- let passive =
- make_passive [term_equality] (equalities @ library_equalities)
+ let equalities =
+ let equalities = equalities @ library_equalities in
+ debug_print (
+ Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities)));
+ debug_print "SIMPLYFYING EQUALITIES...";
+ let rec simpl e others others_simpl =
+ let active = others @ others_simpl in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ (Indexing.empty_table ()) active
+ in
+ let res = forward_simplify env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl (e::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> e::others_simpl
+ )
+ in
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = List.map (fun e -> (Positive, e)) tl in
+ let res =
+ List.rev (List.map snd (simpl (Positive, hd) others []))
+ in
+ debug_print (
+ Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res)));
+ res
in
+ let active = make_active () in
+ let passive = make_passive [term_equality] equalities in
Printf.printf "\ncurrent goal: %s\n"
(string_of_equality ~env term_equality);
Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
(String.concat "\n"
(List.map
(string_of_equality ~env)
- equalities));
+ (equalities @ library_equalities)));
print_endline "--------------------------------------------------";
let start = Unix.gettimeofday () in
print_endline "GO!";
with e ->
Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
Printf.printf "MAXMETA USED: %d\n" !maxmeta;
+ print_endline (string_of_float (finish -. start));
in
()
let env = (metasenv, context, ugraph) in
(* try *)
let term_equality = equality_of_term new_meta_goal goal in
- let res =
+ let res, time =
if is_identity env term_equality then
let w, _, (eq_ty, left, right, o), m, a = term_equality in
let proof =
(HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
eq_ty; left]
in
- ParamodulationSuccess
- (Some (0, Inference.BasicProof proof,
- (eq_ty, left, right, o), m, a), env)
+ (ParamodulationSuccess
+ (Some (0, Inference.BasicProof proof,
+ (eq_ty, left, right, o), m, a), env), 0.)
else
let library_equalities, maxm =
find_library_equalities ~dbd context (proof, goal') (maxm+2)
in
maxmeta := maxm+2;
-
+ let equalities =
+ let equalities = equalities @ library_equalities in
+ debug_print (
+ Printf.sprintf "equalities:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality equalities)));
+ debug_print "SIMPLYFYING EQUALITIES...";
+ let rec simpl e others others_simpl =
+ let active = others @ others_simpl in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ (Indexing.empty_table ()) active
+ in
+ let res = forward_simplify env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl (e::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> e::others_simpl
+ )
+ in
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = List.map (fun e -> (Positive, e)) tl in
+ let res =
+ List.rev (List.map snd (simpl (Positive, hd) others []))
+ in
+ debug_print (
+ Printf.sprintf "equalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map string_of_equality res)));
+ res
+ in
let active = make_active () in
- let passive =
- make_passive [term_equality] (equalities @ library_equalities)
- in
+ let passive = make_passive [term_equality] equalities in
+ let start = Unix.gettimeofday () in
let res = given_clause_fullred env passive active in
- res
+ let finish = Unix.gettimeofday () in
+ (res, finish -. start)
in
match res with
| ParamodulationSuccess (Some goal, env) ->
raise (ProofEngineTypes.Fail
"Found a proof, but it doesn't typecheck")
in
+ debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time);
newstatus
| _ ->
raise (ProofEngineTypes.Fail "NO proof found")
projects / helm.git / blobdiff