equal
deleted
inserted
replaced
66 timeout, expect, ...}) |
66 timeout, expect, ...}) |
67 mode minimize_command only learn |
67 mode minimize_command only learn |
68 {state, goal, subgoal, subgoal_count, facts} name = |
68 {state, goal, subgoal, subgoal_count, facts} name = |
69 let |
69 let |
70 val ctxt = Proof.context_of state |
70 val ctxt = Proof.context_of state |
71 val hard_timeout = time_mult 2.0 (timeout |> the_default one_day) |
71 val hard_timeout = time_mult 3.0 (timeout |> the_default one_day) |
72 val birth_time = Time.now () |
72 val birth_time = Time.now () |
73 val death_time = Time.+ (birth_time, hard_timeout) |
73 val death_time = Time.+ (birth_time, hard_timeout) |
74 val max_facts = |
74 val max_facts = |
75 max_facts |> the_default (default_max_facts_for_prover ctxt slice name) |
75 max_facts |> the_default (default_max_facts_for_prover ctxt slice name) |
76 val num_facts = length facts |> not only ? Integer.min max_facts |
76 val num_facts = length facts |> not only ? Integer.min max_facts |