equal
deleted
inserted
replaced
562 |
562 |
563 fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths = |
563 fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths = |
564 let |
564 let |
565 val thy = Proof_Context.theory_of ctxt |
565 val thy = Proof_Context.theory_of ctxt |
566 val prover = hd provers |
566 val prover = hd provers |
567 val name = ATP_Util.timestamp () ^ serial_string () (* fresh enough *) |
567 val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *) |
568 val feats = features_of ctxt prover thy General [t] |
568 val feats = features_of ctxt prover thy General [t] |
569 val deps = used_ths |> map Thm.get_name_hint |
569 val deps = used_ths |> map Thm.get_name_hint |
570 in |
570 in |
571 mash_map ctxt (fn {thys, fact_graph} => |
571 mash_map ctxt (fn {thys, fact_graph} => |
572 let |
572 let |
581 end |
581 end |
582 |
582 |
583 (* The threshold should be large enough so that MaSh doesn't kick in for Auto |
583 (* The threshold should be large enough so that MaSh doesn't kick in for Auto |
584 Sledgehammer and Try. *) |
584 Sledgehammer and Try. *) |
585 val min_secs_for_learning = 15 |
585 val min_secs_for_learning = 15 |
586 val short_learn_timeout_factor = 0.2 |
586 val learn_timeout_factor = 2.0 |
587 val long_learn_timeout_factor = 4.0 |
|
588 |
587 |
589 fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover |
588 fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover |
590 max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = |
589 max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = |
591 if not (subset (op =) (the_list fact_filter, fact_filters)) then |
590 if not (subset (op =) (the_list fact_filter, fact_filters)) then |
592 error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") |
591 error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".") |
595 else if max_facts <= 0 orelse null facts then |
594 else if max_facts <= 0 orelse null facts then |
596 [] |
595 [] |
597 else |
596 else |
598 let |
597 let |
599 val thy = Proof_Context.theory_of ctxt |
598 val thy = Proof_Context.theory_of ctxt |
600 fun maybe_learn can_suggest = |
599 fun maybe_learn () = |
601 if not learn orelse Async_Manager.has_running_threads MaShN then |
600 if not learn orelse Async_Manager.has_running_threads MaShN then |
602 () |
601 () |
603 else if Time.toSeconds timeout >= min_secs_for_learning then |
602 else if Time.toSeconds timeout >= min_secs_for_learning then |
604 let |
603 let |
605 val factor = |
604 val soft_timeout = time_mult learn_timeout_factor timeout |
606 if can_suggest then short_learn_timeout_factor |
605 val hard_timeout = time_mult 4.0 soft_timeout |
607 else long_learn_timeout_factor |
|
608 val soft_timeout = time_mult factor timeout |
|
609 val hard_timeout = time_mult 2.0 soft_timeout |
|
610 val birth_time = Time.now () |
606 val birth_time = Time.now () |
611 val death_time = Time.+ (birth_time, hard_timeout) |
607 val death_time = Time.+ (birth_time, hard_timeout) |
612 val desc = ("machine learner for Sledgehammer", "") |
608 val desc = ("machine learner for Sledgehammer", "") |
613 in |
609 in |
614 Async_Manager.launch MaShN birth_time death_time desc |
610 Async_Manager.launch MaShN birth_time death_time desc |
617 end |
613 end |
618 else |
614 else |
619 () |
615 () |
620 val fact_filter = |
616 val fact_filter = |
621 case fact_filter of |
617 case fact_filter of |
622 SOME ff => |
618 SOME ff => (() |> ff <> iterN ? maybe_learn; ff) |
623 (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt) |
|
624 else (); ff) |
|
625 | NONE => |
619 | NONE => |
626 if mash_can_suggest_facts ctxt then (maybe_learn true; meshN) |
620 if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) |
627 else if mash_could_suggest_facts () then (maybe_learn false; iterN) |
621 else if mash_could_suggest_facts () then (maybe_learn (); iterN) |
628 else iterN |
622 else iterN |
629 val add_ths = Attrib.eval_thms ctxt add |
623 val add_ths = Attrib.eval_thms ctxt add |
630 fun prepend_facts ths accepts = |
624 fun prepend_facts ths accepts = |
631 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
625 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
632 (accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |
626 (accepts |> filter_out (member Thm.eq_thm_prop ths o snd))) |