(* 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 *) 4;; (* settable by the user *)
let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref 2;;
+let symbols_ratio = ref (* 0 *) 3;;
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 (nl, ns), (pl, ps), tbl = passive in
let howmany = float_of_int howmany
and ratio = float_of_int !weight_age_ratio in
- let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
- and in_age = int_of_float (howmany /. (ratio +. 1.)) in
+ let round v =
+ let t = ceil v in
+ int_of_float (if t -. v < 0.5 then t else v)
+ in
+ let in_weight = round (howmany *. ratio /. (ratio +. 1.))
+ and in_age = round (howmany /. (ratio +. 1.)) in
debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
let symbols, card =
match active with
let _, ps, pl = picka in_age ps pl in
if not (EqualitySet.is_empty ps) then
(* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
- maximal_retained_equality := Some (EqualitySet.max_elt ps);
+ maximal_retained_equality := Some (EqualitySet.max_elt ps);
let tbl =
EqualitySet.fold
(fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
in
derived_clauses := !derived_clauses + (List.length new_neg) +
(List.length new_pos);
- match (* !maximal_weight *)!maximal_retained_equality with
+ match !maximal_retained_equality with
| None -> new_neg, new_pos
- | Some (* w *) eq ->
- let new_pos =
- List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
+ | Some eq ->
+ (* if we have a maximal_retained_equality, we can discard all equalities
+ "greater" than it, as they will never be reached... An equality is
+ greater than maximal_retained_equality if it is bigger
+ wrt. OrderedEquality.compare and it is less similar than
+ maximal_retained_equality to the current goal *)
+ let symbols, card =
+ match active_list with
+ | (Negative, e)::_ ->
+ let symbols = symbols_of_equality e in
+ let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
+ Some symbols, card
+ | _ -> None, 0
+ in
+ let new_pos =
+ match symbols with
+ | None ->
+ List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
+ | Some symbols ->
+ let filterfun e =
+ if OrderedEquality.compare e eq <= 0 then
+ true
+ else
+ let foldfun k v (r1, r2) =
+ if TermMap.mem k symbols then
+ let c = TermMap.find k symbols in
+ let c1 = abs (c - v) in
+ let c2 = v - c1 in
+ r1 + c2, r2 + c1
+ else
+ r1, r2 + v
+ in
+ let initial =
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
+ others + (abs (common - card))
+ in
+ let common, others =
+ TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
+ let c = others + (abs (common - card)) in
+ if c < initial then true else false
+ in
+ List.filter filterfun new_pos
+ in
new_neg, new_pos
;;
in
let all = if pl = [] then active_list else active_list @ pl in
-(* let rec find_duplicate sign current = function *)
+ (* let rec find_duplicate sign current = function *)
(* | [] -> false *)
(* | (s, eq)::tl when s = sign -> *)
(* if meta_convertibility_eq current eq then true *)
;;
-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